:: G{\"o}del's Completeness Theorem
::  by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, CQC_LANG, QC_LANG1, XBOOLE_0, VALUAT_1,
      FINSEQ_1, HENMODEL, CQC_THE1, XBOOLEAN, BVFUNC_2, FUNCT_1, ORDINAL4,
      CALCUL_1, ARYTM_3, RELAT_1, CARD_1, XXREAL_0, TARSKI, ZF_MODEL, CQC_SIM1,
      REALSET1, SUBSTUT1, SUBSTUT2, ZF_LANG, ARYTM_1, CARD_3, ZFMISC_1,
      FINSET_1, MCART_1, GOEDELCP, ORDINAL1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, NAT_1,
      ORDINAL1, CARD_3, FINSEQ_1, FUNCT_1, QC_LANG1, QC_LANG2, QC_LANG3,
      NUMBERS, CQC_LANG, RELAT_1, FINSET_1, VALUAT_1, RELSET_1, FUNCT_2,
      CQC_SIM1, DOMAIN_1, XTUPLE_0, MCART_1, SUBSTUT1, SUBLEMMA, SUBSTUT2,
      CALCUL_1, HENMODEL;
 constructors SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, NAT_D, FINSEQ_2, QC_LANG3,
      CQC_SIM1, SUBSTUT2, CALCUL_1, HENMODEL, CARD_3, RELSET_1, XTUPLE_0;
 registrations SUBSET_1, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, CQC_LANG,
      HENMODEL, FINSEQ_1, FINSET_1, CARD_3, RELSET_1, XTUPLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0, XTUPLE_0;
 theorems TARSKI, FUNCT_1, MCART_1, XBOOLE_0, XBOOLE_1, CQC_LANG, QC_LANG1,
      ZFMISC_1, RELAT_1, QC_LANG3, QC_LANG2, HENMODEL, CALCUL_1, SUBLEMMA,
      NAT_1, FINSEQ_1, VALUAT_1, FUNCT_2, SUBSTUT2, CQC_SIM1, CARD_4, CALCUL_2,
      SUPINF_2, XREAL_1, XXREAL_0, ORDINAL1;
 schemes XBOOLE_0, NAT_1, FUNCT_1, SUBSTUT2, RECDEF_1;

begin :: Henkin`s Theorem

registration
  cluster countable for QC-alphabet;
  existence
  proof
A1: [: NAT,NAT :] is QC-alphabet by QC_LANG1:def 1;
  [:NAT,NAT:] is countable by CARD_4:7;
  hence thesis by A1;
  end;
end;

reserve Al for QC-alphabet;
reserve b,c,d for set,
  X,Y for Subset of CQC-WFF(Al),
  i,j,k,m,n for Element of NAT,
  p,p1,q,r,s,s1 for Element of CQC-WFF(Al),
  x,x1,x2,y,y1 for bound_QC-variable of Al,
  A for non empty set,
  J for interpretation of Al, A,
  v for Element of Valuations_in(Al,A),
  f1,f2 for FinSequence of CQC-WFF(Al),
  CX,CY,CZ for Consistent Subset of CQC-WFF(Al),
  JH for Henkin_interpretation of CX,
  a for Element of A,
  t,u for QC-symbol of Al;

definition
  let Al,X;
  attr X is negation_faithful means
  :Def1:
  X |- p or X |- 'not' p;
end;

definition
  let Al,X;
  attr X is with_examples means
  :Def2:
  for x,p holds ex y st X |- ('not' Ex(x,p)) 'or' (p.(x,y));
end;

theorem
  CX is negation_faithful implies (CX |- p iff not CX |- 'not' p)
  by Def1,HENMODEL:def 2;

theorem Th2:
  for f being FinSequence of CQC-WFF(Al) holds
  |- f^<*'not' p 'or' q*> & |- f^<*p*> implies |- f^<*q*>
proof
  let f be FinSequence of CQC-WFF(Al) such that
A1: |- f^<*'not' p 'or' q*> and
A2: |- f^<*p*>;
  set f1 = f^<*'not' p*>^<*p*>;
A3: Ant(f1) = f^<*'not' p*> by CALCUL_1:5;
A4: Ant(f^<*p*>) = f by CALCUL_1:5;
  Suc(f^<*p*>) = p by CALCUL_1:5;
  then Suc(f^<*p*>) = Suc(f1) by CALCUL_1:5;
  then
A5: |- f1 by A2,A3,A4,CALCUL_1:8,36;
  set f2 = f^<*'not' p*>^<*'not' p*>;
A6: Ant(f2) = f^<*'not' p*> by CALCUL_1:5;
A7: Suc(f2) = 'not' p by CALCUL_1:5;
A8: (Ant(f2)).(len f+1) = 'not' p by A6,FINSEQ_1:42;
  len f+1 = len f + len <*'not' p *> by FINSEQ_1:39;
  then len f+1 = len Ant(f2) by A6,FINSEQ_1:22;
  then len f+1 in dom Ant(f2) by A6,CALCUL_1:10;
  then Suc(f2) is_tail_of Ant(f2) by A7,A8,CALCUL_1:def 16;
  then
A9: |- f2 by CALCUL_1:33;
A10: 0+1 <= len f2 by CALCUL_1:10;
A11: Ant(f1) = Ant(f2) by A6,CALCUL_1:5;
  'not' Suc(f1) = Suc(f2) by A7,CALCUL_1:5;
  then |- Ant(f1)^<*'not' Suc(f1)*> by A9,A10,A11,CALCUL_1:3;
  then
A12: |- Ant(f1)^<*q*> by A5,CALCUL_1:44;
  set f3 = f^<*q*>^<*q*>;
A13: Ant(f3) = f^<*q*> by CALCUL_1:5;
A14: Suc(f3) = q by CALCUL_1:5;
A15: (Ant(f3)).(len f+1) = q by A13,FINSEQ_1:42;
  len f+1 = len f + len <*q*> by FINSEQ_1:39;
  then len f+1 = len Ant(f3) by A13,FINSEQ_1:22;
  then len f+1 in dom Ant(f3) by A13,CALCUL_1:10;
  then Suc(f3) is_tail_of Ant(f3) by A14,A15,CALCUL_1:def 16;
  then |- f3 by CALCUL_1:33;
  then |- f^<*'not' p 'or' q*>^<*q*> by A3,A12,CALCUL_1:53;
  then
A16: |- f^<*'not' ('not' 'not' p '&' 'not' q)*>^<*q*> by QC_LANG2:def 3;
  set f4 = f^<*'not' q*>^<*'not' 'not' p '&' 'not' q*>;
A17: Suc(f4) = 'not' 'not' p '&' 'not' q by CALCUL_1:5;
  then
A18: |- Ant(f4)^<*'not' 'not' p*> by A16,CALCUL_1:40,48;
A19: |- Ant(f4)^<*'not' q*> by A16,A17,CALCUL_1:41,48;
  set f5 = Ant(f4)^<*'not' 'not' p*>;
  set f6 = Ant(f4)^<*'not' q*>;
A20: Ant(f5) = Ant(f4) by CALCUL_1:5;
A21: Suc(f5) = 'not' 'not' p by CALCUL_1:5;
A22: Ant(f6) = Ant(f4) by CALCUL_1:5;
  Suc(f6) = 'not' q by CALCUL_1:5;
  then |- Ant(f4)^<*'not' 'not' p '&' 'not' q*> by A18,A19,A20,A21,A22,
CALCUL_1:39;
  then |- f^<*'not' q*>^<*'not' 'not' p '&' 'not' q*> by CALCUL_1:5;
  then |- f^<*'not' ('not' 'not' p '&' 'not' q)*>^<*q*> by CALCUL_1:48;
  then
A23: |- f^<*'not' p 'or' q*>^<*q*> by QC_LANG2:def 3;
  1 <= len (f^<*'not' p 'or' q*>) by CALCUL_1:10;
  then |- Ant(f^<*'not' p 'or' q*>)^<*q*> by A1,A23,CALCUL_1:45;
  hence thesis by CALCUL_1:5;
end;

theorem Th3:
  X is with_examples implies (X |- Ex(x,p) iff ex y st X |- p.(x,y))
proof
  assume
A1: X is with_examples;
  thus X |- Ex(x,p) implies ex y st X |- p.(x,y)
  proof
    assume X |- Ex(x,p);
    then consider f1 such that
A2: rng f1 c= X and
A3: |- f1^<*Ex(x,p)*> by HENMODEL:def 1;
    consider y such that
A4: X |- 'not' Ex(x,p) 'or' (p.(x,y)) by A1,Def2;
    consider f2 such that
A5: rng f2 c= X and
A6: |- f2^<*'not' Ex(x,p) 'or' (p.(x,y))*> by A4,HENMODEL:def 1;
    take y;
A7: |- f1^f2^<*Ex(x,p)*> by A3,HENMODEL:5;
    |- f1^f2^<*'not' Ex(x,p) 'or' (p.(x,y))*> by A6,CALCUL_2:20;
    then
A8: |- f1^f2^<*p.(x,y)*> by A7,Th2;
    rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
    then rng(f1^f2) c= X by A2,A5,XBOOLE_1:8;
    hence thesis by A8,HENMODEL:def 1;
  end;
  thus (ex y st X |- p.(x,y)) implies X |- Ex(x,p)
  proof
    given y such that
A9: X |- p.(x,y);
    consider f1 such that
A10: rng f1 c= X and
A11: |- f1^<*p.(x,y)*> by A9,HENMODEL:def 1;
    |- f1^<*Ex(x,p)*> by A11,CALCUL_1:58;
    hence thesis by A10,HENMODEL:def 1;
  end;
end;

theorem
  (CX is negation_faithful & CX is with_examples implies
  (JH,valH(Al) |= p iff CX |- p)) implies
  (CX is negation_faithful & CX is with_examples implies
  (JH,valH(Al) |= 'not' p iff CX |- 'not' p))
  by Def1,HENMODEL:def 2,VALUAT_1:17;

theorem Th5:
  |- f1^<*p*> & |- f1^<*q*> implies |- f1^<*p '&' q*>
proof
  set g = f1^<*p*>;
  set g1 = f1^<*q*>;
  assume that
A1: |- g and
A2: |- g1;
A3: Ant(g) = f1 by CALCUL_1:5;
A4: Suc(g) = p by CALCUL_1:5;
A5: Suc(g1) = q by CALCUL_1:5;
  Ant(g) = Ant(g1) by A3,CALCUL_1:5;
  hence thesis by A1,A2,A3,A4,A5,CALCUL_1:39;
end;

theorem Th6:
  X |- p & X |- q iff X |- p '&' q
proof
  thus X |- p & X |- q implies X |- p '&' q
  proof
    assume that
A1: X |- p and
A2: X |- q;
    consider f1 such that
A3: rng f1 c= X and
A4: |- f1^<*p*> by A1,HENMODEL:def 1;
    consider f2 such that
A5: rng f2 c= X and
A6: |- f2^<*q*> by A2,HENMODEL:def 1;
A7: |- f1^f2^<*p*> by A4,HENMODEL:5;
    |- f1^f2^<*q*> by A6,CALCUL_2:20;
    then
A8: |- f1^f2^<*p '&' q*> by A7,Th5;
    rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
    then rng(f1^f2) c= X by A3,A5,XBOOLE_1:8;
    hence thesis by A8,HENMODEL:def 1;
  end;
  thus X |- p '&' q implies X |- p & X |- q
  proof
    assume X |- p '&' q;
    then consider f1 such that
A9: rng f1 c= X and
A10: |- f1^<*p '&' q*> by HENMODEL:def 1;
A11: |- f1^<*p*> by A10,CALCUL_2:22;
    |- f1^<*q*> by A10,CALCUL_2:23;
    hence thesis by A9,A11,HENMODEL:def 1;
  end;
end;

theorem
  (CX is negation_faithful & CX is with_examples implies
  (JH,valH(Al) |= p iff CX |- p)) &
  (CX is negation_faithful & CX is with_examples implies
  (JH,valH(Al) |= q iff CX |- q)) implies
  (CX is negation_faithful & CX is with_examples
  implies (JH,valH(Al) |= p '&' q iff CX |- p '&' q)) by Th6,VALUAT_1:18;

theorem Th8:
  for p st QuantNbr(p) <= 0 holds
  CX is negation_faithful & CX is with_examples implies
  (JH,valH(Al) |= p iff CX |- p)
proof
  defpred P[Element of CQC-WFF(Al)] means
  CX is negation_faithful & CX is with_examples implies
  (JH,valH(Al) |= $1 iff CX |- $1);
A1: for r,s,x,k for l being CQC-variable_list of k,Al
  for P being QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!l] &
  (P[r] implies P['not' r]) & (P[r] & P[s] implies P[r '&' s])
  by Def1,Th6,HENMODEL:16,17,def 2,VALUAT_1:17,18;
A2: for p st QuantNbr(p) = 0 holds P[p] from SUBSTUT2:sch 3(A1);
  now
    let p;
    assume QuantNbr(p) <= 0;
    then QuantNbr(p) = 0 by NAT_1:2;
    hence P[p] by A2;
  end;
  hence thesis;
end;

theorem Th9:
  J,v |= Ex(x,p) iff ex a st J,v.(x|a) |= p
proof
A1: J,v |= 'not' All(x,'not' p) iff not J,v |= All(x,'not' p) by VALUAT_1:17;
A2: (ex a st not J,v.(x|a) |= 'not' p) implies ex a st J,v.(x|a) |= p
  proof
    given a such that
A3: not J,v.(x|a) |= 'not' p;
    take a;
    thus thesis by A3,VALUAT_1:17;
  end;
  (ex a st J,v.(x|a) |= p) implies ex a st not J,v.(x|a) |= 'not' p
  proof
    given a such that
A4: J,v.(x|a) |= p;
    take a;
    thus thesis by A4,VALUAT_1:17;
  end;
  hence thesis by A1,A2,QC_LANG2:def 5,SUBLEMMA:50;
end;

theorem Th10:
  JH,valH(Al) |= Ex(x,p) iff ex y st JH,valH(Al) |= p.(x,y)
proof
  thus JH,valH(Al) |= Ex(x,p) implies ex y st JH,valH(Al) |= p.(x,y)
  proof
    assume JH,valH(Al) |= Ex(x,p);
    then consider x1 being Element of HCar(Al) such that
A1: JH,(valH(Al)).(x|x1) |= p by Th9;
A2: HCar(Al) = bound_QC-variables(Al) by HENMODEL:def 4;
    valH(Al) = id bound_QC-variables(Al) by HENMODEL:def 6;
    then rng valH(Al) = bound_QC-variables(Al) by RELAT_1:45;
    then consider b such that
A3: b in dom valH(Al) and
A4: (valH(Al)).b = x1 by FUNCT_1:def 3,A2;
    reconsider y = b as bound_QC-variable of Al by A3;
    take y;
    thus thesis by A1,A4,CALCUL_1:24;
  end;
  thus (ex y st JH,valH(Al) |= p.(x,y)) implies JH,valH(Al) |= Ex(x,p)
  proof
    given y such that
A5: JH,valH(Al) |= p.(x,y);
    ex x1 being Element of HCar(Al) st ( (valH(Al)).y = x1)&( JH,(valH(Al)).(x|
    x1) |= p) by A5,CALCUL_1:24;
    hence thesis by Th9;
  end;
end;

theorem Th11:
  J,v |= 'not' Ex(x,'not' p) iff J,v |= All(x,p)
proof
A1: not J,v |= Ex(x,'not' p) iff for a holds not J,v.(x|a) |= 'not' p by Th9;
A2: (for a holds not J,v.(x|a) |= 'not' p) implies for a holds J,v.(x|a) |= p
  proof
    assume
A3: for a holds not J,v.(x|a) |= 'not' p;
    let a;
    not J,v.(x|a) |= 'not' p by A3;
    hence thesis by VALUAT_1:17;
  end;
  (for a holds J,v.(x|a) |= p) implies for a holds not J,v.(x|a) |= 'not' p
  proof
    assume
A4: for a holds J,v.(x|a) |= p;
    let a;
    J,v.(x|a) |= p by A4;
    hence thesis by VALUAT_1:17;
  end;
  hence thesis by A1,A2,SUBLEMMA:50,VALUAT_1:17;
end;

theorem Th12:
  X |- 'not' Ex(x,'not' p) iff X |- All(x,p)
proof
  thus X |- 'not' Ex(x,'not' p) implies X |- All(x,p)
  proof
    assume X |- 'not' Ex(x,'not' p);
    then consider f1 such that
A1: rng f1 c= X and
A2: |- f1^<*'not' Ex(x,'not' p)*> by HENMODEL:def 1;
    |- f1^<*All(x,p)*> by A2,CALCUL_1:68;
    hence thesis by A1,HENMODEL:def 1;
  end;
  thus X |- All(x,p) implies X |- 'not' Ex(x,'not' p)
  proof
    assume X |- All(x,p);
    then consider f1 such that
A3: rng f1 c= X and
A4: |- f1^<*All(x,p)*> by HENMODEL:def 1;
    |- f1^<*'not' Ex(x,'not' p)*> by A4,CALCUL_1:68;
    hence thesis by A3,HENMODEL:def 1;
  end;
end;

theorem
  QuantNbr(Ex(x,p)) = QuantNbr(p)+1
proof
  QuantNbr(Ex(x,p)) = QuantNbr('not' All(x,'not' p)) by QC_LANG2:def 5
    .= QuantNbr(All(x,'not' p)) by CQC_SIM1:16
    .= QuantNbr('not' p) + 1 by CQC_SIM1:18;
  hence thesis by CQC_SIM1:16;
end;

theorem Th14:
  QuantNbr(p) = QuantNbr(p.(x,y))
proof
  QuantNbr(p) = QuantNbr(CQC_Sub([p,Sbst(x,y)])) by SUBSTUT2:25;
  hence thesis by SUBSTUT2:def 1;
end;

reserve L for PATH of q,p,
  F1,F3 for QC-formula of Al,
  a for set;

theorem Th15:
  for p st QuantNbr(p) = 1 holds (CX is negation_faithful & CX is with_examples
  implies (JH,valH(Al) |= p iff CX |- p))
proof
  let p such that
A1: QuantNbr(p) = 1 and
A2: CX is negation_faithful and
A3: CX is with_examples;
  consider q such that
A4: q is_subformula_of p and
A5: ex x,r st q = All(x,r) by A1,SUBSTUT2:32;
  consider x,r such that
A6: q = All(x,r) by A5;
A7: QuantNbr(q) <= 1 by A1,A4,SUBSTUT2:30;
A8: QuantNbr(q) = QuantNbr(r) + 1 by A6,CQC_SIM1:18;
  then 1 <= QuantNbr(q) by NAT_1:11;
  then
A9: 1 = QuantNbr(q) by A7,XXREAL_0:1;
  set L =the  PATH of q,p;
A10: 1 <= len L by A4,SUBSTUT2:def 5;
  defpred P[Element of NAT] means 1 <= $1 & $1 <= len L implies
  ex p1 st p1 = L.$1 & QuantNbr(q) <= QuantNbr(p1) &
  (CX |- p1 iff JH,valH(Al) |= p1);
A11: P[0];
A12: for k st P[k] holds P[k + 1]
  proof
    let k such that
A13: P[k];
    assume that
A14: 1 <= k+1 and
A15: k+1 <= len L;
    set j = k+1;
A16: now
      assume k = 0;
      then
A17:  L.j = q by A4,SUBSTUT2:def 5;
      take q;
      thus QuantNbr(q) <= QuantNbr(q);
A18:  now
        assume JH,valH(Al) |= Ex(x,'not' r);
        then consider y such that
A19:    JH,valH(Al) |= ('not' r).(x,y) by Th10;
        QuantNbr('not' r) = 0 by A8,A9,CQC_SIM1:16;
        then QuantNbr(('not' r).(x,y)) = 0 by Th14;
        then CX |- ('not' r).(x,y) by A2,A3,A19,Th8;
        hence CX |- Ex(x,'not' r) by A3,Th3;
      end;
      now
        assume CX |- Ex(x,'not' r);
        then consider y such that
A20:    CX |- ('not' r).(x,y) by A3,Th3;
        QuantNbr('not' r) = 0 by A8,A9,CQC_SIM1:16;
        then QuantNbr(('not' r).(x,y)) = 0 by Th14;
        then JH,valH(Al) |= ('not' r).(x,y) by A2,A3,A20,Th8;
        hence JH,valH(Al) |= Ex(x,'not' r) by Th10;
      end;
      then JH,valH(Al) |= 'not' Ex(x,'not' r) iff CX |- 'not' Ex(x,'not' r)
      by A2,A18,Def1,HENMODEL:def 2,VALUAT_1:17;
      then JH,valH(Al) |= q iff CX |- q by A6,Th11,Th12;
      hence thesis by A17;
    end;
    now
      assume k <> 0;
      then 0 < k by NAT_1:3;
      then
A21:  0+1 <= k by NAT_1:13;
      k < len L by A15,NAT_1:13;
      then consider G1,H1 being Element of QC-WFF(Al) such that
A22:  L.k = G1 and
A23:  L.j = H1 and
A24:  G1 is_immediate_constituent_of H1 by A4,A21,SUBSTUT2:def 5;
      consider p1 such that
A25:  p1 = L.k and
A26:  QuantNbr(q) <= QuantNbr(p1) and
A27:  CX |- p1 iff JH,valH(Al) |= p1 by A13,A15,A21,NAT_1:13;
A28:  ex F3 st ( F3 = L.j)&( F3 is_subformula_of p) by A4,A14,A15,SUBSTUT2:27;
      reconsider s = H1 as Element of CQC-WFF(Al)
      by A4,A14,A15,A23,SUBSTUT2:28;
      take s;
A29:  now
        assume
A30:    s = 'not' p1;
        then
A31:    QuantNbr(q) <= QuantNbr(s) by A26,CQC_SIM1:16;
        CX |- s iff JH,valH(Al) |= s
        by A2,A27,A30,Def1,HENMODEL:def 2,VALUAT_1:17;
        hence thesis by A23,A31;
      end;
A32:  QuantNbr(s) <= 1 by A1,A23,A28,SUBSTUT2:30;
A33:  now
        given F1 such that
A34:    s = p1 '&' F1;
        reconsider F1 as Element of CQC-WFF(Al) by A34,CQC_LANG:9;
        QuantNbr(s) = QuantNbr(p1) + QuantNbr(F1) by A34,CQC_SIM1:17;
        then
A35:    QuantNbr(p1) <= QuantNbr(s) by NAT_1:11;
        then
A36:    QuantNbr(p1) <= 1 by A32,XXREAL_0:2;
A37:    1 <= QuantNbr(s) by A9,A26,A35,XXREAL_0:2;
A38:    QuantNbr(p1) = 1 by A9,A26,A36,XXREAL_0:1;
        QuantNbr(s) = 1 by A32,A37,XXREAL_0:1;
        then 1-1 = QuantNbr(F1)+1-1 by A34,A38,CQC_SIM1:17;
        then
A39:    CX |- F1 iff JH,valH(Al) |= F1 by A2,A3,Th8;
A40:    QuantNbr(q) <= QuantNbr(s) by A26,A35,XXREAL_0:2;
        CX |- s iff JH,valH(Al) |= s by A27,A34,A39,Th6,VALUAT_1:18;
        hence thesis by A23,A40;
      end;
A41:  now
        given F1 such that
A42:    s = F1 '&' p1;
        reconsider F1 as Element of CQC-WFF(Al) by A42,CQC_LANG:9;
A43:    QuantNbr(s) = QuantNbr(p1) + QuantNbr(F1) by A42,CQC_SIM1:17;
        then
A44:    QuantNbr(p1) <= QuantNbr(s) by NAT_1:11;
        then
A45:    QuantNbr(p1) <= 1 by A32,XXREAL_0:2;
A46:    1 <= QuantNbr(s) by A9,A26,A44,XXREAL_0:2;
A47:    QuantNbr(p1) = 1 by A9,A26,A45,XXREAL_0:1;
        QuantNbr(s) = 1 by A32,A46,XXREAL_0:1;
        then
A48:    CX |- F1 iff JH,valH(Al) |= F1 by A2,A3,A43,A47,Th8;
A49:    QuantNbr(q) <= QuantNbr(s) by A26,A44,XXREAL_0:2;
        CX |- s iff JH,valH(Al) |= s by A27,A42,A48,Th6,VALUAT_1:18;
        hence thesis by A23,A49;
      end;
      now
        given x such that
A50:    s = All(x,p1);
        1 < QuantNbr(p1) + 1 by A9,A26,NAT_1:13;
        hence contradiction by A32,A50,CQC_SIM1:18;
      end;
      hence thesis by A22,A24,A25,A29,A33,A41,QC_LANG2:def 19;
    end;
    hence thesis by A16;
  end;
  for k holds P[k] from NAT_1:sch 1(A11,A12);
  then ex p1 st ( p1 = L.(len L))&( QuantNbr(q) <= QuantNbr(p1))&(
  CX |- p1 iff JH,valH(Al) |= p1) by A10;
  hence thesis by A4,SUBSTUT2:def 5;
end;

theorem Th16:
  for n st for p st QuantNbr(p) <= n holds
  (CX is negation_faithful & CX is with_examples
  implies (JH,valH(Al) |= p iff CX |- p)) holds
  for p st QuantNbr(p) <= n+1 holds
  (CX is negation_faithful & CX is with_examples
  implies (JH,valH(Al) |= p iff CX |- p))
proof
  let n such that
A1: for p st QuantNbr(p) <= n holds
  CX is negation_faithful & CX is with_examples
  implies (JH,valH(Al) |= p iff CX |- p);
  let p such that
A2: QuantNbr(p) <= n+1 and
A3: CX is negation_faithful and
A4: CX is with_examples;
A5: QuantNbr(p) <= n implies thesis by A1,A3,A4;
  now
    assume
A6: QuantNbr(p) = n+1;
    then consider q such that
A7: q is_subformula_of p and
A8: QuantNbr(q) = 1 by NAT_1:11,SUBSTUT2:34;
    set L =the  PATH of q,p;
A9: 1 <= len L by A7,SUBSTUT2:def 5;
    defpred P[Element of NAT] means 1 <= $1 & $1 <= len L implies
    ex p1 st p1 = L.$1 & QuantNbr(q) <= QuantNbr(p1) &
    (CX |- p1 iff JH,valH(Al) |= p1);
A10: P[0];
A11: for k st P[k] holds P[k + 1]
    proof
      let k such that
A12:  P[k];
      assume that
A13:  1 <= k+1 and
A14:  k+1 <= len L;
      set j = k+1;
A15:  now
        assume k = 0;
        then
A16:    L.j = q by A7,SUBSTUT2:def 5;
        take q;
        JH,valH(Al) |= q iff CX |- q by A3,A4,A8,Th15;
        hence thesis by A16;
      end;
      now
        assume k <> 0;
        then 0 < k by NAT_1:3;
        then
A17:    0+1 <= k by NAT_1:13;
        k < len L by A14,NAT_1:13;
        then consider G1,H1 being Element of QC-WFF(Al) such that
A18:    L.k = G1 and
A19:    L.j = H1 and
A20:    G1 is_immediate_constituent_of H1 by A7,A17,SUBSTUT2:def 5;
        consider p1 such that
A21:    QuantNbr(q) <= QuantNbr(p1) and
A22:    p1 = L.k and
A23:    CX |- p1 iff JH,valH(Al) |= p1 by A12,A14,A17,NAT_1:13;
A24:    ex F3 st ( F3 = L.j)&( F3 is_subformula_of p) by A7,A13,A14,SUBSTUT2:27
        ;
        reconsider s = H1 as Element of CQC-WFF(Al)
        by A7,A13,A14,A19,SUBSTUT2:28;
        take s;
A25:    now
          assume
A26:      s = 'not' p1;
          then
A27:      QuantNbr(q) <= QuantNbr(s) by A21,CQC_SIM1:16;
CX |- s iff JH,valH(Al) |= s by A3,A23,A26,Def1,HENMODEL:def 2,VALUAT_1:17;
          hence thesis by A19,A27;
        end;
A28:    QuantNbr(s) <= n+1 by A6,A19,A24,SUBSTUT2:30;
A29:    now
          given F1 such that
A30:      s = p1 '&' F1;
          reconsider F1 as Element of CQC-WFF(Al) by A30,CQC_LANG:9;
A31:      QuantNbr(s) = QuantNbr(p1) + QuantNbr(F1) by A30,CQC_SIM1:17;
          then 1+QuantNbr(F1) <= QuantNbr(s) by A8,A21,XREAL_1:6;
          then 1+QuantNbr(F1) <= n+1 by A28,XXREAL_0:2;
          then QuantNbr(F1)+1+(-1) <= n+1+(-1) by XREAL_1:6;
          then CX |- F1 iff JH,valH(Al) |= F1 by A1,A3,A4;
          then
A32:      CX |- s iff JH,valH(Al) |= s by A23,A30,Th6,VALUAT_1:18;
          QuantNbr(p1) <= QuantNbr(s) by A31,NAT_1:11;
          then QuantNbr(q) <= QuantNbr(s) by A21,XXREAL_0:2;
          hence thesis by A19,A32;
        end;
A33:    now
          given F1 such that
A34:      s = F1 '&' p1;
          reconsider F1 as Element of CQC-WFF(Al) by A34,CQC_LANG:9;
A35:      QuantNbr(s) = QuantNbr(p1) + QuantNbr(F1) by A34,CQC_SIM1:17;
          then 1+QuantNbr(F1) <= QuantNbr(s) by A8,A21,XREAL_1:6;
          then 1+QuantNbr(F1) <= n+1 by A28,XXREAL_0:2;
          then QuantNbr(F1)+1+(-1) <= n+1+(-1) by XREAL_1:6;
          then CX |- F1 iff JH,valH(Al) |= F1 by A1,A3,A4;
          then
A36:      CX |- s iff JH,valH(Al) |= s by A23,A34,Th6,VALUAT_1:18;
          QuantNbr(p1) <= QuantNbr(s) by A35,NAT_1:11;
          then QuantNbr(q) <= QuantNbr(s) by A21,XXREAL_0:2;
          hence thesis by A19,A36;
        end;
        now
          given x such that
A37:      s = All(x,p1);
A38:      QuantNbr(s) = QuantNbr(p1) + 1 by A37,CQC_SIM1:18;
          then QuantNbr(p1) < n+1 by A28,NAT_1:13;
          then QuantNbr(p1) <= n by NAT_1:13;
          then
A39:      QuantNbr('not' p1) <= n by CQC_SIM1:16;
A40:      QuantNbr(q) <= QuantNbr(s) by A21,A38,NAT_1:13;
A41:      now
            assume JH,valH(Al) |= Ex(x,'not' p1);
            then consider y such that
A42:        JH,valH(Al) |= ('not' p1).(x,y) by Th10;
            QuantNbr(('not' p1).(x,y)) <= n by A39,Th14;
            then CX |- ('not' p1).(x,y) by A1,A3,A4,A42;
            hence CX |- Ex(x,'not' p1) by A4,Th3;
          end;
          now
            assume CX |- Ex(x,'not' p1);
            then consider y such that
A43:        CX |- ('not' p1).(x,y) by A4,Th3;
            QuantNbr(('not' p1).(x,y)) <= n by A39,Th14;
            then JH,valH(Al) |= ('not' p1).(x,y) by A1,A3,A4,A43;
            hence JH,valH(Al) |= Ex(x,'not' p1) by Th10;
          end;
          then JH,valH(Al) |= 'not' Ex(x,'not' p1) iff
          CX |- 'not' Ex(x,'not' p1 )
          by A3,A41,Def1,HENMODEL:def 2,VALUAT_1:17;
          then JH,valH(Al) |= s iff CX |- s by A37,Th11,Th12;
          hence thesis by A19,A40;
        end;
        hence thesis by A18,A20,A22,A25,A29,A33,QC_LANG2:def 19;
      end;
      hence thesis by A15;
    end;
    for k holds P[k] from NAT_1:sch 1(A10,A11);
    then ex p1 st ( p1 = L.(len L))&( QuantNbr(q) <= QuantNbr(p1))&(
    CX |- p1 iff JH,valH(Al) |= p1) by A9;
    hence thesis by A7,SUBSTUT2:def 5;
  end;
  hence thesis by A2,A5,NAT_1:8;
end;

:: Ebb et al, Chapter V, Henkin's Theorem 1.10

theorem Th17:
  for p holds (CX is negation_faithful & CX is with_examples
  implies (JH,valH(Al) |= p iff CX |- p))
proof
  defpred P[Element of CQC-WFF(Al)] means
  CX is negation_faithful & CX is with_examples
  implies (JH,valH(Al) |= $1 iff CX |- $1);
A1: for p st QuantNbr(p) <= 0 holds P[p] by Th8;
A2: for k st for p st QuantNbr(p) <= k holds P[p] holds
  for p st QuantNbr(p) <= k+1 holds P[p] by Th16;
  thus for p holds P[p] from SUBSTUT2:sch 2(A1,A2);
end;

begin :: Satisfiability of Consistent Sets of Formulas with Finitely Many Free
:: Variables

theorem Th18:
  Al is countable implies
  QC-WFF(Al) is countable
proof
  assume A1: Al is countable;
  QC-WFF(Al) is Al-closed by QC_LANG1:def 11;
  then
A2: QC-WFF(Al) is Subset of [: NAT, QC-symbols(Al):]* by QC_LANG1:def 10;
  [:NAT,QC-symbols(Al):] is non empty set &
  [:NAT,QC-symbols(Al):] is countable by QC_LANG1:5,A1;
  then [:NAT,QC-symbols(Al):]* is countable by CARD_4:13;
  hence thesis by A2;
end;

definition
  let Al;
  func ExCl(Al) -> Subset of CQC-WFF(Al) means
  :Def3:
  a in it iff ex x,p st a = Ex(x,p);
  existence
  proof
    defpred P[set] means ex x,p st $1 = Ex(x,p);
    consider X being set such that
A1: for a holds a in X iff a in CQC-WFF(Al) & P[a] from XBOOLE_0:sch 1;
    for a st a in X holds a in CQC-WFF(Al) by A1;
    then reconsider X as Subset of CQC-WFF(Al) by TARSKI:def 3;
    take X;
    thus thesis by A1;
  end;
  uniqueness
  proof
    defpred P[set] means ex x,p st $1 = Ex(x,p);
    let A1,A2 be Subset of CQC-WFF(Al) such that
A2: a in A1 iff P[a] and
A3: a in A2 iff P[a];
    now
      let a;
      a in A1 iff P[a] by A2;
      hence a in A1 iff a in A2 by A3;
    end;
    hence thesis by TARSKI:1;
  end;
end;

theorem Th19:
  Al is countable implies
  CQC-WFF(Al) is countable
proof
    assume A1: Al is countable;
    QC-WFF(Al) is countable by Th18, A1;
    hence thesis;
end;

theorem Th20:
  Al is countable implies
  ExCl(Al) is non empty & ExCl(Al) is countable
proof
  assume A1: Al is countable;
  set x =the  bound_QC-variable of Al,p =the  Element of CQC-WFF(Al);
  set a = Ex(x,p);
  a in ExCl(Al) by Def3;
  hence ExCl(Al) is non empty;
  CQC-WFF(Al) is countable by Th19, A1;
  hence thesis;
end;

Lm1: for A being non empty set st A is countable holds
ex f being Function st dom f = NAT & A = rng f
proof
  let A be non empty set such that
A1: A is countable;
  A c= A;
  then consider F being Function of NAT,A such that
A2: A = rng F by A1,SUPINF_2:def 8;
  dom F = NAT by FUNCT_2:def 1;
  hence thesis by A2;
end;

definition
  let Al;
  let p be Element of QC-WFF(Al) such that
A1: p is existential;
  func Ex-bound_in p -> bound_QC-variable of Al means
  :Def4:
  ex q being Element of QC-WFF(Al) st p = Ex(it,q);
  existence by A1,QC_LANG2:def 13;
  uniqueness by QC_LANG2:13;
end;

definition
  let Al;
  let p be Element of CQC-WFF(Al) such that
B1: p is existential;
  func Ex-the_scope_of p -> Element of CQC-WFF(Al) means
  :Def5:
  ex x st p = Ex(x,it);
  existence
  proof
    consider x,F1 such that
A1: p = Ex(x,F1) by B1,QC_LANG2:def 13;
    p = 'not' All(x,'not' F1) by A1,QC_LANG2:def 5;
    then All(x,'not' F1) is Element of CQC-WFF(Al) by CQC_LANG:8;
    then
A2: 'not' F1 is Element of CQC-WFF(Al) by CQC_LANG:13;
    take F1;
    thus thesis by A1,A2,CQC_LANG:8;
  end;
  uniqueness by QC_LANG2:13;
end;

definition
  let Al;
  let F be Function of NAT,CQC-WFF(Al),a be Element of NAT;
  func bound_in(F,a) -> bound_QC-variable of Al means
  :Def6:
  p = F.a implies it = Ex-bound_in p;
  existence
  proof
    reconsider p = F.a as Element of CQC-WFF(Al);
    take Ex-bound_in p;
    thus thesis;
  end;
  uniqueness
  proof
    let x1,x2 such that
A1: p = F.a implies x1 = Ex-bound_in p and
A2: p = F.a implies x2 = Ex-bound_in p;
    reconsider q = F.a as Element of CQC-WFF(Al);
    x1 = Ex-bound_in q by A1;
    hence thesis by A2;
  end;
end;

definition
  let Al;
  let F be Function of NAT,CQC-WFF(Al),a be Element of NAT;
  func the_scope_of(F,a) -> Element of CQC-WFF(Al) means
  :Def7:
  p = F.a implies it = Ex-the_scope_of p;
  existence
  proof
    reconsider p = F.a as Element of CQC-WFF(Al);
    take Ex-the_scope_of p;
    thus thesis;
  end;
  uniqueness
  proof
    let q1,q2 be Element of CQC-WFF(Al) such that
A1: p = F.a implies q1 = Ex-the_scope_of p and
A2: p = F.a implies q2 = Ex-the_scope_of p;
    reconsider q = F.a as Element of CQC-WFF(Al);
    q1 = Ex-the_scope_of q by A1;
    hence thesis by A2;
  end;
end;

definition
  let Al,X;
  func still_not-bound_in X -> Subset of bound_QC-variables(Al) equals
  union {still_not-bound_in p : p in X};
  coherence
  proof
    set Y = union {still_not-bound_in p : p in X};
    now
      let a;
      assume a in Y;
      then consider b such that
A1:   a in b & b in {still_not-bound_in p : p in X} by TARSKI:def 4;
      ex p st ( b = still_not-bound_in p)&( p in X) by A1;
      hence a in bound_QC-variables(Al) by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th21:
  p in X implies X |- p
proof
  assume
A1: p in X;
  now
    let a;
    assume a in rng <*p*>;
    then a in {p} by FINSEQ_1:38;
    hence a in X by A1,TARSKI:def 1;
  end;
  then
A2: rng <*p*> c= X by TARSKI:def 3;
  |- <*>CQC-WFF(Al)^<*p*>^<*p*> by CALCUL_2:21;
  then |- <*p*>^<*p*> by FINSEQ_1:34;
  hence thesis by A2,HENMODEL:def 1;
end;

theorem Th22:
  Ex-bound_in Ex(x,p) = x & Ex-the_scope_of Ex(x,p) = p
proof
  Ex(x,p) is existential by QC_LANG2:def 13;
  hence thesis by Def4,Def5;
end;

theorem Th23:
  X |- VERUM(Al)
proof
  set f = <*>CQC-WFF(Al);
A1: rng f c= X by XBOOLE_1:2;
  |- f^<*VERUM(Al)*> by HENMODEL:15;
  hence thesis by A1,HENMODEL:def 1;
end;

theorem Th24:
  X |- 'not' VERUM(Al) iff X is Inconsistent
proof
  thus X |- 'not' VERUM(Al) implies X is Inconsistent
  proof
    assume
A1: X |- 'not' VERUM(Al);
    X |- VERUM(Al) by Th23;
    hence thesis by A1,HENMODEL:def 2;
  end;
  thus thesis by HENMODEL:6;
end;

reserve C,D for Element of [:CQC-WFF(Al),bool bound_QC-variables(Al):];
reserve K,L for Subset of bound_QC-variables(Al);

theorem Th25:
  for f,g being FinSequence of CQC-WFF(Al) st 0 < len f & |- f^<*p*> holds
  |- Ant(f)^g^<*Suc(f)*>^<*p*>
proof
  let f,g be FinSequence of CQC-WFF(Al) such that
A1: 0 < len f and
A2: |- f^<*p*>;
  f is_Subsequence_of Ant(f)^g^<*Suc(f)*> by A1,CALCUL_1:13;
  then Ant(f^<*p*>) is_Subsequence_of Ant(f)^g^<*Suc(f)*> by CALCUL_1:5;
  then
A3: Ant(f^<*p*>) is_Subsequence_of Ant(Ant(f)^g^<*Suc(f)*>^<*p*>)
  by CALCUL_1:5;
  Suc(f^<*p*>) = p by CALCUL_1:5;
  then Suc(f^<*p*>) = Suc(Ant(f)^g^<*Suc(f)*>^<*p*>) by CALCUL_1:5;
  hence thesis by A2,A3,CALCUL_1:36;
end;

theorem Th26:
  still_not-bound_in {p} = still_not-bound_in p
proof
A1: now
    let a;
    assume a in still_not-bound_in {p};
    then consider b such that
A2: a in b & b in {still_not-bound_in q : q in {p}} by TARSKI:def 4;
    ex q st ( b = still_not-bound_in q)&( q in {p}) by A2;
    hence a in still_not-bound_in p by A2,TARSKI:def 1;
  end;
  now
    let a such that
A3: a in still_not-bound_in p;
    set b = still_not-bound_in p;
    p in {p} by TARSKI:def 1;
    then b in {still_not-bound_in q : q in {p}};
    hence a in still_not-bound_in {p} by A3,TARSKI:def 4;
  end;
  hence thesis by A1,TARSKI:1;
end;

theorem Th27:
  still_not-bound_in (X \/ Y) = still_not-bound_in X \/ still_not-bound_in Y
proof
  thus still_not-bound_in (X \/ Y) c=
  still_not-bound_in X \/ still_not-bound_in Y
  proof
    set A = {still_not-bound_in p : p in X \/ Y};
    let b;
    assume b in still_not-bound_in (X \/ Y);
    then consider a such that
A1: b in a and
A2: a in A by TARSKI:def 4;
    consider p such that
A3: a = still_not-bound_in p and
A4: p in X \/ Y by A2;
A5: now
      assume p in X;
      then a in {still_not-bound_in q : q in X} by A3;
      then
A6:   b in union {still_not-bound_in q : q in X} by A1,TARSKI:def 4;
      still_not-bound_in X c= still_not-bound_in X \/ still_not-bound_in Y
      by XBOOLE_1:7;
      hence thesis by A6;
    end;
    now
      assume p in Y;
      then a in {still_not-bound_in q : q in Y} by A3;
      then
A7:   b in union {still_not-bound_in q : q in Y} by A1,TARSKI:def 4;
      still_not-bound_in Y c= still_not-bound_in X \/ still_not-bound_in Y
      by XBOOLE_1:7;
      hence thesis by A7;
    end;
    hence thesis by A4,A5,XBOOLE_0:def 3;
  end;
  thus still_not-bound_in X \/ still_not-bound_in Y c=
  still_not-bound_in (X \/ Y)
  proof
    let b such that
A8: b in still_not-bound_in X \/ still_not-bound_in Y;
A9: now
      assume b in still_not-bound_in X;
      then consider a such that
A10:  b in a & a in {still_not-bound_in p : p in X} by TARSKI:def 4;
A11:  ex p st ( a = still_not-bound_in p)&( p in X) by A10;
      X c= X \/ Y by XBOOLE_1:7;
      then a in {still_not-bound_in q : q in X \/ Y} by A11;
      hence thesis by A10,TARSKI:def 4;
    end;
    now
      assume b in still_not-bound_in Y;
      then consider a such that
A12:  b in a & a in {still_not-bound_in p : p in Y} by TARSKI:def 4;
A13:  ex p st ( a = still_not-bound_in p)&( p in Y) by A12;
      Y c= X \/ Y by XBOOLE_1:7;
      then a in {still_not-bound_in q : q in X \/ Y} by A13;
      hence thesis by A12,TARSKI:def 4;
    end;
    hence thesis by A8,A9,XBOOLE_0:def 3;
  end;
end;

theorem Th28:
  for A being Subset of bound_QC-variables(Al) st A is finite holds
  ex x st not x in A
proof
  let A be Subset of bound_QC-variables(Al);
  A1: not bound_QC-variables(Al) is finite by CALCUL_1:64;
  assume A is finite;
  then not (for b holds b in A iff b in bound_QC-variables(Al))
  by A1,TARSKI:1;
  then consider b such that
A2: not b in A and
A3: b in bound_QC-variables(Al);
  reconsider x = b as bound_QC-variable of Al by A3;
  take x;
  thus thesis by A2;
end;

theorem Th29:
  X c= Y implies still_not-bound_in X c= still_not-bound_in Y
proof
  set A = {still_not-bound_in p : p in X};
  assume
A1: X c= Y;
  now
    let a;
    assume a in still_not-bound_in X;
    then consider b such that
A2: a in b and
A3: b in A by TARSKI:def 4;
    ex p st ( b = still_not-bound_in p)&( p in X) by A3;
    then b in {still_not-bound_in q : q in Y} by A1;
    hence a in still_not-bound_in Y by A2,TARSKI:def 4;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th30:
  for f being FinSequence of CQC-WFF(Al) holds
  still_not-bound_in rng f = still_not-bound_in f
proof
  let f be FinSequence of CQC-WFF(Al);
  set A = {still_not-bound_in p : p in rng f};
A1: now
    let a;
    assume a in still_not-bound_in rng f;
    then consider b such that
A2: a in b and
A3: b in A by TARSKI:def 4;
    consider p such that
A4: b = still_not-bound_in p and
A5: p in rng f by A3;
    ex c st ( c in dom f)&( f.c = p) by A5,FUNCT_1:def 3;
    hence a in still_not-bound_in f by A2,A4,CALCUL_1:def 5;
  end;
  now
    let a;
    assume a in still_not-bound_in f;
    then consider i,q such that
A6: i in dom f and
A7: q = f.i and
A8: a in still_not-bound_in q by CALCUL_1:def 5;
    q in rng f by A6,A7,FUNCT_1:def 3;
    then still_not-bound_in q in A;
    hence a in still_not-bound_in rng f by A8,TARSKI:def 4;
  end;
  hence thesis by A1,TARSKI:1;
end;

:: Ebb et al, Chapter V, Lemma 2.1

theorem Th31:
  ( Al is countable &
  still_not-bound_in CX is finite ) implies
  ex CY st CX c= CY & CY is with_examples
proof
  assume A1: Al is countable;
  assume
A2: still_not-bound_in CX is finite;
  ExCl(Al) is non empty & ExCl(Al) is countable by A1,Th20;
  then consider f being Function such that
A3: dom f = NAT and
A4: ExCl(Al) = rng f by Lm1;
  reconsider f as Function of NAT,CQC-WFF(Al) by A3,A4,FUNCT_2:2;
  defpred P[Element of NAT,set,set] means
  ex K,L st K = $2`2 & L = K \/ still_not-bound_in {f.($1+1)} &
  $3 = [('not' (f.($1+1))) 'or' (the_scope_of(f,($1+1)).(bound_in(f,$1+1),
  x.(Al-one_in {t : not x.t in L}))), K \/ still_not-bound_in
  ('not' (f.($1+1))) 'or' (the_scope_of(f,($1+1)).(bound_in(f,$1+1),
  x.(Al-one_in {u : not x.u in L})))];
A5: for n for C ex D st P[n,C,D]
  proof
    let n,C;
    set K = C`2;
    ex a,b st ( a in CQC-WFF(Al))&( b in bool bound_QC-variables(Al))&(
    C = [a,b]) by ZFMISC_1:def 2;
    then reconsider K as Subset of bound_QC-variables(Al) by MCART_1:7;
    set L = K \/ still_not-bound_in {f.(n+1)};
    set D = [('not' (f.(n+1))) 'or' (the_scope_of(f,(n+1)).(bound_in(f,n+1),
    x.(Al-one_in {t : not x.t in L}))), K \/ still_not-bound_in
    ('not' (f.(n+1))) 'or' (the_scope_of(f,(n+1)).(bound_in(f,n+1),
    x.(Al-one_in {u : not x.u in L})))];
    take D;
    thus thesis;
  end;
  reconsider A = [('not' (f.0)) 'or' (the_scope_of(f,0).(bound_in(f,0),
  x.(Al-one_in {u : not x.u in still_not-bound_in (CX \/ {f.0})}))),
  still_not-bound_in (CX \/ {('not' (f.0)) 'or'
  (the_scope_of(f,0).(bound_in(f,0), x.(Al-one_in {t :
  not x.t in still_not-bound_in (CX \/ {f.0})})))})]
  as Element of [:CQC-WFF(Al),bool bound_QC-variables(Al):];
  consider h being Function of NAT,[:CQC-WFF(Al),bool bound_QC-variables(Al):]
  such that
A6: h.0 = A & for n holds P[n,h.n,h.(n+1)] from RECDEF_1:sch 2(A5);
  set CY = CX \/ {(h.n)`1 : not contradiction};
  now
    let a such that
