Library classcomp
Krivine's constructive proof of completeness for classical
first-order logic, following the paper of Berardi and Valentini.
Uses Russell O'Connor's implementation of the Cantor Pairing function in Coq.
A part involving list sorting is not fully formalised.
Danko Ilik, October 2008
Uses Russell O'Connor's implementation of the Cantor Pairing function in Coq.
A part involving list sorting is not fully formalised.
Danko Ilik, October 2008
Require Export List.
Require Import Setoid.
Require Import Bool.
Require Import EqNat.
Require Export Peano_dec.
Require Import Compare_dec.
Require Import Max.
Require Import Le.
This imports the proof of the constructive Ultra-filter Theorem
This imports the unfinished list-sorting library
To build the syntax of formulas, we start with decidable countable sets of constant, function, and predicate symbols.
Module Type classical_completeness_signature.
Parameters function predicate constant0 : Set.
Parameter function_dec : ∀ f1 f2:function, {f1 = f2} + {f1 ≠ f2}.
Parameter predicate_dec : ∀ f1 f2:predicate, {f1 = f2} + {f1 ≠ f2}.
Parameter constant0_dec : ∀ f1 f2:constant0, {f1 = f2} + {f1 ≠ f2}.
Parameter enum_function : function → nat.
Parameter enum_predicate : predicate → nat.
Parameter enum_constant0 : constant0 → nat.
Parameter enum_function_inj :
∀ p q, enum_function p = enum_function q → p = q.
Parameter enum_predicate_inj :
∀ p q, enum_predicate p = enum_predicate q → p = q.
Parameter enum_constant0_inj :
∀ p q, enum_constant0 p = enum_constant0 q → p = q.
End classical_completeness_signature.
Module classical_completeness (ccsig:classical_completeness_signature).
Export ccsig.
Parameters function predicate constant0 : Set.
Parameter function_dec : ∀ f1 f2:function, {f1 = f2} + {f1 ≠ f2}.
Parameter predicate_dec : ∀ f1 f2:predicate, {f1 = f2} + {f1 ≠ f2}.
Parameter constant0_dec : ∀ f1 f2:constant0, {f1 = f2} + {f1 ≠ f2}.
Parameter enum_function : function → nat.
Parameter enum_predicate : predicate → nat.
Parameter enum_constant0 : constant0 → nat.
Parameter enum_function_inj :
∀ p q, enum_function p = enum_function q → p = q.
Parameter enum_predicate_inj :
∀ p q, enum_predicate p = enum_predicate q → p = q.
Parameter enum_constant0_inj :
∀ p q, enum_constant0 p = enum_constant0 q → p = q.
End classical_completeness_signature.
Module classical_completeness (ccsig:classical_completeness_signature).
Export ccsig.
A formula is then defined using the above. There is a special added constructor for constants, these are the Henkin constants. There are separate constructors for variables bound by quantifiers bvar, and free variables fvar.
Inductive formula : Set :=
| bot : formula
| imp : formula → formula → formula
| all : formula → formula
| atom : predicate → term → formula
with term : Set :=
| bvar : nat → term
| fvar : nat → term
| cnst : constant → term
| func : function → term → term
with constant : Set :=
| original : constant0 → constant
| added : formula → constant.
| bot : formula
| imp : formula → formula → formula
| all : formula → formula
| atom : predicate → term → formula
with term : Set :=
| bvar : nat → term
| fvar : nat → term
| cnst : constant → term
| func : function → term → term
with constant : Set :=
| original : constant0 → constant
| added : formula → constant.
'Opening up' quantifiers, i.e. replacing a de Bruijn variable bound
by a quantifier, by a formula.
Fixpoint
open_rec (k : nat) (u : term) (t : formula) {struct t} : formula :=
match t with
| bot ⇒ bot
| imp t1 t2 ⇒ imp (open_rec k u t1) (open_rec k u t2)
| all t1 ⇒ all (open_rec (S k) u t1)
| atom p t1 ⇒ atom p (open_rec_term k u t1)
end
with
open_rec_term (k : nat) (u : term) (t : term) {struct t} : term :=
match t with
| bvar i ⇒ if beq_nat k i then u else (bvar i)
| fvar x ⇒ fvar x
| cnst c ⇒ cnst c
| func f t1 ⇒ func f (open_rec_term k u t1)
end.
open_rec (k : nat) (u : term) (t : formula) {struct t} : formula :=
match t with
| bot ⇒ bot
| imp t1 t2 ⇒ imp (open_rec k u t1) (open_rec k u t2)
| all t1 ⇒ all (open_rec (S k) u t1)
| atom p t1 ⇒ atom p (open_rec_term k u t1)
end
with
open_rec_term (k : nat) (u : term) (t : term) {struct t} : term :=
match t with
| bvar i ⇒ if beq_nat k i then u else (bvar i)
| fvar x ⇒ fvar x
| cnst c ⇒ cnst c
| func f t1 ⇒ func f (open_rec_term k u t1)
end.
Substituting the first variable in the term u, by the term t.
Definition open t u := open_rec 0 u t.
Notation "t ^^ u" := (open t u) (at level 67).
Notation "t ^ x" := (open t (fvar x)).
Notation "t ^^ u" := (open t u) (at level 67).
Notation "t ^ x" := (open t (fvar x)).
A formula is locl (locally closed) when all bvar-s are bound by quantifiers, but there might well be fvar-s around.
A term is locally-closed if it simply does not have bound
variables, but let us define it symmetrically to locl.
Definition loclt (t:term) := ∀ n t', (open_rec_term n t' t) = t.
Definition locll (Gamma:list formula) := ∀ B, In B Gamma → locl B.
Definition notin (x:nat) (L:list nat) := not (In x L).
Notation "x \notin L" := (notin x L) (at level 69).
Definition locll (Gamma:list formula) := ∀ B, In B Gamma → locl B.
Definition notin (x:nat) (L:list nat) := not (In x L).
Notation "x \notin L" := (notin x L) (at level 69).
Natural deduction system for classical predicate logic with cofinite quantification
Inductive proof : list formula → formula → Prop :=
| bot_elim : ∀ Gamma,
proof Gamma bot → ∀ A, proof Gamma A
| imp_elim : ∀ Gamma A B,
proof Gamma (imp A B) → proof Gamma A → proof Gamma B
| imp_intro : ∀ Gamma A B,
proof (A::Gamma) B → proof Gamma (imp A B)
| dneg : ∀ Gamma A,
proof Gamma (imp (imp A bot) bot) → proof Gamma A
| hypo : ∀ Gamma A,
In A Gamma → proof Gamma A
| all_elim : ∀ Gamma A,
proof Gamma (all A) → ∀ t:term, proof Gamma (A^^t)
| all_intro : ∀ Gamma A L, locl (all A) →
(∀ x, x \notin L → proof Gamma (A^x)) →
proof Gamma (all A)
| weaken : ∀ Gamma A B, proof Gamma A → proof (B::Gamma) A.
Notation "A ⇒ B" := (imp A B) (at level 55, right associativity).
Notation "'neg' A" := (imp A bot) (at level 53, right associativity).
| bot_elim : ∀ Gamma,
proof Gamma bot → ∀ A, proof Gamma A
| imp_elim : ∀ Gamma A B,
proof Gamma (imp A B) → proof Gamma A → proof Gamma B
| imp_intro : ∀ Gamma A B,
proof (A::Gamma) B → proof Gamma (imp A B)
| dneg : ∀ Gamma A,
proof Gamma (imp (imp A bot) bot) → proof Gamma A
| hypo : ∀ Gamma A,
In A Gamma → proof Gamma A
| all_elim : ∀ Gamma A,
proof Gamma (all A) → ∀ t:term, proof Gamma (A^^t)
| all_intro : ∀ Gamma A L, locl (all A) →
(∀ x, x \notin L → proof Gamma (A^x)) →
proof Gamma (all A)
| weaken : ∀ Gamma A B, proof Gamma A → proof (B::Gamma) A.
Notation "A ⇒ B" := (imp A B) (at level 55, right associativity).
Notation "'neg' A" := (imp A bot) (at level 53, right associativity).
A general set of formulas
Definition of a "minimal model", one without standard
interpretation of absurdity
Record model (M:formula_set) : Prop := {
model_dneg : ∀ A, M (neg neg A ⇒ A);
model_imp_faithful1 : ∀ A B,
M (A ⇒ B) → (M A → M B);
model_imp_faithful2 : ∀ A B,
(M A → M B) → M (A ⇒ B);
model_all_faithful1 : ∀ A,
M (all A) →
∀ t:term, M (A^^t);
model_all_faithful2 : ∀ A, locl (all A) →
(∀ t:term, loclt t → M (A^^t)) →
M (all A)
}.
model_dneg : ∀ A, M (neg neg A ⇒ A);
model_imp_faithful1 : ∀ A B,
M (A ⇒ B) → (M A → M B);
model_imp_faithful2 : ∀ A B,
(M A → M B) → M (A ⇒ B);
model_all_faithful1 : ∀ A,
M (all A) →
∀ t:term, M (A^^t);
model_all_faithful2 : ∀ A, locl (all A) →
(∀ t:term, loclt t → M (A^^t)) →
M (all A)
}.
The definition of a "classical" as opposed to a "minimal" model is
given, but not used.
Definition model_bot_faithful (M:formula_set) := not (M bot).
Definition classical_model (M:formula_set) : Prop :=
model M ∧ model_bot_faithful M.
Definition classical_model (M:formula_set) : Prop :=
model M ∧ model_bot_faithful M.
A set of formulas interprets a sequent Gamma|-A if the inclusion of Gamma
implies the inclusion of A
Definition interprets (M:formula_set)(Gamma:list formula)(A:formula) :=
(∀ f, In f Gamma → M f) → M A.
(∀ f, In f Gamma → M f) → M A.
A sequent is valid if it is true in all models
Definition valid (Gamma:list formula)(A:formula) :=
∀ M, model M → interprets M Gamma A.
Section natural_deduction_lemmas.
Lemma peirce : ∀ Gamma P Q, proof Gamma (((P ⇒ Q) ⇒ P) ⇒ P).
Lemma proof_imp_trans : ∀ Gamma x y z,
proof Gamma (x ⇒ y) → proof Gamma (y ⇒ z) → proof Gamma (x ⇒ z).
Lemma proof_imp_contrapos : ∀ Gamma x y,
proof Gamma (x ⇒ y) → proof Gamma (neg y ⇒ neg x).
End natural_deduction_lemmas.
∀ M, model M → interprets M Gamma A.
Section natural_deduction_lemmas.
Lemma peirce : ∀ Gamma P Q, proof Gamma (((P ⇒ Q) ⇒ P) ⇒ P).
Lemma proof_imp_trans : ∀ Gamma x y z,
proof Gamma (x ⇒ y) → proof Gamma (y ⇒ z) → proof Gamma (x ⇒ z).
Lemma proof_imp_contrapos : ∀ Gamma x y,
proof Gamma (x ⇒ y) → proof Gamma (neg y ⇒ neg x).
End natural_deduction_lemmas.
Some tactics used for building the Lindenbaum algebra below
Ltac impi := apply imp_intro.
Ltac impe := fun x ⇒ apply imp_elim with x.
Ltac dneg := apply dneg.
Ltac hypo := apply hypo; simpl; auto.
Ltac weak := apply weaken.
Ltac tran := fun x ⇒ apply proof_imp_trans with x.
Ltac contra := apply proof_imp_contrapos.
Lemma formula_dec : ∀ x y:formula, {x = y}+{x ≠ y}.
Lemma constant_dec : ∀ f1 f2:constant, {f1 = f2} + {f1 ≠ f2}.
Module Export CBAproof <: CBA.
Ltac impe := fun x ⇒ apply imp_elim with x.
Ltac dneg := apply dneg.
Ltac hypo := apply hypo; simpl; auto.
Ltac weak := apply weaken.
Ltac tran := fun x ⇒ apply proof_imp_trans with x.
Ltac contra := apply proof_imp_contrapos.
Lemma formula_dec : ∀ x y:formula, {x = y}+{x ≠ y}.
Lemma constant_dec : ∀ f1 f2:constant, {f1 = f2} + {f1 ≠ f2}.
Module Export CBAproof <: CBA.
The Lindenbaum Boolean algebra which will be used in the model
existence lemma to build a maximal consistent extension of a set of
formulas. (the "Universal model")
Section boolean_algebra.
Let B := formula.
Definition compl : B → B.
Defined.
Definition meet : B → B → B.
Defined.
Definition join : B → B → B.
Defined.
Definition top : B.
Defined.
Definition eq_B (x y:B): Prop :=
(∃ p:proof nil (x ⇒ y), True)
∧ (∃ p:proof nil (y ⇒ x), True).
Theorem eq_B_refl : reflexive B eq_B.
Theorem eq_B_symm : symmetric B eq_B.
Theorem eq_B_trans : transitive B eq_B.
Notation "x == y" := (eq_B x y) (at level 70, no associativity).
Add Relation B eq_B
reflexivity proved by eq_B_refl
symmetry proved by eq_B_symm
transitivity proved by eq_B_trans
as eq_B_relation.
Add Morphism join with signature eq_B ⇒ eq_B ⇒ eq_B as join_morphism.
Add Morphism meet with signature eq_B ⇒ eq_B ⇒ eq_B as meet_morphism.
Lemma id_B_dec : ∀ x y : B, {x = y}+{x ≠ y}.
Lemma id_B_dec_right : ∀ (x y:B), x<>y →
∃ H:x<>y, id_B_dec x y = right (x=y) H.
Lemma id_B_dec_left : ∀ x:B, ∃ H:x=x,
id_B_dec x x = left (x<>x) H.
Lemma join_idem : ∀ x, join x x == x.
Lemma meet_idem : ∀ x, meet x x == x.
Lemma join_comm : ∀ x y, join x y == join y x.
Lemma meet_comm : ∀ x y, meet x y == meet y x.
Lemma join_assoc : ∀ x y z, join x (join y z) == join (join x y) z.
Lemma meet_assoc : ∀ x y z, meet x (meet y z) == meet (meet x y) z.
Lemma meet_absorb : ∀ x y, meet x (join x y) == x.
Lemma join_absorb : ∀ x y, join x (meet x y) == x.
Lemma join_distrib : ∀ x y z, join (meet x y) z == meet (join x z) (join y z).
Lemma meet_bott : ∀ x, meet bot x == bot.
Lemma join_bott : ∀ x, join bot x == x.
Lemma meet_top : ∀ x, meet top x == x.
Lemma join_top : ∀ x, join top x == top.
Lemma meet_compl : ∀ x, meet x (compl x) == bot.
Lemma join_compl : ∀ x, join x (compl x) == top.
Lemma meet_distrib : ∀ x y z, meet (join x y) z == join (meet x z) (meet y z).
End boolean_algebra.
Let B := formula.
Definition compl : B → B.
Defined.
Definition meet : B → B → B.
Defined.
Definition join : B → B → B.
Defined.
Definition top : B.
Defined.
Definition eq_B (x y:B): Prop :=
(∃ p:proof nil (x ⇒ y), True)
∧ (∃ p:proof nil (y ⇒ x), True).
Theorem eq_B_refl : reflexive B eq_B.
Theorem eq_B_symm : symmetric B eq_B.
Theorem eq_B_trans : transitive B eq_B.
Notation "x == y" := (eq_B x y) (at level 70, no associativity).
Add Relation B eq_B
reflexivity proved by eq_B_refl
symmetry proved by eq_B_symm
transitivity proved by eq_B_trans
as eq_B_relation.
Add Morphism join with signature eq_B ⇒ eq_B ⇒ eq_B as join_morphism.
Add Morphism meet with signature eq_B ⇒ eq_B ⇒ eq_B as meet_morphism.
Lemma id_B_dec : ∀ x y : B, {x = y}+{x ≠ y}.
Lemma id_B_dec_right : ∀ (x y:B), x<>y →
∃ H:x<>y, id_B_dec x y = right (x=y) H.
Lemma id_B_dec_left : ∀ x:B, ∃ H:x=x,
id_B_dec x x = left (x<>x) H.
Lemma join_idem : ∀ x, join x x == x.
Lemma meet_idem : ∀ x, meet x x == x.
Lemma join_comm : ∀ x y, join x y == join y x.
Lemma meet_comm : ∀ x y, meet x y == meet y x.
Lemma join_assoc : ∀ x y z, join x (join y z) == join (join x y) z.
Lemma meet_assoc : ∀ x y z, meet x (meet y z) == meet (meet x y) z.
Lemma meet_absorb : ∀ x y, meet x (join x y) == x.
Lemma join_absorb : ∀ x y, join x (meet x y) == x.
Lemma join_distrib : ∀ x y z, join (meet x y) z == meet (join x z) (join y z).
Lemma meet_bott : ∀ x, meet bot x == bot.
Lemma join_bott : ∀ x, join bot x == x.
Lemma meet_top : ∀ x, meet top x == x.
Lemma join_top : ∀ x, join top x == top.
Lemma meet_compl : ∀ x, meet x (compl x) == bot.
Lemma join_compl : ∀ x, join x (compl x) == top.
Lemma meet_distrib : ∀ x y z, meet (join x y) z == join (meet x z) (meet y z).
End boolean_algebra.
To use the completion of filters from filters.v, we also need an
enumeration of the elements of the Boolean algebra, which is achieved
by borrowing code about the Cantor pairing function from Russell
O'Connor's formalisation of the incompleteness theorem
Section Enumeration.
Add LoadPath "pairing".
Require Import cPair.
Definition enump := fun p ⇒ cPair 11 (enum_predicate p).
Definition enumc0 := fun c ⇒ cPair 12 (enum_constant0 c).
Definition enumfunc := fun f ⇒ cPair 13 (enum_function f).
Fixpoint enumf (f:formula) : nat :=
match f with
| (atom p t) ⇒ cPair 1 (cPair (enump p) (enumt t))
| (all g) ⇒ cPair 2 (enumf g)
| (imp g h) ⇒ cPair 3 (cPair (enumf g) (enumf h))
| bot ⇒ 4
end
with enumt (t:term) : nat :=
match t with
| (func phi t') ⇒ cPair 5 (cPair (enumfunc phi) (enumt t'))
| (cnst c) ⇒ cPair 6 (enumc c)
| (fvar x) ⇒ cPair 7 x
| (bvar x) ⇒ cPair 8 x
end
with enumc (c:constant) : nat :=
match c with
| (added x) ⇒ cPair 9 (enumf x)
| (original x) ⇒ cPair 10 (enumc0 x)
end.
Scheme Induction for formula Sort Prop
with Induction for term Sort Prop
with Induction for constant Sort Prop.
Theorem countable_ftc :
(∀ f g, enumf f = enumf g → f = g)
∧ (∀ t s, enumt t = enumt s → t = s)
∧ (∀ c k, enumc c = enumc k → c = k).
Definition enum := enumf.
Definition countable : ∀ x y, enum x = enum y → x = y
:= proj1 countable_ftc.
End Enumeration.
Definition eq_B_join_morph := join_morphism_Morphism.
Definition eq_B_meet_morph := meet_morphism_Morphism.
Definition bott := bot.
Definition B := formula.
End CBAproof.
Add LoadPath "pairing".
Require Import cPair.
Definition enump := fun p ⇒ cPair 11 (enum_predicate p).
Definition enumc0 := fun c ⇒ cPair 12 (enum_constant0 c).
Definition enumfunc := fun f ⇒ cPair 13 (enum_function f).
Fixpoint enumf (f:formula) : nat :=
match f with
| (atom p t) ⇒ cPair 1 (cPair (enump p) (enumt t))
| (all g) ⇒ cPair 2 (enumf g)
| (imp g h) ⇒ cPair 3 (cPair (enumf g) (enumf h))
| bot ⇒ 4
end
with enumt (t:term) : nat :=
match t with
| (func phi t') ⇒ cPair 5 (cPair (enumfunc phi) (enumt t'))
| (cnst c) ⇒ cPair 6 (enumc c)
| (fvar x) ⇒ cPair 7 x
| (bvar x) ⇒ cPair 8 x
end
with enumc (c:constant) : nat :=
match c with
| (added x) ⇒ cPair 9 (enumf x)
| (original x) ⇒ cPair 10 (enumc0 x)
end.
Scheme Induction for formula Sort Prop
with Induction for term Sort Prop
with Induction for constant Sort Prop.
Theorem countable_ftc :
(∀ f g, enumf f = enumf g → f = g)
∧ (∀ t s, enumt t = enumt s → t = s)
∧ (∀ c k, enumc c = enumc k → c = k).
Definition enum := enumf.
Definition countable : ∀ x y, enum x = enum y → x = y
:= proj1 countable_ftc.
End Enumeration.
Definition eq_B_join_morph := join_morphism_Morphism.
Definition eq_B_meet_morph := meet_morphism_Morphism.
Definition bott := bot.
Definition B := formula.
End CBAproof.
Various lemmas that have to do with general lists or their
interaction with proofs
Section list_proof_lemmas.
Definition included (Gamma:list formula)(T:formula_set) :=
∀ f, In f Gamma → T f.
Lemma nil_included : ∀ Ax, included nil Ax.
Lemma nil_lem1 : ∀ l:list formula, incl nil l.
Lemma included_lem1 : ∀ l1 l2:list formula, ∀ Ax:formula_set,
included l1 Ax → included l2 Ax → included (l1++l2) Ax.
Lemma weaken_lem1 : ∀ Gamma Delta A, incl Gamma Delta →
proof Gamma A → proof Delta A.
End list_proof_lemmas.
Definition included (Gamma:list formula)(T:formula_set) :=
∀ f, In f Gamma → T f.
Lemma nil_included : ∀ Ax, included nil Ax.
Lemma nil_lem1 : ∀ l:list formula, incl nil l.
Lemma included_lem1 : ∀ l1 l2:list formula, ∀ Ax:formula_set,
included l1 Ax → included l2 Ax → included (l1++l2) Ax.
Lemma weaken_lem1 : ∀ Gamma Delta A, incl Gamma Delta →
proof Gamma A → proof Delta A.
End list_proof_lemmas.
A couple of lemmas about locally closed formulas
Section locl_lemmas.
Lemma locl_all_neg : ∀ A, locl (all A) → locl (all (neg A)).
Lemma locl_henkin : ∀ A,
locl (all A) → locl (all (A ⇒ all A)).
Lemma locl_henkin_neg : ∀ A,
locl (all A) → locl (all (neg (A ⇒ all A))).
End locl_lemmas.
Lemma locl_all_neg : ∀ A, locl (all A) → locl (all (neg A)).
Lemma locl_henkin : ∀ A,
locl (all A) → locl (all (A ⇒ all A)).
Lemma locl_henkin_neg : ∀ A,
locl (all A) → locl (all (neg (A ⇒ all A))).
End locl_lemmas.
This section defines a fixpoint c_appears which determines if a
given constant appears in the formula and then goes on to prove
that c_appears f (added (all f)) = false, i.e. that a formula
cannot contain an added (Henkin) constant indexed by itself. This
is obvious, but the proof has to go on the induction of the depth
of the formula.
Another fixpoint added_cnsts is also defined, to check if a formula contains _any_ added constants and is connected to c_appears.
Another fixpoint added_cnsts is also defined, to check if a formula contains _any_ added constants and is connected to c_appears.
Section constants_in_formulas.
Fixpoint c_appears (t:formula)(c:constant) {struct t} : bool :=
match t with
| bot ⇒ false
| imp t1 t2 ⇒ orb (c_appears t1 c) (c_appears t2 c)
| all t1 ⇒ c_appears t1 c
| atom p t1 ⇒ c_appears_term t1 c
end
with
c_appears_term (t:term)(c:constant) {struct t} : bool :=
match t with
| bvar i ⇒ false
| fvar x ⇒ false
| cnst k ⇒ if (constant_dec k c) then true else false
| func f t1 ⇒ c_appears_term t1 c
end.
Fixpoint c_appears (t:formula)(c:constant) {struct t} : bool :=
match t with
| bot ⇒ false
| imp t1 t2 ⇒ orb (c_appears t1 c) (c_appears t2 c)
| all t1 ⇒ c_appears t1 c
| atom p t1 ⇒ c_appears_term t1 c
end
with
c_appears_term (t:term)(c:constant) {struct t} : bool :=
match t with
| bvar i ⇒ false
| fvar x ⇒ false
| cnst k ⇒ if (constant_dec k c) then true else false
| func f t1 ⇒ c_appears_term t1 c
end.
c_appears applied to a list
Fixpoint c_appears_l (l:list formula)(c:constant) {struct l} : bool :=
match l with
| (cons x x0) ⇒ orb (c_appears x c) (c_appears_l x0 c)
| nil ⇒ false
end.
Fixpoint depth (f:formula) : nat :=
match f with
| (atom p t) ⇒ depth_term t
| (all g) ⇒ S (depth g)
| (imp g h) ⇒ S (max (depth g) (depth h))
| bot ⇒ 1
end
with
depth_term (t:term) : nat :=
match t with
| (func f t') ⇒ S (depth_term t')
| (cnst c) ⇒
match c with
| original k ⇒ 1
| added f ⇒ S (depth f)
end
| (fvar x) ⇒ 1
| (bvar x) ⇒ 1
end.
Lemma bb''' : ∀ f g, depth f ≤ depth g → c_appears f (added g) = false.
Theorem c_appears_thm : ∀ f, c_appears f (added (all f)) = false.
Lemma c_appears_l_app : ∀ l1 l2 c,
c_appears_l l1 c = false ∧ c_appears_l l2 c = false →
c_appears_l (l1++l2) c = false.
Fixpoint added_cnsts (t:term) : bool :=
match t with
| (func f t') ⇒ added_cnsts t'
| (cnst c) ⇒
match c with
| (added k) ⇒ true
| (original k) ⇒ false
end
| (fvar x) ⇒ false
| (bvar x) ⇒ false
end.
Fixpoint added_cnsts_f (f:formula) : bool :=
match f with
| (atom p t) ⇒ added_cnsts t
| (all g) ⇒ added_cnsts_f g
| (imp g h) ⇒ added_cnsts_f g || added_cnsts_f h
| bot ⇒ false
end.
Lemma added_cnsts_c_appears : ∀ t k,
added_cnsts t = false → c_appears_term t (added k) = false.
Lemma added_cnsts_c_appears' : ∀ f g,
added_cnsts_f f = false → c_appears f (added g) = false.
End constants_in_formulas.
match l with
| (cons x x0) ⇒ orb (c_appears x c) (c_appears_l x0 c)
| nil ⇒ false
end.
Fixpoint depth (f:formula) : nat :=
match f with
| (atom p t) ⇒ depth_term t
| (all g) ⇒ S (depth g)
| (imp g h) ⇒ S (max (depth g) (depth h))
| bot ⇒ 1
end
with
depth_term (t:term) : nat :=
match t with
| (func f t') ⇒ S (depth_term t')
| (cnst c) ⇒
match c with
| original k ⇒ 1
| added f ⇒ S (depth f)
end
| (fvar x) ⇒ 1
| (bvar x) ⇒ 1
end.
Lemma bb''' : ∀ f g, depth f ≤ depth g → c_appears f (added g) = false.
Theorem c_appears_thm : ∀ f, c_appears f (added (all f)) = false.
Lemma c_appears_l_app : ∀ l1 l2 c,
c_appears_l l1 c = false ∧ c_appears_l l2 c = false →
c_appears_l (l1++l2) c = false.
Fixpoint added_cnsts (t:term) : bool :=
match t with
| (func f t') ⇒ added_cnsts t'
| (cnst c) ⇒
match c with
| (added k) ⇒ true
| (original k) ⇒ false
end
| (fvar x) ⇒ false
| (bvar x) ⇒ false
end.
Fixpoint added_cnsts_f (f:formula) : bool :=
match f with
| (atom p t) ⇒ added_cnsts t
| (all g) ⇒ added_cnsts_f g
| (imp g h) ⇒ added_cnsts_f g || added_cnsts_f h
| bot ⇒ false
end.
Lemma added_cnsts_c_appears : ∀ t k,
added_cnsts t = false → c_appears_term t (added k) = false.
Lemma added_cnsts_c_appears' : ∀ f g,
added_cnsts_f f = false → c_appears f (added g) = false.
End constants_in_formulas.
This section provides that if there is a derivation Gamma |- A,
then there is a derivation Gamma{x/c} |- A{x/c}, where {x/c} is a
substitution of the constant c by the free variable x. This lemma
is needed in henkin_equiconsistent.
Section vanDalen_thm283.
Fixpoint
c2t (t:formula)(c:constant)(x:term) {struct t} : formula :=
match t with
| bot ⇒ bot
| imp t1 t2 ⇒ imp (c2t t1 c x) (c2t t2 c x)
| all t1 ⇒ all (c2t t1 c x)
| atom p t1 ⇒ atom p (c2t_term t1 c x)
end
with
c2t_term (t:term)(c:constant)(x:term) {struct t} : term :=
match t with
| bvar i ⇒ (bvar i)
| fvar x ⇒ fvar x
| cnst k ⇒ if (constant_dec k c) then x else (cnst k)
| func f t1 ⇒ func f (c2t_term t1 c x)
end.
Fixpoint c2tl (l:list formula)(c:constant)(v:term) {struct l} :=
match l with
| (cons x x0) ⇒ (c2t x c v) :: (c2tl x0 c v)
| nil ⇒ nil
end.
Lemma c2t_idem : ∀ (f:formula)(c:constant)(x:term),
c_appears f c = false → c2t f c x = f.
Lemma c2tl_idem : ∀ (Gamma:list formula)(c:constant)(x:term),
c_appears_l Gamma c = false →
c2tl Gamma c x = Gamma.
Lemma c2t_lem2 : ∀ (A:formula)(c:constant)(s:term)(t:term),
c_appears_term t c = false → loclt s →
(c2t A c s) ^^ t = c2t (A ^^ t) c s.
Lemma c2t_lem3 : ∀ (n : nat) (A : formula) (c : constant) (s t : term),
loclt s →
open_rec n (c2t_term t c s) (c2t A c s) = c2t (open_rec n t A) c s.
Lemma openrec_lem1 : ∀ A n t x,
open_rec n t (open_rec n (fvar x) A) =
open_rec n (fvar x) A.
Lemma locl_all_c2t : ∀ A,
locl A →
∀ c x, locl (c2t A c (fvar x)).
Lemma thm283 : ∀ Gamma f x k,
proof Gamma f →
proof (c2tl Gamma (added k) (fvar x)) (c2t f (added k) (fvar x)).
Lemma c2t_term_idem : ∀ c t, c2t_term (cnst c) c t = t.
End vanDalen_thm283.
Fixpoint
c2t (t:formula)(c:constant)(x:term) {struct t} : formula :=
match t with
| bot ⇒ bot
| imp t1 t2 ⇒ imp (c2t t1 c x) (c2t t2 c x)
| all t1 ⇒ all (c2t t1 c x)
| atom p t1 ⇒ atom p (c2t_term t1 c x)
end
with
c2t_term (t:term)(c:constant)(x:term) {struct t} : term :=
match t with
| bvar i ⇒ (bvar i)
| fvar x ⇒ fvar x
| cnst k ⇒ if (constant_dec k c) then x else (cnst k)
| func f t1 ⇒ func f (c2t_term t1 c x)
end.
Fixpoint c2tl (l:list formula)(c:constant)(v:term) {struct l} :=
match l with
| (cons x x0) ⇒ (c2t x c v) :: (c2tl x0 c v)
| nil ⇒ nil
end.
Lemma c2t_idem : ∀ (f:formula)(c:constant)(x:term),
c_appears f c = false → c2t f c x = f.
Lemma c2tl_idem : ∀ (Gamma:list formula)(c:constant)(x:term),
c_appears_l Gamma c = false →
c2tl Gamma c x = Gamma.
Lemma c2t_lem2 : ∀ (A:formula)(c:constant)(s:term)(t:term),
c_appears_term t c = false → loclt s →
(c2t A c s) ^^ t = c2t (A ^^ t) c s.
Lemma c2t_lem3 : ∀ (n : nat) (A : formula) (c : constant) (s t : term),
loclt s →
open_rec n (c2t_term t c s) (c2t A c s) = c2t (open_rec n t A) c s.
Lemma openrec_lem1 : ∀ A n t x,
open_rec n t (open_rec n (fvar x) A) =
open_rec n (fvar x) A.
Lemma locl_all_c2t : ∀ A,
locl A →
∀ c x, locl (c2t A c (fvar x)).
Lemma thm283 : ∀ Gamma f x k,
proof Gamma f →
proof (c2tl Gamma (added k) (fvar x)) (c2t f (added k) (fvar x)).
Lemma c2t_term_idem : ∀ c t, c2t_term (cnst c) c t = t.
End vanDalen_thm283.
A section implementing the drinker paradox and another lemma, both
needed in henkin_equiconsistent.
some things are more naturally stated in terms of the
existential quantifier
Notation "'ex' x" := (neg (all (neg x))) (at level 0).
Lemma ex_intro : ∀ Delta t f, proof ((f^^t)::Delta) (ex f).
Lemma ex_elim : ∀ Gamma f g, locl (all f) →
proof Gamma (neg (all (neg f))) →
(∀ t, proof ((f^^t)::Gamma) g) →
proof Gamma g.
Lemma lemma_HE1 : ∀ Delta h, locl (all (h ⇒ all h)) →
proof Delta ((all (neg (h ⇒ all h))) ⇒ (neg ex (h ⇒ all h))).
Lemma ex_intro : ∀ Delta t f, proof ((f^^t)::Delta) (ex f).
Lemma ex_elim : ∀ Gamma f g, locl (all f) →
proof Gamma (neg (all (neg f))) →
(∀ t, proof ((f^^t)::Gamma) g) →
proof Gamma g.
Lemma lemma_HE1 : ∀ Delta h, locl (all (h ⇒ all h)) →
proof Delta ((all (neg (h ⇒ all h))) ⇒ (neg ex (h ⇒ all h))).
and we also introduce disjunction
Notation "x ∨ y" := ((neg x) ⇒ y).
Lemma disj_intro1 : ∀ Gamma f g, proof (f::Gamma) (f ∨ g).
Lemma disj_intro2 : ∀ Gamma f g, proof (g::Gamma) (f ∨ g).
Lemma disj_elim : ∀ Gamma f g h,
proof (f::Gamma) h → proof (g::Gamma) h → proof Gamma ((f ∨ g) ⇒ h).
Lemma LEM : ∀ Gamma f, proof Gamma (f ∨ neg f).
Lemma lemma_HE2_1 : ∀ h Delta, locl (all h) →
proof (all h::Delta) ex (h ⇒ all h).
Lemma lemma_HE2_2 : ∀ h Delta, locl (all h) →
proof (neg all h :: Delta) ex (neg h).
Lemma disj_intro1 : ∀ Gamma f g, proof (f::Gamma) (f ∨ g).
Lemma disj_intro2 : ∀ Gamma f g, proof (g::Gamma) (f ∨ g).
Lemma disj_elim : ∀ Gamma f g h,
proof (f::Gamma) h → proof (g::Gamma) h → proof Gamma ((f ∨ g) ⇒ h).
Lemma LEM : ∀ Gamma f, proof Gamma (f ∨ neg f).
Lemma lemma_HE2_1 : ∀ h Delta, locl (all h) →
proof (all h::Delta) ex (h ⇒ all h).
Lemma lemma_HE2_2 : ∀ h Delta, locl (all h) →
proof (neg all h :: Delta) ex (neg h).
Drinker paradox
A predicate for distinguishing Henkin axioms
Definition HA := fun f:formula ⇒
∃ g:formula, f = ((g^^(cnst (added (all g)))) ⇒ all g)
∧ locl (all g).
∃ g:formula, f = ((g^^(cnst (added (all g)))) ⇒ all g)
∧ locl (all g).
We also need a technical lemma for removing duplicate henkin axioms
from a context
Section removing_duplicate_henkin_axioms.
Lemma rem_dup_lem1 :
∀ a b g h, g<>h → a = ((g ^^ cnst (added (all g))) ⇒ all g) →
b = ((h ^^ cnst (added (all h))) ⇒ all h) →
depth h ≤ depth g →
c_appears b (added (all g)) = false.
Lemma rem_dup_lem1 :
∀ a b g h, g<>h → a = ((g ^^ cnst (added (all g))) ⇒ all g) →
b = ((h ^^ cnst (added (all h))) ⇒ all h) →
depth h ≤ depth g →
c_appears b (added (all g)) = false.
an order of deeper-than for the indexes of the Henkin
constants of two Henkin axioms; for non-Henkin axioms, no
behaviour is specified intentionally, but that's not a problem
because we use this order only for comparing Henkin axioms
Definition hgt (a b:formula) : bool :=
match a with
| (imp _ a') ⇒
match a' with
| (all a'') ⇒
match b with
| (imp _ b') ⇒
match b' with
| (all b'') ⇒ Compare_dec.leb (depth b'') (depth a'')
| _ ⇒ false
end
| _ ⇒ false
end
| _ ⇒ false
end
| _ ⇒ false
end.
Lemma rem_dup_HA : ∀ Gamma, included Gamma HA →
∃ Gamma', incl Gamma Gamma' ∧ incl Gamma' Gamma ∧
∀ a Delta, Suffix (a::Delta) Gamma' →
∀ g, a = ((g ^^ cnst (added (all g))) ⇒ all g) →
c_appears_l Delta (added (all g)) = false.
End removing_duplicate_henkin_axioms.
Module CBAproof_completion := filter_completion CBAproof.
Export CBAproof_completion.
Section Completeness.
match a with
| (imp _ a') ⇒
match a' with
| (all a'') ⇒
match b with
| (imp _ b') ⇒
match b' with
| (all b'') ⇒ Compare_dec.leb (depth b'') (depth a'')
| _ ⇒ false
end
| _ ⇒ false
end
| _ ⇒ false
end
| _ ⇒ false
end.
Lemma rem_dup_HA : ∀ Gamma, included Gamma HA →
∃ Gamma', incl Gamma Gamma' ∧ incl Gamma' Gamma ∧
∀ a Delta, Suffix (a::Delta) Gamma' →
∀ g, a = ((g ^^ cnst (added (all g))) ⇒ all g) →
c_appears_l Delta (added (all g)) = false.
End removing_duplicate_henkin_axioms.
Module CBAproof_completion := filter_completion CBAproof.
Export CBAproof_completion.
Section Completeness.
T1 is an extension of T2, both sets of formulas
A classical theory is a set of formulas T closed under
derivation over a set of Axioms
Definition theory (Axioms:formula_set)(T:formula_set) :=
∀ f:formula,
(T f ↔
∃ Gamma:list formula,
(included Gamma Axioms ∧ ∃ p:proof Gamma f, True)).
∀ f:formula,
(T f ↔
∃ Gamma:list formula,
(included Gamma Axioms ∧ ∃ p:proof Gamma f, True)).
A set of formulas is Henkin-complete if it contains a Henkin
axiom for any locally closed formula.
Definition henkin_complete (T:formula_set) :=
∀ f:formula,
locl (all f) →
T ((f^^(cnst (added (all f)))) ⇒ all f).
∀ f:formula,
locl (all f) →
T ((f^^(cnst (added (all f)))) ⇒ all f).
Two sets of formulas being equiconsistent
An axiom set is extended with Henkin axioms
A theory that closes the extended axiom set under derivation
Definition TH (T A:formula_set) := fun f:formula ⇒
∃ Gamma:list formula,
included Gamma (AxH T A) ∧ ∃ p:proof Gamma f, True.
∃ Gamma:list formula,
included Gamma (AxH T A) ∧ ∃ p:proof Gamma f, True.
When an axiom set contains no added constants
Definition noHC (A:formula_set) := ∀ f, A f → added_cnsts_f f = false.
Notation "'ex' x" := (neg (all (neg x))) (at level 0).
Open Scope type_scope.
Notation "'ex' x" := (neg (all (neg x))) (at level 0).
Open Scope type_scope.
If T is a theory over an axiom set which contains no Henkin
constants, then (TH T) is equiconsistent with T.
If T is a theory whose axiom set has no Henkin constants, then
(TH T) is a theory which is Henkin-complete and equiconsistent
with T.
Theorem enrich : ∀ T A:formula_set, noHC A → theory A T →
extension (AxH T A) A ∧ extension (TH T A) T ∧
theory (AxH T A) (TH T A) ∧ henkin_complete (TH T A) ∧ equicons (TH T A) T.
extension (AxH T A) A ∧ extension (TH T A) T ∧
theory (AxH T A) (TH T A) ∧ henkin_complete (TH T A) ∧ equicons (TH T A) T.
A theory is also a filter
A subsection which implements the model existence lemma by using
enrich and the ultrafilter Z from filters.v
A Henkin extension of T
Definition T1 : formula → Prop := TH T Ax.
Definition Ax1 : formula → Prop := AxH T Ax.
Definition T1theory := (proj1 (proj2 (proj2 (enrich AxnoHC Ttheory)))).
Definition T1filter : Filter T1 := theory2filter T1theory.
Definition Ax1 : formula → Prop := AxH T Ax.
Definition T1theory := (proj1 (proj2 (proj2 (enrich AxnoHC Ttheory)))).
Definition T1filter : Filter T1 := theory2filter T1theory.
Extend T1 to a meta-dn filter using the Z defined in filters.v
The properties of Z, proved in thm22 in filters.v
An abbreviation for F_n which lives in formula->Prop
The accompanying axioms
Fixpoint GAx (n':nat) : formula → Prop :=
match n' with
| O ⇒ Ax1
| S n ⇒
let Fn := F_ T1 n
in fun f:formula ⇒
GAx n f ∨
enum f = n ∧
equiconsistent Fn (up (union_singl Fn f))
end.
Definition ZAx := fun f:formula ⇒ ∃ n:nat, GAx n f.
Lemma GAx_monotone : ∀ n m:nat, le n m →
∀ f, GAx n f → GAx m f.
Lemma remove_In_neq_In : ∀ ys y xn,
In y ys → y ≠ xn → In y (remove id_B_dec xn ys).
Lemma proof_fold_left : ∀ Gamma f,
proof Gamma f → fold_left meet Gamma top ≤ f.
Lemma fold_left_proof : ∀ Gamma f,
fold_left meet Gamma top ≤ f → proof Gamma f.
match n' with
| O ⇒ Ax1
| S n ⇒
let Fn := F_ T1 n
in fun f:formula ⇒
GAx n f ∨
enum f = n ∧
equiconsistent Fn (up (union_singl Fn f))
end.
Definition ZAx := fun f:formula ⇒ ∃ n:nat, GAx n f.
Lemma GAx_monotone : ∀ n m:nat, le n m →
∀ f, GAx n f → GAx m f.
Lemma remove_In_neq_In : ∀ ys y xn,
In y ys → y ≠ xn → In y (remove id_B_dec xn ys).
Lemma proof_fold_left : ∀ Gamma f,
proof Gamma f → fold_left meet Gamma top ≤ f.
Lemma fold_left_proof : ∀ Gamma f,
fold_left meet Gamma top ≤ f → proof Gamma f.
Every filter F_n is also a theory
Lemma F_n_theory : ∀ n, theory (GAx n) (G n).
Theorem Z'theory : theory ZAx Z'.
Definition metaDN (X:formula_set) := ∀ f:formula,
(X (neg f) → X bot) → X f.
Lemma metaDNZ': metaDN Z'.
Lemma model_existence2 :
(∀ A B : formula, Z' (A ⇒ B) → Z' A → Z' B) ∧
(∀ A B : formula, (Z' A → Z' B) → Z' (A ⇒ B)).
Lemma model_existence3' : henkin_complete Z'.
Lemma model_existence3 :
(∀ A, Z' (all A) → (∀ t:term, Z' (A^^t))) ∧
(∀ A, locl (all A) → (∀ t:term, loclt t → Z' (A^^t)) → Z' (all A)).
Theorem model_existence : extension Z' T ∧ model Z' ∧ equicons T Z'.
End model_existence.
Fixpoint HCl (A:list formula) : bool :=
match A with
| nil ⇒ false
| cons f fs ⇒ orb (added_cnsts_f f) (HCl fs)
end.
Lemma HCl_correct : ∀ f Gamma, In f Gamma → HCl Gamma = false →
added_cnsts_f f = false.
Definition noHCf (f:formula) := added_cnsts_f f = false.
Definition noHCl (A:list formula) := HCl A = false.
Theorem Z'theory : theory ZAx Z'.
Definition metaDN (X:formula_set) := ∀ f:formula,
(X (neg f) → X bot) → X f.
Lemma metaDNZ': metaDN Z'.
Lemma model_existence2 :
(∀ A B : formula, Z' (A ⇒ B) → Z' A → Z' B) ∧
(∀ A B : formula, (Z' A → Z' B) → Z' (A ⇒ B)).
Lemma model_existence3' : henkin_complete Z'.
Lemma model_existence3 :
(∀ A, Z' (all A) → (∀ t:term, Z' (A^^t))) ∧
(∀ A, locl (all A) → (∀ t:term, loclt t → Z' (A^^t)) → Z' (all A)).
Theorem model_existence : extension Z' T ∧ model Z' ∧ equicons T Z'.
End model_existence.
Fixpoint HCl (A:list formula) : bool :=
match A with
| nil ⇒ false
| cons f fs ⇒ orb (added_cnsts_f f) (HCl fs)
end.
Lemma HCl_correct : ∀ f Gamma, In f Gamma → HCl Gamma = false →
added_cnsts_f f = false.
Definition noHCf (f:formula) := added_cnsts_f f = false.
Definition noHCl (A:list formula) := HCl A = false.
Finally, the completeness theorem. If Gamma and A contain no Henkin constants, that is, if they are built up of/like usual formulas, and if A is true in every model in which Gamma is true, then there is a derivation of A with hypothesis form Gamma.
Theorem completeness : ∀ Gamma A, noHCl Gamma → noHCf A →
valid Gamma A → proof Gamma A.
End Completeness.
End classical_completeness.
valid Gamma A → proof Gamma A.
End Completeness.
End classical_completeness.
This page has been generated by coqdoc