:: G{\"o}del's Completeness Theorem
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2026 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;
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: a = 0 implies ex y being bound_QC-variable of Al
st CY |- 'not' Ex(x,p) 'or' (p.(x,y)) by A6,A11,A14,A15,A16,A17,Th21;
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;