A7: a in CY;
    now
      assume not a in CX;
      then a in {(h.n)`1 : not contradiction} by A7,XBOOLE_0:def 3;
      then consider n such that
A8:   a = (h.n)`1;
      ex c,d st ( c in CQC-WFF(Al))&( d in bool bound_QC-variables(Al))&(
      h.n = [c,d]) by ZFMISC_1:def 2;
      hence a in CQC-WFF(Al) by A8,MCART_1:7;
    end;
    hence a in CQC-WFF(Al);
  end;
  then reconsider CY as Subset of CQC-WFF(Al) by TARSKI:def 3;
A9: now
    let x,p;
    Ex(x,p) in ExCl(Al) by Def3;
    then consider a such that
A10: a in dom f and
A11: f.a = Ex(x,p) by A4,FUNCT_1:def 3;
    reconsider a as Element of NAT by A10;
    reconsider r9 = f.a as Element of CQC-WFF(Al);
A12: Ex-bound_in r9 = x by A11,Th22;
A13: Ex-the_scope_of r9 = p by A11,Th22;
A14: bound_in(f,a) = x by A12,Def6;
A15: the_scope_of(f,a) = p by A13,Def7;
A16: (h.a)`1 in {(h.n)`1 : not contradiction};
A17: {(h.n)`1 : not contradiction} c= CY by XBOOLE_1:7;
A18: now
      assume
A19:  a = 0;
      take y = x.(Al-one_in {t:not x.t in still_not-bound_in (CX \/ {r9})});
      (h.a)`1 = 'not' r9 'or' (the_scope_of(f,a).(bound_in(f,a),y))
      by A6,A19,MCART_1:7;
      hence CY |- 'not' Ex(x,p) 'or' (p.(x,y)) by A11,A14,A15,A16,A17,Th21;
    end;
    now
      assume a <> 0;
      then consider m being natural number such that
A20:  a = m+1 by NAT_1:6;
      reconsider m as Element of NAT by ORDINAL1:def 12;
A21:  ex K,L st K = (h.m)`2 & L = K \/ still_not-bound_in {r9} &
      h.a = [('not' r9) 'or' (the_scope_of(f,a).(bound_in(f,a),
      x.(Al-one_in {t : not x.t in L}))), K \/ still_not-bound_in
      ('not' r9) 'or' (the_scope_of(f,a).(bound_in(f,a),
      x.(Al-one_in {u : not x.u in L})))] by A6,A20;
      set K = (h.m)`2;
      set L = still_not-bound_in ({r9}) \/ K;
      take y = x.(Al-one_in {t : not x.t in L});
      (h.a)`1 = 'not' r9 'or' (the_scope_of(f,a).(bound_in(f,a),y))
      by A21,MCART_1:7;
      hence CY |- ('not' Ex(x,p)) 'or' (p.(x,y)) by A11,A14,A15,A16,A17,Th21;
    end;
    hence ex y st CY |- 'not' Ex(x,p) 'or' (p.(x,y)) by A18;
  end;
  deffunc G(set) = CX \/ {(h.n)`1 : n in $1};
  consider F being Function such that
