:: G{\"o}del's Completeness Theorem :: by Patrick Braselmann and Peter Koepke :: :: Received September 25, 2004 :: Copyright (c) 2004-2018 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, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, ORDINAL1, CARD_1, CARD_3, FINSEQ_1, FUNCT_1, NAT_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, XFAMILY, 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, XFAMILY; 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; equalities XBOOLE_0, ORDINAL1, CARD_1; expansions TARSKI, XBOOLE_0; theorems TARSKI, FUNCT_1, MCART_1, XBOOLE_0, XBOOLE_1, CQC_LANG, QC_LANG1, ZFMISC_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 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 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 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; 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 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 by VALUAT_1:17; (ex a st J,v.(x|a) |= p) implies ex a st not J,v.(x|a) |= 'not' p proof given a such that A3: J,v.(x|a) |= p; take a; thus thesis by A3,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); then consider b being object such that A3: b in dom valH(Al) and A4: (valH(Al)).b = x1 by A2,FUNCT_1:def 3; 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 by VALUAT_1:17; 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[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,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,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 2(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[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,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,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 2(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 A1,QC_LANG1:5; 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[object] means ex x,p st \$1 = Ex(x,p); consider X being set such that A1: for a being object holds a in X iff a in CQC-WFF(Al) & P[a] from XBOOLE_0:sch 1; for a being object 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[object] 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 be object; a in A1 iff P[a] by A2; hence a in A1 iff a in A2 by A3; end; hence thesis by TARSKI:2; 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 sequence of 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 A1: 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 A2: p = Ex(x,F1) by A1,QC_LANG2:def 13; p = 'not' All(x,'not' F1) by A2,QC_LANG2:def 5; then All(x,'not' F1) is Element of CQC-WFF(Al) by CQC_LANG:8; then A3: 'not' F1 is Element of CQC-WFF(Al) by CQC_LANG:13; take F1; thus thesis by A2,A3,CQC_LANG:8; end; uniqueness by QC_LANG2:13; end; definition let Al; let F be sequence of CQC-WFF(Al),a be 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 sequence of CQC-WFF(Al),a be 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 be object; 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 be object; 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; |- <*>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; |- f^<*VERUM(Al)*> by HENMODEL:15; hence thesis by A1,HENMODEL:def 1; end; theorem Th24: X |- 'not' VERUM(Al) iff X is Inconsistent by Th23,HENMODEL:6,def 2; 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 be object; 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 be object 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:2; 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 be object; 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 be object 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 being object holds b in A iff b in bound_QC-variables(Al)) by A1,TARSKI:2; 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; let a be object; 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; 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 be object; assume a in still_not-bound_in rng f; then consider b being set 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 being object 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 be object; assume a in still_not-bound_in f; then consider i being Nat,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:2; 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 sequence of CQC-WFF(Al) by A3,A4,FUNCT_2:2; defpred P[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 being Nat for C ex D st P[n,C,D] proof let n be Nat,C; set K = C`2; ex a,b being object 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); 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 sequence of [:CQC-WFF(Al),bool bound_QC-variables(Al):] such that A6: h.0 = A & for n being Nat holds P[n,h.n,h.(n+1)] from RECDEF_1:sch 2(A5); set CY = CX \/ the set of all (h.n)`1 ; now let a be object such that A7: a in CY; now assume not a in CX; then a in the set of all (h.n)`1 by A7,XBOOLE_0:def 3; then consider n such that A8: a = (h.n)`1; ex c,d being object 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; 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 being object such that A10: a in dom f and A11: f.a = Ex(x,p) by A4,FUNCT_1:def 3; reconsider a as 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 the set of all (h.n)`1 ; A17: the set of all (h.n)`1 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; 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 Nat such that A20: a = m+1 by NAT_1:6; reconsider m as Nat; 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; 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 5; A23: CY c= union rng F proof let a be object; 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 be object; 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 the set of all (h.n)`1 ; then consider n such that A29: a = (h.n)`1; n < n+1 by NAT_1:13; then n in Segm(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 be object; 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 being object 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 the set of all (h.i)`1 ; the set of all (h.i)`1 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; 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; reconsider n,m as Element of NAT by ORDINAL1:def 12; 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 be object 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 Segm n; i < n by A49,NAT_1:44; then i < m by A42,XXREAL_0:2; then i in Segm 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; end; rng F c= bool CQC-WFF(Al) proof let a be object; assume a in rng F; then consider b being object 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 be object; 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); then F.b c= CQC-WFF(Al) by A53,XBOOLE_1:8; hence thesis by A52; end; then reconsider F as sequence of bool CQC-WFF(Al) by A22,FUNCT_2:2; A54: for n holds F.(n+1) = F.n \/ {(h.n)`1} proof let n; A55: n in NAT by ORDINAL1:def 12; now let a be object; assume a in {(h.i)`1 : i in n+1}; then consider j such that A56: a = (h.j)`1 and A57: j in Segm(n+1); j < n+1 by A57,NAT_1:44; then A58: j+1 <= n+1 by NAT_1:13; A59: now assume j+1 = n+1; then A60: a in {(h.n)`1} by A56,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 A60; end; now assume j+1 <= n; then j < n by NAT_1:13; then j in Segm n by NAT_1:44; then A61: a in {(h.k)`1 : k in n} by A56; {(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 A61; end; hence a in {(h.i)`1 : i in n} \/ {(h.n)`1} by A58,A59,NAT_1:8; end; then A62: {(h.k)`1 : k in n+1} c= {(h.i)`1 : i in n} \/ {(h.n)`1}; now let a be object; assume A63: a in {(h.i)`1 : i in n} \/ {(h.n)`1}; A64: now assume a in {(h.i)`1 : i in n}; then consider j such that A65: (h.j)`1 = a and A66: j in Segm n; A67: n <= n+1 by NAT_1:11; j < n by A66,NAT_1:44; then j < n+1 by A67,XXREAL_0:2; then j in Segm(n+1) by NAT_1:44; hence a in {(h.i)`1 : i in n+1} by A65; end; now assume a in {(h.n)`1}; then A68: a = (h.n)`1 by TARSKI:def 1; n < n+1 by NAT_1:13; then n in Segm(n+1) by NAT_1:44; hence a in {(h.i)`1 : i in n+1} by A68; end; hence a in {(h.i)`1 : i in n+1} by A63,A64,XBOOLE_0:def 3; end; then {(h.i)`1 : i in n} \/ {(h.n)`1} c= {(h.k)`1 : k in n+1}; then {(h.i)`1 : i in n} \/ {(h.n)`1} = {(h.k)`1 : k in n+1} by A62; then F.(n+1) = CX \/ ({(h.k)`1 : k in n} \/ {(h.n)`1}) by A22; then F.(n+1) = G(n) \/ {(h.n)`1} by XBOOLE_1:4; hence F.(n+1) = F.n \/ {(h.n)`1} by A22,A55; end; defpred P[Nat] means (h.\$1)`2 is finite & (h.\$1)`2 is Subset of bound_QC-variables(Al); A69: P[0] proof A70: (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; 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 A70,Th27; end; A71: for k st P[k] holds P[k+1] proof let k such that A72: P[k]; A73: 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 A72; 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 A72,A73; end; A74: for k holds P[k] from NAT_1:sch 2(A69,A71); defpred P[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)}); A75: 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 A76: 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); A77: (h.0)`2 = still_not-bound_in (CX \/ A1) by A6; reconsider B = (h.0)`2 as Subset of bound_QC-variables(Al) by A6; 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 A78: not x in C by A69,Th28; consider u such that A79: x.u = x by QC_LANG3:30; u in {t : not x.t in C} by A78,A79; then reconsider A = {t : not x.t in C} as non empty set; now let a be object; 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 A80: ex t st ( t = u)&( not x.t in C); A81: F.0 = CX \/ {(h.n)`1 : n in 0} by A22; now let b be object; assume b in {(h.n)`1 : n in 0}; then ex n st ( b = (h.n)`1)&( n in 0); hence contradiction; end; then A82: {(h.n)`1 : n in 0} = {} by XBOOLE_0:def 1; (h.0)`1 = r by A6; then F.(0+1) = CX \/ {r} by A54,A81,A82; hence thesis by A77,A80,Th27; end; A83: for k st P[k] holds P[k+1] proof let k such that A84: P[k]; reconsider s = f.(k+2) as Element of CQC-WFF(Al); A85: 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 A74; 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}))); A86: (h.(k+1))`1 = r by A85; A87: (h.(k+1))`2 = K \/ still_not-bound_in r by A85; reconsider B = (h.(k+1))`2 as Subset of bound_QC-variables(Al) by A85; 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 A88: still_not-bound_in {s} is finite by Th26; (h.(k+1))`2 is finite by A74; then consider x such that A89: not x in C by A88,Th28; consider u such that A90: x.u = x by QC_LANG3:30; u in {t : not x.t in still_not-bound_in {s} \/ B} by A89,A90; then reconsider A = {t : not x.t in still_not-bound_in {s} \/ B} as non empty set; now let a be object; 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 A91: ex t st ( t = u)&( not x.t in C); then A92: 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 A84,A87,XBOOLE_1:9; then still_not-bound_in (F.(k+1)) \/ still_not-bound_in {r} c= B by Th26; then A93: 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,A86; then not x.u in still_not-bound_in (F.(k+1+1)) by A91,XBOOLE_0:def 3; then not x.u in still_not-bound_in (F.(k+1+1)) \/ still_not-bound_in {s} by A92,XBOOLE_0:def 3; hence thesis by A54,A86,A93,Th27; end; for k holds P[k] from NAT_1:sch 2(A76,A83); hence thesis; end; defpred P[Nat] means F.\$1 is Consistent; now let a be object; 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 A94: F.0 = CX \/ {} by A22; then A95: P[0]; A96: for k st P[k] holds P[k+1] proof let k such that A97: P[k]; ex c,d being object 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); 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 A98: rng f1 c= F.k and A99: |- f1^<*r*>^<*'not' VERUM(Al)*> by HENMODEL:8; A100: |- f1^<*'not' (f.k)*>^<*'not' (f.k)*> by CALCUL_2:21; A101: now assume A102: k = 0; then A103: 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; 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); A104: |- (f1^<*'not' (f.k)*>)^<*('not' (f.k)) 'or' s*> by A100,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 A99,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 A105: |- f1^<*'not' (f.k)*>^<*'not' VERUM(Al)*> by A102,A103,A104,CALCUL_2:24; |- f1^<*s*>^<*s*> by CALCUL_2:21; then A106: |- 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 A99,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 A107: |- f1^<*s*>^<*'not' VERUM(Al)*> by A102,A103,A106,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 A108: not x in C by Th28; consider u such that A109: x.u = x by QC_LANG3:30; u in {t : not x.t in C} by A108,A109; then reconsider A = {t : not x.t in C} as non empty set; now let a be object; 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 A110: t = u and A111: not x.t in C; A112: not x.t in still_not-bound_in CX \/ still_not-bound_in {r1} by A111,Th27; then A113: not x.t in still_not-bound_in {r1} by XBOOLE_0:def 3; A114: F.0 = CX \/ {(h.n)`1 : n in 0} by A22; now let b be object; 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 A98,A102,A114,Th29; then not x.t in still_not-bound_in rng f1 by A112,XBOOLE_0:def 3; then A115: not x.u in still_not-bound_in f1 by A110,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 A116: r1 = Ex(y1,s1) by Def3; A117: s1 = Ex-the_scope_of r1 by A116,Th22; A118: r2 = Ex-the_scope_of r1 by Def7; A119: y1 = Ex-bound_in r1 by A116,Th22; A120: y2 = Ex-bound_in r1 by Def6; not x.u in still_not-bound_in r1 by A110,A113,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 A115,XBOOLE_0:def 3; then A121: 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 A121,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 A107,A116,A117,A118,A119,A120, CALCUL_1:61; then |- f1^<*'not' VERUM(Al)*> by A102,A105,CALCUL_2:26; then F.k |- 'not' VERUM(Al) by A98,HENMODEL:def 1; hence contradiction by A94,A102,Th24; end; now assume k <> 0; then consider k1 being Nat such that A122: k = k1+1 by NAT_1:6; reconsider k1 as Nat; A123: 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}))); A124: r = p1 by A122,A123; 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); A125: |- (f1^<*'not' r1*>)^<*p1*> by A100,A122,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 A99,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 A126: |- f1^<*'not' r1*>^<*'not' VERUM(Al)*> by A124,A125,CALCUL_2:24; |- f1^<*s*>^<*s*> by CALCUL_2:21; then A127: |- 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 A99,Th25; then |- f1^<*s*>^<*Suc(f1^<*r*>)*>^<*'not' VERUM(Al)*> by CALCUL_1:5; then |- (f1^<*s*>)^<*p1*>^<*'not' VERUM(Al)*> by A124,CALCUL_1:5; then A128: |- f1^<*s*>^<*'not' VERUM(Al)*> by A127,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 A129: r1 = Ex(y1,s1) by Def3; A130: s1 = Ex-the_scope_of r1 by A129,Th22; A131: r2 = Ex-the_scope_of r1 by Def7; A132: y1 = Ex-bound_in r1 by A129,Th22; A133: 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 A75,A122; then A134: not y in still_not-bound_in Z \/ still_not-bound_in {r1} by Th27; then A135: 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 A98,Th29; then not y in still_not-bound_in rng f1 by A134,XBOOLE_0:def 3; then A136: not y in still_not-bound_in f1 by Th30; not y in still_not-bound_in r1 by A135,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 A136,XBOOLE_0:def 3; then A137: 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 A137,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 A128,A129,A130,A131,A132,A133, CALCUL_1:61; then |- f1^<*'not' VERUM(Al)*> by A126,CALCUL_2:26; then F.k |- 'not' VERUM(Al) by A98,HENMODEL:def 1; hence contradiction by A97,Th24; end; hence contradiction by A101; end; hence thesis; end; for n holds P[n] from NAT_1:sch 2(A95,A96); 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,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; 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 sequence of 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 being Nat for C ex D st P[n,C,D] proof let n be Nat; 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 sequence of bool CQC-WFF(Al) such that A6: h.0 = CX & for n being Nat holds P[n,h.n,h.(n+1)] from RECDEF_1:sch 2(A5); set CY = union rng h; A7: now let a be object 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; A10: for n holds h.n c= h.(n+1) proof let n; let a be object 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[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; end; hence thesis by A18,NAT_1:8; end; for k holds P[k] from NAT_1:sch 2(A15,A16); hence thesis by A14; end; defpred P[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 2(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 being object such that A24: a in dom f and A25: f.a = p by A4,FUNCT_1:def 3; reconsider n = a as 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 be object such that A29: a in h.n; A30: n in NAT by ORDINAL1:def 12; dom h = NAT by FUNCT_2:def 1; then h.n in rng h by FUNCT_1:3,A30; hence a in CY by A29,TARSKI:def 4; end; then h.n c= CY; then CY \/ {p} |- 'not' VERUM(Al) by A28,Th32,XBOOLE_1:9; hence contradiction by A26,Th24; end; A31: 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 be object such that A32: 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 A32,TARSKI:def 4; end; then A33: h.(n+1) c= CY; {p} c= h.(n+1) by A25,A27,A31,XBOOLE_1:7; then {p} c= CY by A33; then p in CY by ZFMISC_1:31; hence CY |- p by Th21; end; hence thesis; end; A34: CY is with_examples proof let x,p; consider y such that A35: CX |- ('not' Ex(x,p)) 'or' (p.(x,y)) by A2; take y; thus thesis by A9,A35,Th32; end; take CY; thus thesis by A7,A23,A34; 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; 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;