Library classcomp
A constructive proof of completeness for classical first-order
logic, globally following the paper of Berardi and Valentini,
itself unwinding Krivine's proof, itself unwinding the classical
proof.
Danko Ilik, October 2008, revisited August 2025
From Stdlib Require Export List.
From Stdlib Require Import Setoid.
From Stdlib Require Import Bool.
From Stdlib Require Import Arith.
From Stdlib Require Import Cantor.
From Stdlib Require Import Sorting.Mergesort.
From Stdlib Require Import Orders.
This imports the proof of the constructive Ultra-filter Theorem
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 quantifier-bound de
Bruijn variable, by a term.
Fixpoint open_rec_term (k : nat) (u : term) (t : term) {struct t} : term :=
match t with
| bvar i ⇒ if Nat.eqb 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.
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.
match t with
| bvar i ⇒ if Nat.eqb 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.
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.
Substituting the first variable in the term u, the one that would
be first captured by a surrounding quantifier, 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, although 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 analogously 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).
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.
| 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).
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.
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) → added_cnsts_f A = false →
(∀ 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) → added_cnsts_f A = false →
(∀ 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 membership 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 using the Cantor pairing function from the Coq
standard library (formerly we used the one from Russell O'Connor's
formalization of the incompleteness theorem)
Section Enumeration.
Definition enump := fun p ⇒ to_nat (11, enum_predicate p).
Definition enumc0 := fun c ⇒ to_nat (12, enum_constant0 c).
Definition enumfunc := fun f ⇒ to_nat (13, enum_function f).
Fixpoint enumf (f:formula) : nat :=
match f with
| (atom p t) ⇒ to_nat (1, to_nat (enump p, enumt t))
| (all g) ⇒ to_nat (2, enumf g)
| (imp g h) ⇒ to_nat (3, to_nat (enumf g, enumf h))
| bot ⇒ to_nat (4, 0)
end
with enumt (t:term) : nat :=
match t with
| (func phi t') ⇒ to_nat (5, to_nat (enumfunc phi, enumt t'))
| (cnst c) ⇒ to_nat (6, enumc c)
| (fvar x) ⇒ to_nat (7, x)
| (bvar x) ⇒ to_nat (8, x)
end
with enumc (c:constant) : nat :=
match c with
| (added x) ⇒ to_nat (9, enumf x)
| (original x) ⇒ to_nat (10, enumc0 x)
end.
Scheme Induction for formula Sort Prop
with Induction for term Sort Prop
with Induction for constant Sort Prop.
Combined Scheme ftc_ind from formula_ind, term_ind, constant_ind.
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).
Opaque to_nat.
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_Proper.
Definition eq_B_meet_morph := meet_morphism_Proper.
Definition bott := bot.
Definition B := formula.
End CBAproof.
Definition enump := fun p ⇒ to_nat (11, enum_predicate p).
Definition enumc0 := fun c ⇒ to_nat (12, enum_constant0 c).
Definition enumfunc := fun f ⇒ to_nat (13, enum_function f).
Fixpoint enumf (f:formula) : nat :=
match f with
| (atom p t) ⇒ to_nat (1, to_nat (enump p, enumt t))
| (all g) ⇒ to_nat (2, enumf g)
| (imp g h) ⇒ to_nat (3, to_nat (enumf g, enumf h))
| bot ⇒ to_nat (4, 0)
end
with enumt (t:term) : nat :=
match t with
| (func phi t') ⇒ to_nat (5, to_nat (enumfunc phi, enumt t'))
| (cnst c) ⇒ to_nat (6, enumc c)
| (fvar x) ⇒ to_nat (7, x)
| (bvar x) ⇒ to_nat (8, x)
end
with enumc (c:constant) : nat :=
match c with
| (added x) ⇒ to_nat (9, enumf x)
| (original x) ⇒ to_nat (10, enumc0 x)
end.
Scheme Induction for formula Sort Prop
with Induction for term Sort Prop
with Induction for constant Sort Prop.
Combined Scheme ftc_ind from formula_ind, term_ind, constant_ind.
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).
Opaque to_nat.
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_Proper.
Definition eq_B_meet_morph := meet_morphism_Proper.
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 formal proof proceeds by induction on 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.
Section constants_in_formulas.
Fixpoint 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.
Fixpoint 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.
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.
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.
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_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
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.
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_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
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.
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) ∧ added_cnsts_f g = false.
Module DepthOrder <: TotalLeBool.
Local Coercion is_true : bool >-> Sortclass.
Definition t := formula.
∃ g:formula, f = ((g^^(cnst (added (all g)))) ⇒ all g)
∧ locl (all g) ∧ added_cnsts_f g = false.
Module DepthOrder <: TotalLeBool.
Local Coercion is_true : bool >-> Sortclass.
Definition t := formula.
an order of deeper-than for the indexes of the Henkin
constants of 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 leb (a b : formula) : bool := Nat.leb (depth b) (depth a).
Infix "<=?" := leb (at level 70, no associativity).
Theorem leb_total : ∀ a1 a2, a1 <=? a2 ∨ a2 <=? a1.
End DepthOrder.
Module Import DepthSort := Sort DepthOrder.
Section DepthOrder_lemmas.
Local Coercion is_true : bool >-> Sortclass.
Lemma leb_transitive : Transitive (fun x y ⇒ is_true (DepthOrder.leb x y)).
End DepthOrder_lemmas.
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 every possible locally closed formula in the language
(regardless whether the formula itself or its universal closure
is in T or not).
Definition henkin_complete (T:formula_set) :=
∀ f:formula,
locl (all f) → added_cnsts_f f = false →
T ((f^^(cnst (added (all f)))) ⇒ all f).
∀ f:formula,
locl (all f) → added_cnsts_f f = false →
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) → added_cnsts_f A = false → (∀ 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) → added_cnsts_f A = false → (∀ 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.
Check completeness.
End classical_completeness.
valid Gamma A → proof Gamma A.
End Completeness.
Check completeness.
End classical_completeness.
This page has been generated by coqdoc