A22: dom F = NAT & for a st a in NAT holds F.a = G(a) from FUNCT_1:sch 3;
A23: CY c= union rng F
  proof
    let a;
    assume
A24: a in CY;
A25: now
      assume
A26:  a in CX;
A27:  F.0 = CX \/ {(h.n)`1 : n in 0} by A22;
      now
        let b;
        assume b in {(h.n)`1 : n in 0};
        then ex n st ( b = (h.n)`1)&( n in 0);
        hence contradiction;
      end;
      then
A28:  {(h.n)`1 : n in 0} = {} by XBOOLE_0:def 1;
      F.0 in rng F by A22,FUNCT_1:3;
      hence thesis by A26,A27,A28,TARSKI:def 4;
    end;
    now
      assume a in {(h.n)`1 : not contradiction};
      then consider n such that
A29:  a = (h.n)`1;
      n < n+1 by NAT_1:13;
      then n in n+1 by NAT_1:44;
      then
A30:  a in {(h.m)`1 : m in n+1} by A29;
      F.(n+1) = CX \/ {(h.m)`1 : m in n+1} by A22;
      then
A31:  {(h.m)`1 : m in n+1} c= F.(n+1) by XBOOLE_1:7;
      F.(n+1) in rng F by A22,FUNCT_1:3;
      hence thesis by A30,A31,TARSKI:def 4;
    end;
    hence thesis by A24,A25,XBOOLE_0:def 3;
  end;
  union rng F c= CY
  proof
    let a;
    assume a in union rng F;
    then consider b such that
A32: a in b and
A33: b in rng F by TARSKI:def 4;
    consider c such that
A34: c in dom F and
A35: F.c = b by A33,FUNCT_1:def 3;
    reconsider n = c as Element of NAT by A22,A34;
A36: a in CX \/ {(h.m)`1 : m in n} by A22,A32,A35;
A37: now
      assume
A38:  a in CX;
      CX c= CY by XBOOLE_1:7;
      hence thesis by A38;
    end;
    now
      assume a in {(h.m)`1 : m in n};
      then ex m st ( a = (h.m)`1)&( m in n);
      then
A39:  a in {(h.i)`1 : not contradiction};
      {(h.i)`1 : not contradiction} c= CY by XBOOLE_1:7;
      hence thesis by A39;
    end;
    hence thesis by A36,A37,XBOOLE_0:def 3;
  end;
  then
A40: CY = union rng F by A23,XBOOLE_0:def 10;
A41: for n,m st m in dom F & n in dom F & n < m holds F.n c= F.m
  proof
    let n,m such that
    m in dom F and n in dom F and
A42: n < m;
A43: F.n = CX \/ {(h.i)`1 : i in n} by A22;
A44: F.m = CX \/ {(h.i)`1 : i in m} by A22;
    now
      let a such that
A45:  a in F.n;
A46:  now
        assume
A47:    a in CX;
        CX c= F.m by A44,XBOOLE_1:7;
        hence a in F.m by A47;
      end;
      now
        assume a in {(h.i)`1 : i in n};
        then consider i such that
A48:    (h.i)`1 = a and
A49:    i in n;
        i < n by A49,NAT_1:44;
        then i < m by A42,XXREAL_0:2;
        then i in m by NAT_1:44;
        then
A50:    a in {(h.j)`1 : j in m} by A48;
        {(h.j)`1 : j in m} c= F.m by A44,XBOOLE_1:7;
        hence a in F.m by A50;
      end;
      hence a in F.m by A43,A45,A46,XBOOLE_0:def 3;
    end;
    hence thesis by TARSKI:def 3;
  end;
  rng F c= bool CQC-WFF(Al)
  proof
    let a;
    assume a in rng F;
    then consider b such that
A51: b in dom F and
A52: F.b = a by FUNCT_1:def 3;
    reconsider b as Element of NAT by A22,A51;
A53: F.b = CX \/ {(h.i)`1 : i in b} by A22;
    now
      let c;
      assume c in {(h.i)`1 : i in b};
      then ex i st ( (h.i)`1 = c)&( i in b);
      hence c in CQC-WFF(Al) by MCART_1:10;
    end;
    then {(h.i)`1 : i in b} c= CQC-WFF(Al) by TARSKI:def 3;
    then F.b c= CQC-WFF(Al) by A53,XBOOLE_1:8;
    hence thesis by A52;
  end;
  then reconsider F as Function of NAT,bool CQC-WFF(Al) by A22,FUNCT_2:2;
A54: for n holds F.(n+1) = F.n \/ {(h.n)`1}
  proof
    let n;
    now
      let a;
      assume a in {(h.i)`1 : i in n+1};
      then consider j such that
A55:  a = (h.j)`1 and
A56:  j in n+1;
      j < n+1 by A56,NAT_1:44;
      then
A57:  j+1 <= n+1 by NAT_1:13;
A58:  now
        assume j+1 = n+1;
        then
A59:    a in {(h.n)`1} by A55,TARSKI:def 1;
        {(h.n)`1} c= {(h.i)`1 : i in n} \/ {(h.n)`1} by XBOOLE_1:7;
        hence a in {(h.i)`1 : i in n} \/ {(h.n)`1} by A59;
      end;
      now
        assume j+1 <= n;
        then j < n by NAT_1:13;
        then j in n by NAT_1:44;
        then
A60:    a in {(h.k)`1 : k in n} by A55;
        {(h.k)`1 : k in n} c= {(h.i)`1 : i in n} \/ {(h.n)`1} by XBOOLE_1:7;
        hence a in {(h.i)`1 : i in n} \/ {(h.n)`1} by A60;
      end;
      hence a in {(h.i)`1 : i in n} \/ {(h.n)`1} by A57,A58,NAT_1:8;
    end;
    then
A61: {(h.k)`1 : k in n+1} c= {(h.i)`1 : i in n} \/ {(h.n)`1} by TARSKI:def 3;
    now
      let a;
      assume
A62:  a in {(h.i)`1 : i in n} \/ {(h.n)`1};
A63:  now
        assume a in {(h.i)`1 : i in n};
        then consider j such that
A64:    (h.j)`1 = a and
A65:    j in n;
A66:    n <= n+1 by NAT_1:11;
        j < n by A65,NAT_1:44;
        then j < n+1 by A66,XXREAL_0:2;
        then j in n+1 by NAT_1:44;
        hence a in {(h.i)`1 : i in n+1} by A64;
      end;
      now
        assume a in {(h.n)`1};
        then
A67:    a = (h.n)`1 by TARSKI:def 1;
        n < n+1 by NAT_1:13;
        then n in n+1 by NAT_1:44;
        hence a in {(h.i)`1 : i in n+1} by A67;
      end;
      hence a in {(h.i)`1 : i in n+1} by A62,A63,XBOOLE_0:def 3;
    end;
    then {(h.i)`1 : i in n} \/ {(h.n)`1} c= {(h.k)`1 : k in n+1}
    by TARSKI:def 3;
    then {(h.i)`1 : i in n} \/ {(h.n)`1} = {(h.k)`1 : k in n+1}
    by A61,XBOOLE_0:def 10;
    then F.(n+1) = CX \/ ({(h.k)`1 : k in n} \/ {(h.n)`1}) by A22;
    then F.(n+1) = CX \/ {(h.k)`1 : k in n} \/ {(h.n)`1} by XBOOLE_1:4;
    hence thesis by A22;
  end;
  defpred P[Element of NAT] means (h.$1)`2 is finite &
  (h.$1)`2 is Subset of bound_QC-variables(Al);
A68: P[0]
  proof
A69: (h.0)`2 = still_not-bound_in (CX \/ {('not' (f.0)) 'or'
    (the_scope_of(f,0).(bound_in(f,0), x.(Al-one_in {t :
    not x.t in still_not-bound_in (CX \/ {f.0})})))}) by A6,MCART_1:7;
    reconsider s = ('not' (f.0)) 'or'
    (the_scope_of(f,0).(bound_in(f,0), x.(Al-one_in {t :
    not x.t in still_not-bound_in (CX \/ {f.0})})))
    as Element of CQC-WFF(Al);
    still_not-bound_in s is finite by CQC_SIM1:19;
    then still_not-bound_in {s} is finite by Th26;
    then still_not-bound_in {s} \/ still_not-bound_in CX is finite by A2;
    hence thesis by A69,Th27;
  end;
A70: for k st P[k] holds P[k+1]
  proof
    let k such that
A71: P[k];
A72: ex K,L st K = (h.k)`2 & L = K \/ still_not-bound_in {f.(k+1)} &
    h.(k+1) = [('not' (f.(k+1))) 'or' (the_scope_of(f,k+1).(bound_in(f,k+1),
    x.(Al-one_in {t : not x.t in L}))), K \/ still_not-bound_in
    ('not' (f.(k+1))) 'or' (the_scope_of(f,k+1).(bound_in(f,k+1),
    x.(Al-one_in {u : not x.u in L})))] by A6;
    set K = (h.k)`2;
    reconsider K as Subset of bound_QC-variables(Al) by A71;
    set L = K \/ still_not-bound_in {f.(k+1)};
    set s = ('not' (f.(k+1))) 'or' (the_scope_of(f,(k+1)).
    (bound_in(f,k+1),x.(Al-one_in {t : not x.t in L})));
    still_not-bound_in s is finite by CQC_SIM1:19;
    hence thesis by A71,A72,MCART_1:7;
  end;
A73: for k holds P[k] from NAT_1:sch 1(A68,A70);
  defpred P[Element of NAT] means still_not-bound_in (F.($1+1)) c= (h.$1)`2 &
  not x.(Al-one_in {t : not x.t in still_not-bound_in
  {f.($1+1)} \/ (h.$1)`2}) in still_not-bound_in (F.($1+1) \/ {f.($1+1)});
