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

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
Require Import filters.
This imports the unfinished list-sorting library
Require Import lists.



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} + {f1f2}.
  Parameter predicate_dec : ∀ f1 f2:predicate, {f1 = f2} + {f1f2}.
  Parameter constant0_dec : ∀ f1 f2:constant0, {f1 = f2} + {f1f2}.
  Parameter enum_function : functionnat.
  Parameter enum_predicate : predicatenat.
  Parameter enum_constant0 : constant0nat.
  Parameter enum_function_inj :
    ∀ p q, enum_function p = enum_function qp = q.
  Parameter enum_predicate_inj :
    ∀ p q, enum_predicate p = enum_predicate qp = q.
  Parameter enum_constant0_inj :
    ∀ p q, enum_constant0 p = enum_constant0 qp = 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 : formulaformulaformula
| all : formulaformula
| atom : predicatetermformula
with term : Set :=
| bvar : natterm
| fvar : natterm
| cnst : constantterm
| func : functiontermterm
with constant : Set :=
| original : constant0constant
| added : formulaconstant.

'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
    | botbot
    | imp t1 t2imp (open_rec k u t1) (open_rec k u t2)
    | all t1all (open_rec (S k) u t1)
    | atom p t1atom 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 iif beq_nat k i then u else (bvar i)
    | fvar xfvar x
    | cnst ccnst c
    | func f t1func 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)).

A formula is locl (locally closed) when all bvar-s are bound by quantifiers, but there might well be fvar-s around.
Definition locl (f:formula) := ∀ n t, (open_rec n t f) = f.

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 Gammalocl 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 formulaformulaProp :=
| bot_elim : ∀ Gamma,
  proof Gamma bot → ∀ A, proof Gamma A
| imp_elim : ∀ Gamma A B,
  proof Gamma (imp A B) → proof Gamma Aproof Gamma B
| imp_intro : ∀ Gamma A B,
  proof (A::Gamma) Bproof Gamma (imp A B)
| dneg : ∀ Gamma A,
  proof Gamma (imp (imp A bot) bot) → proof Gamma A
| hypo : ∀ Gamma A,
  In A Gammaproof 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 Lproof Gamma (A^x)) →
    proof Gamma (all A)
