#### [Problem Statement](http://younesse.net/Preuve-assistee-par-ordinateur/Coherence_Heyting/) / [Github Repository](https://github.com/youqad/Coherence-of-Heyting-arithmetic)
Terms
- Terms:
-
inductively defined over the Peano signature $(0, S, +, ×)$ as
-
variable or constants
-
$f(t_1, \ldots, t_n)$ where $f$ is a function of arity $n$ and the $t_i$ are terms
-
Fixpoint tlift n t k :=
match t with
| Tvar i => Tvar (if k <=? i then n+i else i)
| Tzero => Tzero
| Tsucc u => Tsucc (tlift n u k)
| Tplus u v => Tplus (tlift n u k) (tlift n v k)
| Tmult u v => Tmult (tlift n u k) (tlift n v k)
end.
Lifting
- Lifting:
-
tlift n t k
increases by $n$ all the variables $≥ k$ in the term $t$ (recall that we’re using De Bruijn indices)
Lifting properties
-
lifting by $n$ over $k$ then $n’$ over $k’$ $⟺$ lifting by $n+n’$ over $k$ provided that $k ≤ k’ ≤ k+n$
Lemma tlift_1 : forall t n n' k k', k <= k' -> k' <= k + n -> tlift n' (tlift n t k) k' = tlift (n' + n) t k.
-
lifting by $n$ over $k$ then $n’$ over $k’$ $⟺$ lifting by $n$ over $n’+k$ then lifting by $n’$ over $k’$ provided that $k’ ≤ k$
Lemma tlift_2 : forall t n n' k k', k' <= k -> tlift n' (tlift n t k) k' = tlift n (tlift n' t k') (n' + k).
⟹ Straightforward proofs:
induction t; intros; simpl; f_equal; repeat break; auto.
relying on
f_equal
and the fact that inductively defined terms are of the form $f(t_1, \ldots, t_n)$
Substitutions
- Substitution:
-
tsubst x t' t
-
replaces
x
int
byt'
where all the variables have been lifted byx
-
and decrement by one all the variables greater than
x
int
this decrementing step stems from the $∀$-elimination and $∃$-introduction natural deduction rules:
| Rforall_e Γ B t : Γ:-(Fforall B) -> Γ:-(fsubst 0 t B) | Rexists_i Γ B t : Γ:-(fsubst 0 t B) -> Γ:-(Fexists B)
-
Substitution-related Lemmas
-
Substituting in a lifted term:
Lemma tsubst_1 : forall t x t' n k, k <= x -> x <= k + n -> tsubst x t' (tlift (S n) t k) = tlift n t k.
-
Substituting, then lifting $⟺$ Lifting then Substituting
Lemma tsubst_2 : forall t x t' n k, k <= x -> tlift n (tsubst x t' t) k = tsubst (n + x) t' (tlift n t k). Lemma tsubst_3 : forall t x t' n k, tlift n (tsubst x t' t) (x + k) = tsubst x (tlift n t' k) (tlift n t (x + S k)).
-
Substituting two times in a row:
Lemma tsubst_4 : forall t x t' y u', tsubst (x + y) u' (tsubst x t' t) = tsubst x (tsubst y u' t') (tsubst (x + S y) u' t).
Bounded terms
- Terms whose variables are $< n$:
-
Inductive cterm n : term -> Prop
cterm
-related lemmas
-
Monotony:
Lemma cterm_1 : forall n t, cterm n t -> forall n', n <= n' -> cterm n' t.
-
Lifting above the upper bound does nothing:
Lemma cterm_2 : forall n t, cterm n t -> forall k, tlift k t n = t.
-
Susbstituting above the upper bound either:
Lemma cterm_3 : forall n t, cterm n t -> forall t' j, n <= j -> tsubst j t' t = t.
-
Substituting the last variable by a closed term decrements the upper bound by one:
Lemma cterm_4 : forall n t, cterm (S n) t -> forall t', cterm 0 t' -> cterm n (tsubst n t' t).
Formulas
Inductive formula :=
| Fequal : term -> term -> formula
| Ffalse : formula
| Fand : formula -> formula -> formula
| For : formula -> formula -> formula
| Fimplies : formula -> formula -> formula
| Fexists : formula -> formula
| Fforall : formula -> formula.
Then: we lift the term lemmas to formulas (the proofs are underlied by the “term inductive” case each time)
Contexts
Definition context := list formula.
(* Lifting to any context *)
Definition clift n Γ k := map (fun A => flift n A k) Γ.
Natural deduction inference rules
Inductive rule : context -> formula -> Prop :=
| Rax Γ A : In A Γ -> Γ:-A
| Rfalse_e Γ : Γ:-Ffalse -> forall A, Γ:-A
| Rand_i Γ B C : Γ:-B -> Γ:-C -> Γ:-B/\C
| Rand_e1 Γ B C : Γ:-B/\C -> Γ:-B
| Rand_e2 Γ B C : Γ:-B/\C -> Γ:-C
| Ror_i1 Γ B C : Γ:-B -> Γ:-B\/C
| Ror_i2 Γ B C : Γ:-C -> Γ:-B\/C
| Ror_e Γ A B C : Γ:-B\/C -> (B::Γ):-A -> (C::Γ):-A -> Γ:-A
| Rimpl_i Γ B C : (B::Γ):-C -> Γ:-B==>C
| Rimpl_e Γ B C : Γ:-B==>C -> Γ:-B -> Γ:-C
| Rforall_i Γ B : (clift 1 Γ 0):-B -> Γ:-(Fforall B)
| Rforall_e Γ B t : Γ:-(Fforall B) -> Γ:-(fsubst 0 t B)
| Rexists_i Γ B t : Γ:-(fsubst 0 t B) -> Γ:-(Fexists B)
| Rexists_e Γ A B :
Γ:-(Fexists B) -> (B::clift 1 Γ 0):-(flift 1 A 0) -> Γ:-A
where "Γ :- A" := (rule Γ A).
Theorems:
Definition Thm T :=
exists axioms, (forall A, In A axioms -> PeanoAx A) /\ (axioms:-T).
The overall goal is to show that $⊥$ is not a theorem
Valuations
Semantics: Interpretation of terms and formulas via valuations
Definition valuation := list nat.
Fixpoint tinterp (v:valuation) t :=
match t with
| Tvar j => nth j v O
| Tzero => O
| Tsucc t => S (tinterp v t)
| Tplus t t' => tinterp v t + tinterp v t'
| Tmult t t' => tinterp v t * tinterp v t'
end.
Fixpoint finterp v A :=
match A with
| Fequal t t' => tinterp v t = tinterp v t'
| Ffalse => False
| Fand B C => finterp v B /\ finterp v C
| For B C => finterp v B \/ finterp v C
| Fimplies B C => finterp v B -> finterp v C
| Fexists B => exists n, finterp (n::v) B
| Fforall B => forall n, finterp (n::v) B
end.
tinterp
-related lemmas
tinterp
:-
- for a
tlift
ed term - for a
tsubst
ituted one
- for a
Lemma tinterp_1 : forall t v0 v1 v2,
tinterp (v0++v1++v2) (tlift (length v1) t (length v0)) =
tinterp (v0++v2) t.
Lemma tinterp_2 : forall t' t v1 v2,
tinterp (v1 ++ v2) (tsubst (length v1) t' t) =
tinterp (v1 ++ (tinterp v2 t') :: v2) t.
Then: we lift these lemmas to formulas
Last Lemmas
Lemma soundness_rules : forall Γ A, Γ:-A ->
forall v, cinterp v Γ -> finterp v A.
relying on:
(* n-times repeated Tsucc *)
Fixpoint nTsucc n :=
match n with
| 0 => (fun t => t)
| S m => (fun t => Tsucc (nTsucc m t))
end.
Lemma nTsucc_at_n0 : forall A n n0 v, finterp (n0::v) (nFforall n A)
<-> finterp v (nFforall n (fsubst n (nTsucc n0 Tzero) A)).
Lemma soundness_axioms : forall A, PeanoAx A -> forall v, finterp v A.
Finally leading to:
Theorem soundness : forall A, Thm A -> forall v, finterp v A.
Theorem coherence : ~Thm Ffalse.