A74: for k holds still_not-bound_in (F.(k+1)) c= (h.k)`2 & not x.(Al-one_in {t:
  not x.t in still_not-bound_in {f.(k+1)} \/ (h.k)`2})
  in still_not-bound_in (F.(k+1) \/ {f.(k+1)})
  proof
A75: P[0]
    proof
      set r = ('not' (f.0)) 'or'
      (the_scope_of(f,0).(bound_in(f,0), x.(Al-one_in {t :
      not x.t in still_not-bound_in (CX \/ {f.0})})));
      set A1 = {r};
      reconsider s = f.1 as Element of CQC-WFF(Al);
A76:  (h.0)`2 = still_not-bound_in (CX \/ A1) by A6,MCART_1:7;
      reconsider B = (h.0)`2 as Subset of bound_QC-variables(Al)
      by A6,MCART_1:7;
      reconsider C = still_not-bound_in {s} \/ B as Element of
      bool bound_QC-variables(Al);
      still_not-bound_in s is finite by CQC_SIM1:19;
      then still_not-bound_in {s} is finite by Th26;
      then consider x such that
A77:  not x in C by A68,Th28;
      consider u such that
A78:  x.u = x by QC_LANG3:30;
      u in {t : not x.t in C} by A77,A78;
      then reconsider A = {t : not x.t in C} as non empty set;
      now
        let a;
        assume a in A;
        then ex t st ( a = t)&( not x.t in C);
        hence a in QC-symbols(Al);
      end;
      then reconsider A={t:not x.t in C} as non empty Subset of QC-symbols(Al)
      by TARSKI:def 3;
      set u = Al-one_in A;
      u = the Element of A by QC_LANG1:def 41;
      then u in A;
      then