| weaken : ∀ Gamma A B, proof Gamma Aproof (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 formula_set := formulaProp.

Definition of a "minimal model", one without standard interpretation of absurdity
Record model (M:formula_set) : Prop := {

  model_dneg : ∀ A, M (neg neg AA);
  
  model_imp_faithful1 : ∀ A B,
    M (AB) → (M AM B);
  
  model_imp_faithful2 : ∀ A B,
    (M AM B) → M (AB);
  
  model_all_faithful1 : ∀ A,
    M (all A) →
    ∀ t:term, M (A^^t);
  
  model_all_faithful2 : ∀ A, locl (all A) →
    (∀ t:term, loclt tM (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 Mmodel_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 GammaM f) → M A.

A sequent is valid if it is true in all models
Definition valid (Gamma:list formula)(A:formula) :=
  ∀ M, model Minterprets M Gamma A.

Section natural_deduction_lemmas.
  Lemma peirce : ∀ Gamma P Q, proof Gamma (((PQ) ⇒ P) ⇒ P).

  Lemma proof_imp_trans : ∀ Gamma x y z,
    proof Gamma (xy) → proof Gamma (yz) → proof Gamma (xz).

  Lemma proof_imp_contrapos : ∀ Gamma x y,
    proof Gamma (xy) → proof Gamma (neg yneg x).
End natural_deduction_lemmas.

Some tactics used for building the Lindenbaum algebra below
Ltac impi := apply imp_intro.
Ltac impe := fun xapply imp_elim with x.
Ltac dneg := apply dneg.
Ltac hypo := apply hypo; simpl; auto.
Ltac weak := apply weaken.
Ltac tran := fun xapply 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} + {f1f2}.

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 : BB.
  Defined.

  Definition meet : BBB.
  Defined.

  Definition join : BBB.
  Defined.

  Definition top : B.
  Defined.

  Definition eq_B (x y:B): Prop :=
    (∃ p:proof nil (xy), True)
    ∧ (∃ p:proof nil (yx), 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_Beq_Beq_B as join_morphism.

  Add Morphism meet with signature eq_Beq_Beq_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 pcPair 11 (enum_predicate p).
  Definition enumc0 := fun ccPair 12 (enum_constant0 c).
  Definition enumfunc := fun fcPair 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 gf = g)
    ∧ (∀ t s, enumt t = enumt st = s)
    ∧ (∀ c k, enumc c = enumc kc = k).

  Definition enum := enumf.

  Definition countable : ∀ x y, enum x = enum yx = 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 GammaT 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 Axincluded l2 Axincluded (l1++l2) Ax.

  Lemma weaken_lem1 : ∀ Gamma Delta A, incl Gamma Delta
    proof Gamma Aproof 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 (Aall A)).

  Lemma locl_henkin_neg : ∀ A,
    locl (all A) → locl (all (neg (Aall 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.
Section constants_in_formulas.
  Fixpoint c_appears (t:formula)(c:constant) {struct t} : bool :=
    match t with
      | botfalse
      | imp t1 t2orb (c_appears t1 c) (c_appears t2 c)
      | all t1c_appears t1 c
      | atom p t1c_appears_term t1 c
    end
  with
    c_appears_term (t:term)(c:constant) {struct t} : bool :=
    match t with
      | bvar ifalse
      | fvar xfalse
      | cnst kif (constant_dec k c) then true else false
      | func f t1c_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)
      | nilfalse
    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 fS (depth f)
        end
      | (fvar x) ⇒ 1
      | (bvar x) ⇒ 1
    end.

  Lemma bb''' : ∀ f g, depth fdepth gc_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 = falsec_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
      | botfalse
    end.

  Lemma added_cnsts_c_appears : ∀ t k,
    added_cnsts t = falsec_appears_term t (added k) = false.

  Lemma added_cnsts_c_appears' : ∀ f g,
    added_cnsts_f f = falsec_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
      | botbot
      | imp t1 t2imp (c2t t1 c x) (c2t t2 c x)
      | all t1all (c2t t1 c x)
      | atom p t1atom 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 xfvar x
      | cnst kif (constant_dec k c) then x else (cnst k)
      | func f t1func 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)
      | nilnil
    end.

  Lemma c2t_idem : ∀ (f:formula)(c:constant)(x:term),
    c_appears f c = falsec2t 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 = falseloclt 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.
Section drinker.

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 (hall h)) →
    proof Delta ((all (neg (hall h))) ⇒ (neg ex (hall h))).

and we also introduce disjunction
  Notation "x ∨ y" := ((neg x) ⇒ y).

  Lemma disj_intro1 : ∀ Gamma f g, proof (f::Gamma) (fg).

  Lemma disj_intro2 : ∀ Gamma f g, proof (g::Gamma) (fg).

  Lemma disj_elim : ∀ Gamma f g h,
    proof (f::Gamma) hproof (g::Gamma) hproof Gamma ((fg) ⇒ h).

  Lemma LEM : ∀ Gamma f, proof Gamma (fneg f).

  Lemma lemma_HE2_1 : ∀ h Delta, locl (all h) →
    proof (all h::Delta) ex (hall h).

  Lemma lemma_HE2_2 : ∀ h Delta, locl (all h) →
    proof (neg all h :: Delta) ex (neg h).

Drinker paradox
  Lemma lemma_HE2 : ∀ Delta h, locl (all h) →
    proof Delta (ex (hall h)).
End drinker.

A predicate for distinguishing Henkin axioms
Definition HA := fun f:formula ⇒
  ∃ 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 hdepth 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.

T1 is an extension of T2, both sets of formulas
  Definition extension (T1 T2:formula_set) := ∀ f, T2 fT1 f.

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)).

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).

Two sets of formulas being equiconsistent
  Definition equicons (X Y:formula_set) := X botY bot.

An axiom set is extended with Henkin axioms
  Definition AxH (T A:formula_set) := fun f:formula ⇒ A fHA f.

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.

When an axiom set contains no added constants
  Definition noHC (A:formula_set) := ∀ f, A fadded_cnsts_f f = false.

  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.
  Lemma henkin_equiconsistent : ∀ A T:formula_set, noHC Atheory A T
    (TH T A) botT bot.

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 Atheory A T
    extension (AxH T A) Aextension (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
  Theorem theory2filter : ∀ T Ax, theory Ax TFilter T.

A subsection which implements the model existence lemma by using enrich and the ultrafilter Z from filters.v
  Section model_existence.
    Variables (T Ax:formula_set)(AxnoHC:noHC Ax)(Ttheory:theory Ax T).

A Henkin extension of T
    Definition T1 : formulaProp := TH T Ax.
    Definition Ax1 : formulaProp := 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
    Definition Z' := Z T1.

The properties of Z, proved in thm22 in filters.v
    Definition lem15 := thm22 T1filter.

    Lemma model_existence1 : extension Z' Tequicons T Z'.

An abbreviation for F_n which lives in formula->Prop
    Definition G := F_ T1.

The accompanying axioms
    Fixpoint GAx (n':nat) : formulaProp :=
      match n' with
        | OAx1
        | 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 fGAx m f.

    Lemma remove_In_neq_In : ∀ ys y xn,
      In y ysyxnIn y (remove id_B_dec xn ys).

    Lemma proof_fold_left : ∀ Gamma f,
      proof Gamma ffold_left meet Gamma topf.

    Lemma fold_left_proof : ∀ Gamma f,
      fold_left meet Gamma topfproof 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' (AB) → Z' AZ' B) ∧
      (∀ A B : formula, (Z' AZ' B) → Z' (AB)).

    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 tZ' (A^^t)) → Z' (all A)).

    Theorem model_existence : extension Z' Tmodel Z'equicons T Z'.

  End model_existence.

  Fixpoint HCl (A:list formula) : bool :=
    match A with
      | nilfalse
      | cons f fsorb (added_cnsts_f f) (HCl fs)
    end.

  Lemma HCl_correct : ∀ f Gamma, In f GammaHCl 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 GammanoHCf A
    valid Gamma Aproof Gamma A.

End Completeness.

End classical_completeness.

This page has been generated by coqdoc