Common Declarations
This page contains 12 theorems of higher-order logic. The theorems verify that a certain M-set model of elementary type theory gives a model of higher-order abstract syntax.
Xin Zhang is currently trying to get LEO-II to prove the last four theorems automatically.
Common Declarations
substmonoid
The set of (sigma-normal) substitutions forms a monoid M. Difficulty: Easy Note: Leo-II has proved this automatically.termmset
The set of (sigma-normal) terms T forms an M-set. Difficulty: Easy Note: Leo-II has proved this automatically.hoasapinj1
(ac)=(bd) → a=b is true in the M-set model. Difficulty: Easy Note: Leo-II has proved this automatically.hoasapinj2
(ac)=(bd) → c=d is true in the M-set model. Difficulty: Easy Note: Leo-II has proved this automatically.hoaslaminj
(λf)=(λg) → f=g is true in the M-set model. Difficulty: A Bit Challenging Note: Leo-II has proved this automatically.hoaslamnotap
(λf)≠(ab) is true in the M-set model. Difficulty: Easy Note: Leo-II has proved this automatically.hoaslamnotvar
¬(Var (λ f)) is true in the M-set model. Difficulty: Easy Note: Leo-II has proved this automatically.hoasapnotvar
¬(Var (ab)) is true in the M-set model. Difficulty: Easy Note: Leo-II has proved this automatically.pushprop
If P(a) holds and P(x[m]) holds for every variable x, then P(x[a.m]) holds for every variable x. Proof: Induction on variables. Difficulty: Challenging Note: Leo-II has not proved this automatically.induction2lem
If P satisfies closure properties with respect to application and λ-abstraction, then P(a[m]) for any term a and substitution m such that P(x[m]) for all variable x. Proof: Use induction and pushprop. Difficulty: Very Challenging -- LEO-II would need to synthesize a set substitution of the form (λa.∀m.(∀x.*→*)→*) Note: Leo-II has not proved this automatically.induction2
If P is true for variables and satisfies closure properties with respect to application and λ-abstraction, then P(a[m]) for any term a. Proof: Use induction2lem. Difficulty: Relatively Easy Note: Leo-II has not proved this automatically.hoasinduction
The induction principle (∀ P . (∀ x . Var(x) → P(x)) → (∀ a b . P(a) → P(b) → P(ab)) → (&forall f . (&forall a.P(a) → P(f(a))) → P(λ f)) → &forall a . P(a)) is true in the M-set model. Proof: Use induction2. Difficulty: A Bit Challenging Note: Leo-II has not proved this automatically.Javascript Interactive Higher-Order Theorem Prover
Automated Reasoning in Higher Order Logic