A79:  ex t st ( t = u)&( not x.t in C);
A80:  F.0 = CX \/ {(h.n)`1 : n in 0} by A22;
      now
        let b;
        assume b in {(h.n)`1 : n in 0};
        then ex n st ( b = (h.n)`1)&( n in 0);
        hence contradiction;
      end;
      then
A81:  {(h.n)`1 : n in 0} = {} by XBOOLE_0:def 1;
      (h.0)`1 = r by A6,MCART_1:7;
      then F.(0+1) = CX \/ {r} by A54,A80,A81;
      hence thesis by A76,A79,Th27;
    end;
A82: for k st P[k] holds P[k+1]
    proof
      let k such that
A83:  P[k];
      reconsider s = f.(k+2) as Element of CQC-WFF(Al);
A84:  ex K,L st K = (h.k)`2 & L = K \/ still_not-bound_in {f.(k+1)} &
      h.(k+1) = [('not' (f.(k+1))) 'or' (the_scope_of(f,(k+1)).
      (bound_in(f,k+1),x.(Al-one_in {t : not x.t in L}))),
      K \/ still_not-bound_in
      ('not' (f.(k+1))) 'or' (the_scope_of(f,k+1).(bound_in(f,k+1),
      x.(Al-one_in {u : not x.u in L})))] by A6;
      set K = (h.k)`2;
      reconsider K as Subset of bound_QC-variables(Al) by A73;
      set L = K \/ still_not-bound_in {f.(k+1)};
      set r = ('not' (f.(k+1))) 'or' (the_scope_of(f,(k+1)).
      (bound_in(f,k+1),x.(Al-one_in {t : not x.t in L})));
A85:  (h.(k+1))`1 = r by A84,MCART_1:7;
A86:  (h.(k+1))`2 = K \/ still_not-bound_in r by A84,MCART_1:7;
      reconsider B = (h.(k+1))`2 as Subset of bound_QC-variables(Al) by A84,
MCART_1:7;
      reconsider C = still_not-bound_in {s} \/ B as Element of
      bool bound_QC-variables(Al);
      still_not-bound_in s is finite by CQC_SIM1:19;
      then
A87:  still_not-bound_in {s} is finite by Th26;
      (h.(k+1))`2 is finite by A73;
      then consider x such that
A88:  not x in C by A87,Th28;
      consider u such that
A89:  x.u = x by QC_LANG3:30;
      u in {t : not x.t in still_not-bound_in {s} \/ B} by A88,A89;
      then reconsider A = {t : not x.t in still_not-bound_in {s} \/ B}
      as non empty set;
      now
        let a;
        assume a in A;
        then ex t st ( a = t)&( not x.t in C);
        hence a in QC-symbols(Al);
      end;
      then reconsider A = {t : not x.t in still_not-bound_in {s} \/ B}
      as non empty Subset of QC-symbols(Al) by TARSKI:def 3;
      set u = Al-one_in A;
      u = the Element of A by QC_LANG1:def 41;
      then u in A;
      then
A90:  ex t st ( t = u)&( not x.t in C);
      then
A91:  not x.u in still_not-bound_in {s} by XBOOLE_0:def 3;
      still_not-bound_in (F.(k+1)) \/ still_not-bound_in r c= B
      by A83,A86,XBOOLE_1:9;
      then still_not-bound_in (F.(k+1)) \/ still_not-bound_in {r} c= B by Th26;
      then
A92:  still_not-bound_in (F.(k+1) \/ {r}) c= B by Th27;
      then still_not-bound_in (F.(k+1+1)) c= B by A54,A85;
      then not x.u in still_not-bound_in (F.(k+1+1)) by A90,XBOOLE_0:def 3;
      then not x.u in still_not-bound_in (F.(k+1+1)) \/
      still_not-bound_in {s} by A91,XBOOLE_0:def 3;
      hence thesis by A54,A85,A92,Th27;
    end;
    for k holds P[k] from NAT_1:sch 1(A75,A82);
    hence thesis;
  end;
  defpred P[Element of NAT] means F.$1 is Consistent;
  now
    let a;
    assume a in {(h.i)`1 : i in 0};
    then ex j st ( a = (h.j)`1)&( j in 0);
    hence contradiction;
  end;
  then {(h.i)`1 : i in 0} = {} by XBOOLE_0:def 1;
  then
A93: F.0 = CX \/ {} by A22;
  then
A94: P[0];
A95: for k st P[k] holds P[k+1]
  proof
    let k such that
A96: P[k];
    ex c,d st ( c in CQC-WFF(Al))&( d in bool bound_QC-variables(Al))&(
    h.k = [c,d]) by ZFMISC_1:def 2;
    then reconsider r = (h.k)`1 as Element of CQC-WFF(Al) by MCART_1:7;
    now
      assume F.(k+1) is Inconsistent;
      then F.(k+1) |- 'not' VERUM(Al) by HENMODEL:6;
      then F.k \/ {r} |- 'not' VERUM(Al) by A54;
      then consider f1 being FinSequence of CQC-WFF(Al) such that
A97:  rng f1 c= F.k and
A98:  |- f1^<*r*>^<*'not' VERUM(Al)*> by HENMODEL:8;
A99:  |- f1^<*'not' (f.k)*>^<*'not' (f.k)*> by CALCUL_2:21;
A100:  now
        assume
A101:   k = 0;
        then
A102:   r = 'not' (f.0) 'or' (the_scope_of(f,0).(bound_in(f,0),
        x.(Al-one_in {t : not x.t in still_not-bound_in (CX \/ {f.0})})))
        by A6,MCART_1:7;
        reconsider s = the_scope_of(f,0).(bound_in(f,0),
        x.(Al-one_in {t : not x.t in still_not-bound_in (CX \/ {f.0})}))
        as Element of CQC-WFF(Al);
A103:   |- (f1^<*'not' (f.k)*>)^<*('not' (f.k)) 'or' s*> by A99,CALCUL_1:51;
        0+1 <= len (f1^<*r*>) by CALCUL_1:10;
        then |- Ant(f1^<*r*>)^<*'not' (f.k)*>^<*Suc(f1^<*r*>)*>^<*'not'
        VERUM(Al)*> by A98,Th25;
        then |- f1^<*'not' (f.k)*>^<*Suc(f1^<*r*>)*>^<*'not' VERUM(Al)*>
        by CALCUL_1:5;
        then |- (f1^<*'not' (f.k)*>)^<*r*>^<*'not' VERUM(Al)*> by CALCUL_1:5;
        then
A104:   |- f1^<*'not' (f.k)*>^<*'not' VERUM(Al)*>
        by A101,A102,A103,CALCUL_2:24;
        |- f1^<*s*>^<*s*> by CALCUL_2:21;
        then
A105:   |- f1^<*s*>^<*('not' (f.k)) 'or' s*> by CALCUL_1:52;
        0+1 <= len (f1^<*r*>) by CALCUL_1:10;
        then |- Ant(f1^<*r*>)^<*s*>^<*Suc(f1^<*r*>)*>^<*'not' VERUM(Al)*>
        by A98,Th25;
        then |- f1^<*s*>^<*Suc(f1^<*r*>)*>^<*'not' VERUM(Al)*> by CALCUL_1:5;
        then |- (f1^<*s*>)^<*r*>^<*'not' VERUM(Al)*> by CALCUL_1:5;
        then
A106:   |- f1^<*s*>^<*'not' VERUM(Al)*> by A101,A102,A105,CALCUL_2:24;
        reconsider r1 = f.0 as Element of CQC-WFF(Al);
        set C = still_not-bound_in (CX \/ {r1});
        still_not-bound_in r1 is finite by CQC_SIM1:19;
        then still_not-bound_in {r1} is finite by Th26;
        then still_not-bound_in {r1} \/ still_not-bound_in CX is finite by A2;
        then C is finite by Th27;
        then consider x such that
A107:   not x in C by Th28;
        consider u such that
A108:   x.u = x by QC_LANG3:30;
        u in {t : not x.t in C} by A107,A108;
        then reconsider A = {t : not x.t in C} as non empty set;
        now
          let a;
          assume a in A;
          then ex t st ( a = t)&( not x.t in C);
          hence a in QC-symbols(Al);
        end;
        then reconsider A = {t : not x.t in C} as
             non empty Subset of QC-symbols(Al)
        by TARSKI:def 3;
        set u = Al-one_in A;
        u = the Element of A by QC_LANG1:def 41;
        then u in A;
        then consider t such that
A109:   t = u and
A110:   not x.t in C;
A111:   not x.t in still_not-bound_in CX \/ still_not-bound_in {r1}
        by A110,Th27;
        then
A112:   not x.t in still_not-bound_in {r1} by XBOOLE_0:def 3;
A113:   F.0 = CX \/ {(h.n)`1 : n in 0} by A22;
        now
          let b;
          assume b in {(h.n)`1 : n in 0};
          then ex n st ( b = (h.n)`1)&( n in 0);
          hence contradiction;
        end;
        then {(h.n)`1 : n in 0} = {} by XBOOLE_0:def 1;
        then still_not-bound_in rng f1 c=
        still_not-bound_in CX by A97,A101,A113,Th29;
        then not x.t in still_not-bound_in rng f1 by A111,XBOOLE_0:def 3;
        then
A114:   not x.u in still_not-bound_in f1 by A109,Th30;
        reconsider r2 = the_scope_of(f,0) as Element of CQC-WFF(Al);
        reconsider y2 = bound_in(f,0) as bound_QC-variable of Al;
        r1 in ExCl(Al) by A3,A4,FUNCT_1:3;
        then consider y1,s1 such that
A115:   r1 = Ex(y1,s1) by Def3;
A116:   s1 = Ex-the_scope_of r1 by A115,Th22;
A117:   r2 = Ex-the_scope_of r1 by Def7;
A118:   y1 = Ex-bound_in r1 by A115,Th22;
A119:   y2 = Ex-bound_in r1 by Def6;
        not x.u in still_not-bound_in r1 by A109,A112,Th26;
        then not x.u in still_not-bound_in <*r1*> by CALCUL_1:60;
        then not x.u in still_not-bound_in f1 \/ still_not-bound_in <*r1*>
        by A114,XBOOLE_0:def 3;
        then
A120:   not x.u in still_not-bound_in (f1^<*r1*>) by CALCUL_1:59;
        still_not-bound_in VERUM(Al) = {} by QC_LANG3:3;
        then not x.u in still_not-bound_in 'not' VERUM(Al) by QC_LANG3:7;
        then not x.u in still_not-bound_in <*'not' VERUM(Al)*>
        by CALCUL_1:60;
        then not x.u in still_not-bound_in (f1^<*r1*>) \/
        still_not-bound_in <*'not' VERUM(Al)*> by A120,XBOOLE_0:def 3;
        then not x.u in still_not-bound_in (f1^<*r1*>^<*'not' VERUM(Al)*>)
        by CALCUL_1:59;
        then |- f1^<*r1*>^<*'not' VERUM(Al)*> by A106,A115,A116,A117,A118,A119,
CALCUL_1:61;
        then |- f1^<*'not' VERUM(Al)*> by A101,A104,CALCUL_2:26;
        then F.k |- 'not' VERUM(Al) by A97,HENMODEL:def 1;
        hence contradiction by A93,A101,Th24;
      end;
      now
        assume k <> 0;
        then consider k1 being natural number such that
A121:   k = k1+1 by NAT_1:6;
        reconsider k1 as Element of NAT by ORDINAL1:def 12;
A122:   ex K,L st K = (h.k1)`2 & L = K \/ still_not-bound_in {f.(k1+1)} &
        h.(k1+1) = [('not' (f.(k1+1))) 'or' (the_scope_of(f,(k1+1)).
        (bound_in(f,k1+1),x.(Al-one_in {t : not x.t in L}))),
        K \/ still_not-bound_in
        ('not' (f.(k1+1))) 'or' (the_scope_of(f,k1+1).(bound_in(f,k1+1),
        x.(Al-one_in {u : not x.u in L})))] by A6;
        set K = (h.k1)`2;
        set r1 = f.(k1+1);
        set L = K \/ still_not-bound_in {r1};
        set p1 = 'not' r1 'or' (the_scope_of(f,(k1+1)).
        (bound_in(f,k1+1),x.(Al-one_in {t : not x.t in L})));
A123:   r = p1 by A121,A122,MCART_1:7;
        reconsider s = (the_scope_of(f,(k1+1)).
        (bound_in(f,k1+1),x.(Al-one_in {t : not x.t in L})))
        as Element of CQC-WFF(Al);
A124:   |- (f1^<*'not' r1*>)^<*p1*> by A99,A121,CALCUL_1:51;
        0+1 <= len (f1^<*r*>) by CALCUL_1:10;
        then |- Ant(f1^<*r*>)^<*'not' r1*>^<*Suc(f1^<*r*>)*>^
        <*'not' VERUM(Al)*> by A98,Th25;
        then |- f1^<*'not' r1*>^<*Suc(f1^<*r*>)*>^<*'not' VERUM(Al)*>
        by CALCUL_1:5;
        then |- (f1^<*'not' r1*>)^<*r*>^<*'not' VERUM(Al)*> by CALCUL_1:5;
        then
A125:   |- f1^<*'not' r1*>^<*'not' VERUM(Al)*> by A123,A124,CALCUL_2:24;
        |- f1^<*s*>^<*s*> by CALCUL_2:21;
        then
A126:   |- f1^<*s*>^<*p1*> by CALCUL_1:52;
        0+1 <= len (f1^<*r*>) by CALCUL_1:10;
        then |- Ant(f1^<*r*>)^<*s*>^<*Suc(f1^<*r*>)*>^<*'not' VERUM(Al)*>
        by A98,Th25;
        then |- f1^<*s*>^<*Suc(f1^<*r*>)*>^<*'not' VERUM(Al)*> by CALCUL_1:5;
        then |- (f1^<*s*>)^<*p1*>^<*'not' VERUM(Al)*> by A123,CALCUL_1:5;
        then
A127:   |- f1^<*s*>^<*'not' VERUM(Al)*> by A126,CALCUL_2:24;
        set y = x.(Al-one_in {t : not x.t in L});
        set u = Al-one_in {t : not x.t in L};
        reconsider r2 = the_scope_of(f,k1+1) as Element of CQC-WFF(Al);
        reconsider y2 = bound_in(f,k1+1) as bound_QC-variable of Al;
        reconsider r1 as Element of CQC-WFF(Al);
        r1 in ExCl(Al) by A3,A4,FUNCT_1:3;
        then consider y1,s1 such that
A128:   r1 = Ex(y1,s1) by Def3;
A129:   s1 = Ex-the_scope_of r1 by A128,Th22;
A130:   r2 = Ex-the_scope_of r1 by Def7;
A131:   y1 = Ex-bound_in r1 by A128,Th22;
A132:   y2 = Ex-bound_in r1 by Def6;
        reconsider Z = F.k as Subset of CQC-WFF(Al);
        not y in still_not-bound_in (Z \/ {r1}) by A74,A121;
        then
A133:   not y in still_not-bound_in Z \/ still_not-bound_in {r1} by Th27;
        then
A134:   not y in still_not-bound_in { r1} by XBOOLE_0:def 3;
        still_not-bound_in rng f1 c= still_not-bound_in Z by A97,Th29;
        then not y in still_not-bound_in rng f1 by A133,XBOOLE_0:def 3;
        then
A135:   not y in still_not-bound_in f1 by Th30;
        not y in still_not-bound_in r1 by A134,Th26;
        then not y in still_not-bound_in <*r1*> by CALCUL_1:60;
        then not y in still_not-bound_in f1 \/
        still_not-bound_in <*r1*> by A135,XBOOLE_0:def 3;
        then
A136:   not y in still_not-bound_in (f1^<*r1*>) by CALCUL_1:59;
        still_not-bound_in VERUM(Al) = {} by QC_LANG3:3;
        then not x.u in still_not-bound_in 'not' VERUM(Al) by QC_LANG3:7;
        then not x.u in still_not-bound_in <*'not' VERUM(Al)*>
        by CALCUL_1:60;
        then not x.u in still_not-bound_in (f1^<*r1*>) \/
        still_not-bound_in <*'not' VERUM(Al)*> by A136,XBOOLE_0:def 3;
        then not x.u in still_not-bound_in (f1^<*r1*>^<*'not' VERUM(Al)*>)
        by CALCUL_1:59;
        then |- f1^<*r1*>^<*'not' VERUM(Al)*> by A127,A128,A129,A130,A131,A132,
CALCUL_1:61;
        then |- f1^<*'not' VERUM(Al)*> by A125,CALCUL_2:26;
        then F.k |- 'not' VERUM(Al) by A97,HENMODEL:def 1;
        hence contradiction by A96,Th24;
      end;
      hence contradiction by A100;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A94,A95);
  then for n,m st m in dom F & n in dom F & n < m holds F.n is Consistent &
  F.n c= F.m by A41;
  then reconsider CY as Consistent Subset of CQC-WFF(Al) by A40,HENMODEL:11;
  take CY;
  thus thesis by A9,Def2,XBOOLE_1:7;
end;

theorem Th32:
  X |- p & X c= Y implies Y |- p
proof
  assume that
A1: X |- p and
A2: X c= Y;
  consider f being FinSequence of CQC-WFF(Al) such that
A3: rng f c= X and
A4: |- f^<*p*> by A1,HENMODEL:def 1;
  rng f c= Y by A2,A3,XBOOLE_1:1;
  hence thesis by A4,HENMODEL:def 1;
end;

reserve C,D for Subset of CQC-WFF(Al);

:: Ebb et al, Chapter V, Lemma 2.2

theorem Th33:
  ( Al is countable &
  CX is with_examples ) implies ( ex CY st CX c= CY &
  CY is negation_faithful & CY is with_examples )
proof
  assume A1: Al is countable;
  assume
A2: CX is with_examples;
  CQC-WFF(Al) is non empty & CQC-WFF(Al) is countable by Th19, A1;
  then consider f being Function such that
A3: dom f = NAT and
A4: CQC-WFF(Al) = rng f by Lm1;
  reconsider f as Function of NAT,CQC-WFF(Al) by A3,A4,FUNCT_2:2;
  defpred P[set,set,set] means
  ex X st X = $2 \/ {f.$1} & (X is Consistent implies $3 = X) &
  (not X is Consistent implies $3 = $2);
A5: for n for C ex D st P[n,C,D]
  proof
    let n;
    reconsider p = f.n as Element of CQC-WFF(Al);
    let C;
    set X = C \/ {p};
    reconsider X as Subset of CQC-WFF(Al);
    not X is Consistent implies ex D st D = C &
    ex X st X = C \/ {p} & (X is Consistent implies D = X) &
    (not X is Consistent implies D = C);
    hence thesis;
  end;
  consider h being Function of NAT,bool CQC-WFF(Al) such that
A6: h.0 = CX & for n holds P[n,h.n,h.(n+1)] from RECDEF_1:sch 2(A5);
  set CY = union rng h;
A7: now
    let a such that
A8: a in CX;
    dom h = NAT by FUNCT_2:def 1;
    then h.0 in rng h by FUNCT_1:3;
    hence a in union rng h by A6,A8,TARSKI:def 4;
  end;
  then
A9: CX c= CY by TARSKI:def 3;
A10: for n holds h.n c= h.(n+1)
  proof
    let n;
    let a such that
A11: a in h.n;
    reconsider p = f.n as Element of CQC-WFF(Al);
    set X = h.n \/ {p};
    reconsider X as Subset of CQC-WFF(Al);
A12: h.n c= X by XBOOLE_1:7;
    ex Y st Y = h.n \/ {f.n} & (Y is Consistent implies h.(n+1) = Y) &
    (not Y is Consistent implies h.(n+1) = h.n) by A6;
    hence thesis by A11,A12;
  end;
A13: for n,m st m in dom h & n in dom h & n < m holds h.n c= h.m
  proof
    let n,m such that
    m in dom h and n in dom h and
A14: n < m;
    defpred P[Element of NAT] means n <= $1 implies h.n c= h.$1;
A15: P[0]
    proof
      assume n <= 0;
      then n = 0 by NAT_1:2;
      hence thesis;
    end;
A16: for k st P[k] holds P[k+1]
    proof
      let k such that
A17:  P[k];
      assume
A18:  n <= k+1;
      now
        assume
A19:    n <= k;
        h.k c= h.(k+1) by A10;
        hence thesis by A17,A19,XBOOLE_1:1;
      end;
      hence thesis by A18,NAT_1:8;
    end;
    for k holds P[k] from NAT_1:sch 1(A15,A16);
    hence thesis by A14;
  end;
  defpred P[Element of NAT] means h.$1 is Consistent;
A20: P[0] by A6;
A21: for k st P[k] holds P[k+1]
  proof
    let n such that
A22: P[n];
    ex Y st Y = h.n \/ {f.n} & (Y is Consistent implies h.(n+1) = Y) &
    (not Y is Consistent implies h.(n+1) = h.n) by A6;
    hence thesis by A22;
  end;
  set CY = union rng h;
  for n holds P[n] from NAT_1:sch 1(A20,A21);
  then for n,m st m in dom h & n in dom h & n < m holds h.n is Consistent &
  h.n c= h.m by A13;
  then reconsider CY as Consistent Subset of CQC-WFF(Al) by HENMODEL:11;
A23: CY is negation_faithful
  proof
    let p;
    consider a such that
A24: a in dom f and
A25: f.a = p by A4,FUNCT_1:def 3;
    reconsider n = a as Element of NAT by A24;
    now
      assume not CY |- 'not' p;
      then
A26:  not CY \/ {p} is Inconsistent by HENMODEL:10;
A27:  now
        assume h.n \/ {p} is Inconsistent;
        then
A28:    h.n \/ {p} |- 'not' VERUM(Al) by Th24;
        now
          let a such that
A29:      a in h.n;
          dom h = NAT by FUNCT_2:def 1;
          then h.n in rng h by FUNCT_1:3;
          hence a in CY by A29,TARSKI:def 4;
        end;
        then h.n c= CY by TARSKI:def 3;
        then CY \/ {p} |- 'not' VERUM(Al) by A28,Th32,XBOOLE_1:9;
        hence contradiction by A26,Th24;
      end;
A30:  ex Y st Y = h.n \/ {f.n} & (Y is Consistent implies h.(n+1) = Y) &
      (not Y is Consistent implies h.(n+1) = h.n) by A6;
      now
        let a such that
A31:    a in h.(n+1);
        dom h = NAT by FUNCT_2:def 1;
        then h.(n+1) in rng h by FUNCT_1:3;
        hence a in CY by A31,TARSKI:def 4;
      end;
      then
A32:  h.(n+1) c= CY by TARSKI:def 3;
      {p} c= h.(n+1) by A25,A27,A30,XBOOLE_1:7;
      then {p} c= CY by A32,XBOOLE_1:1;
      then p in CY by ZFMISC_1:31;
      hence CY |- p by Th21;
    end;
    hence thesis;
  end;
A33: CY is with_examples
  proof
    let x,p;
    consider y such that
A34: CX |- ('not' Ex(x,p)) 'or' (p.(x,y)) by A2,Def2;
    take y;
    thus thesis by A9,A34,Th32;
  end;
  take CY;
  thus thesis by A7,A23,A33,TARSKI:def 3;
end;

reserve JH1 for Henkin_interpretation of CZ,
  J for interpretation of Al, A,
  v for Element of Valuations_in(Al,A);

theorem Th34:
  (Al is countable & still_not-bound_in CX is finite)
   implies ex CZ,JH1 st JH1,valH(Al) |= CX
proof
  assume A1: Al is countable;
  assume still_not-bound_in CX is finite;
  then consider CY such that
A2: CX c= CY and
A3: CY is with_examples by Th31, A1;
  consider CZ such that
A4: CY c= CZ and
A5: CZ is negation_faithful and
A6: CZ is with_examples by A1,A3,Th33;
A7: CX c= CZ by A2,A4,XBOOLE_1:1;
  set JH1 =the  Henkin_interpretation of CZ;
A8: now
    let p;
    assume p in CX;
    then CZ |- p by A7,Th21;
    hence JH1,valH(Al) |= p by A5,A6,Th17;
  end;
  take CZ,JH1;
  thus thesis by A8,CALCUL_1:def 11;
end;

begin :: Goedel's Completeness Theorem,
:: Ebb et al, Chapter V, Completeness Theorem 4.1

theorem Th35:
  J,v |= X & Y c= X implies J,v |= Y
proof
  assume
A1: J,v |= X;
  assume Y c= X;
  then p in Y implies J,v |= p by A1,CALCUL_1:def 11;
  hence thesis by CALCUL_1:def 11;
end;

theorem Th36:
  still_not-bound_in X is finite implies
  still_not-bound_in (X \/ {p}) is finite
proof
  assume
A1: still_not-bound_in X is finite;
  still_not-bound_in p is finite by CQC_SIM1:19;
  then still_not-bound_in {p} is finite by Th26;
  then still_not-bound_in X \/ still_not-bound_in {p} is finite by A1;
  hence thesis by Th27;
end;

theorem Th37:
  X |= p implies not J,v |= X \/ {'not' p}
proof
  assume
A1: X |= p;
  assume
A2: J,v |= X \/ {'not' p};
  then
A3: J,v |= X by Th35,XBOOLE_1:7;
A4: {'not' p} c= X \/ {'not' p} by XBOOLE_1:7;
  'not' p in {'not' p} by TARSKI:def 1;
  then J,v |= 'not' p by A2,A4,CALCUL_1:def 11;
  then not J,v |= p by VALUAT_1:17;
  hence contradiction by A1,A3,CALCUL_1:def 12;
end;

::$N Goedel Completeness Theorem
theorem
  ( Al is countable &
  still_not-bound_in X is finite & X |= p ) implies X |- p
proof
  assume
A1: Al is countable;
  assume
A2: still_not-bound_in X is finite;
  assume
A3: X |= p;
  assume
A4: not X |- p;
  reconsider Y = X \/ {'not' p} as Subset of CQC-WFF(Al);
A5: still_not-bound_in Y is finite by A2,Th36;
  Y is Consistent by A4,HENMODEL:9;
  then ex CZ,JH1 st ( JH1,valH(Al) |= Y) by A1,A5,Th34;
  hence contradiction by A3,Th37;
end;