:: GOEDELCP semantic presentation

begin

registration
cluster countable for QC-alphabet ;
existence
 ex b1 being QC-alphabet st b1 is countable
proof
A1: [:NAT,NAT:] is QC-alphabet by QC_LANG1:def_1;
 [:NAT,NAT:] is countable by CARD_4:7;
hence  ex b1 being QC-alphabet st b1 is countable by A1; ::_thesis: verum
end;
end;


definition
let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
attrX is negation_faithful  means :Def1: :: GOEDELCP:def 1
 for p being Element of CQC-WFF Al holds
( X |- p or X |- 'not' p );
end;

:: deftheorem Def1 defines negation_faithful GOEDELCP:def_1_:_
 for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds
( X is negation_faithful iff for p being Element of CQC-WFF Al holds
( X |- p or X |- 'not' p ) );

definition
let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
attrX is with_examples  means :Def2: :: GOEDELCP:def 2
 for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st X |- ('not' (Ex (x,p))) 'or' (p . (x,y));
end;

:: deftheorem Def2 defines with_examples GOEDELCP:def_2_:_
 for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds
( X is with_examples iff for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st X |- ('not' (Ex (x,p))) 'or' (p . (x,y)) );

theorem :: GOEDELCP:1
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al) st CX is negation_faithful holds
( CX |- p iff not CX |- 'not' p ) by Def1, HENMODEL:def_2;

theorem Th2: :: GOEDELCP:2
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*(('not' p) 'or' q)*> & |- f ^ <*p*> holds
|- f ^ <*q*>
proof
let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*(('not' p) 'or' q)*> & |- f ^ <*p*> holds
|- f ^ <*q*>
let p, q be Element of CQC-WFF Al; ::_thesis: for f being FinSequence of CQC-WFF Al st |- f ^ <*(('not' p) 'or' q)*> & |- f ^ <*p*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF Al; ::_thesis: ( |- f ^ <*(('not' p) 'or' q)*> & |- f ^ <*p*> implies |- f ^ <*q*> )
assume that
A1: |- f ^ <*(('not' p) 'or' q)*> and
A2: |- f ^ <*p*> ; ::_thesis: |- f ^ <*q*>
set f1 = (f ^ <*('not' p)*>) ^ <*p*>;
A3: Ant ((f ^ <*('not' p)*>) ^ <*p*>) = 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 ((f ^ <*('not' p)*>) ^ <*p*>) by CALCUL_1:5;
then A5: |- (f ^ <*('not' p)*>) ^ <*p*> by A2, A3, A4, CALCUL_1:8, CALCUL_1:36;
set f2 = (f ^ <*('not' p)*>) ^ <*('not' p)*>;
A6: Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = f ^ <*('not' p)*> by CALCUL_1:5;
A7: Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = 'not' p by CALCUL_1:5;
A8: (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((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 ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) by A6, FINSEQ_1:22;
then  (len f) + 1 in dom (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) by A6, CALCUL_1:10;
then  Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) is_tail_of Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) by A7, A8, CALCUL_1:def_16;
then A9: |- (f ^ <*('not' p)*>) ^ <*('not' p)*> by CALCUL_1:33;
A10: 0 + 1 <= len ((f ^ <*('not' p)*>) ^ <*('not' p)*>) by CALCUL_1:10;
A11: Ant ((f ^ <*('not' p)*>) ^ <*p*>) = Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) by A6, CALCUL_1:5;
 'not' (Suc ((f ^ <*('not' p)*>) ^ <*p*>)) = Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) by A7, CALCUL_1:5;
then  |- (Ant ((f ^ <*('not' p)*>) ^ <*p*>)) ^ <*('not' (Suc ((f ^ <*('not' p)*>) ^ <*p*>)))*> by A9, A10, A11, CALCUL_1:3;
then A12: |- (Ant ((f ^ <*('not' p)*>) ^ <*p*>)) ^ <*q*> by A5, CALCUL_1:44;
set f3 = (f ^ <*q*>) ^ <*q*>;
A13: Ant ((f ^ <*q*>) ^ <*q*>) = f ^ <*q*> by CALCUL_1:5;
A14: Suc ((f ^ <*q*>) ^ <*q*>) = q by CALCUL_1:5;
A15: (Ant ((f ^ <*q*>) ^ <*q*>)) . ((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 ((f ^ <*q*>) ^ <*q*>)) by A13, FINSEQ_1:22;
then  (len f) + 1 in dom (Ant ((f ^ <*q*>) ^ <*q*>)) by A13, CALCUL_1:10;
then  Suc ((f ^ <*q*>) ^ <*q*>) is_tail_of Ant ((f ^ <*q*>) ^ <*q*>) by A14, A15, CALCUL_1:def_16;
then  |- (f ^ <*q*>) ^ <*q*> 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 ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>) = ('not' ('not' p)) '&' ('not' q) by CALCUL_1:5;
then A18: |- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*> by A16, CALCUL_1:40, CALCUL_1:48;
A19: |- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*> by A16, A17, CALCUL_1:41, CALCUL_1:48;
set f5 = (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*>;
set f6 = (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*>;
A20: Ant ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*>) = Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>) by CALCUL_1:5;
A21: Suc ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*>) = 'not' ('not' p) by CALCUL_1:5;
A22: Ant ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*>) = Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>) by CALCUL_1:5;
 Suc ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*>) = 'not' q by CALCUL_1:5;
then  |- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*(('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  |- f ^ <*q*> by CALCUL_1:5; ::_thesis: verum
end;

theorem Th3: :: GOEDELCP:3
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al st X is with_examples holds
( X |- Ex (x,p) iff ex y being bound_QC-variable of Al st X |- p . (x,y) )
proof
let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al st X is with_examples holds
( X |- Ex (x,p) iff ex y being bound_QC-variable of Al st X |- p . (x,y) )
let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al st X is with_examples holds
( X |- Ex (x,p) iff ex y being bound_QC-variable of Al st X |- p . (x,y) )
let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al st X is with_examples holds
( X |- Ex (x,p) iff ex y being bound_QC-variable of Al st X |- p . (x,y) )
let x be bound_QC-variable of Al; ::_thesis: ( X is with_examples implies ( X |- Ex (x,p) iff ex y being bound_QC-variable of Al st X |- p . (x,y) ) )
assume A1: X is with_examples ; ::_thesis: ( X |- Ex (x,p) iff ex y being bound_QC-variable of Al st X |- p . (x,y) )
thus  ( X |- Ex (x,p) implies ex y being bound_QC-variable of Al st X |- p . (x,y) ) ::_thesis: ( ex y being bound_QC-variable of Al st X |- p . (x,y) implies X |- Ex (x,p) )
proof
assume  X |- Ex (x,p) ; ::_thesis: ex y being bound_QC-variable of Al st X |- p . (x,y)
then consider f1 being FinSequence of CQC-WFF Al such that
A2: rng f1 c= X and
A3: |- f1 ^ <*(Ex (x,p))*> by HENMODEL:def_1;
consider y being bound_QC-variable of Al such that
A4: X |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A1, Def2;
consider f2 being FinSequence of CQC-WFF Al 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 ; ::_thesis: X |- p . (x,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  X |- p . (x,y) by A8, HENMODEL:def_1; ::_thesis: verum
end;
thus  ( ex y being bound_QC-variable of Al st X |- p . (x,y) implies X |- Ex (x,p) ) ::_thesis: verum
proof
given y being bound_QC-variable of Al such that A9: X |- p . (x,y) ; ::_thesis: X |- Ex (x,p)
consider f1 being FinSequence of CQC-WFF Al 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  X |- Ex (x,p) by A10, HENMODEL:def_1; ::_thesis: verum
end;
end;

theorem :: GOEDELCP:4
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX st ( CX is negation_faithful & CX is with_examples implies ( JH, valH Al |= p iff CX |- p ) ) & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= 'not' p iff CX |- 'not' p ) by Def1, HENMODEL:def_2, VALUAT_1:17;

theorem Th5: :: GOEDELCP:5
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f1 being FinSequence of CQC-WFF Al st |- f1 ^ <*p*> & |- f1 ^ <*q*> holds
|- f1 ^ <*(p '&' q)*>
proof
let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al
for f1 being FinSequence of CQC-WFF Al st |- f1 ^ <*p*> & |- f1 ^ <*q*> holds
|- f1 ^ <*(p '&' q)*>
let p, q be Element of CQC-WFF Al; ::_thesis: for f1 being FinSequence of CQC-WFF Al st |- f1 ^ <*p*> & |- f1 ^ <*q*> holds
|- f1 ^ <*(p '&' q)*>
let f1 be FinSequence of CQC-WFF Al; ::_thesis: ( |- f1 ^ <*p*> & |- f1 ^ <*q*> implies |- f1 ^ <*(p '&' q)*> )
set g = f1 ^ <*p*>;
set g1 = f1 ^ <*q*>;
assume that
A1: |- f1 ^ <*p*> and
A2: |- f1 ^ <*q*> ; ::_thesis: |- f1 ^ <*(p '&' q)*>
A3: Ant (f1 ^ <*p*>) = f1 by CALCUL_1:5;
A4: Suc (f1 ^ <*p*>) = p by CALCUL_1:5;
A5: Suc (f1 ^ <*q*>) = q by CALCUL_1:5;
 Ant (f1 ^ <*p*>) = Ant (f1 ^ <*q*>) by A3, CALCUL_1:5;
hence  |- f1 ^ <*(p '&' q)*> by A1, A2, A3, A4, A5, CALCUL_1:39; ::_thesis: verum
end;

theorem Th6: :: GOEDELCP:6
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al holds
( ( X |- p & X |- q ) iff X |- p '&' q )
proof
let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al holds
( ( X |- p & X |- q ) iff X |- p '&' q )
let X be Subset of (CQC-WFF Al); ::_thesis: for p, q being Element of CQC-WFF Al holds
( ( X |- p & X |- q ) iff X |- p '&' q )
let p, q be Element of CQC-WFF Al; ::_thesis: ( ( X |- p & X |- q ) iff X |- p '&' q )
thus  ( X |- p & X |- q implies X |- p '&' q ) ::_thesis: ( X |- p '&' q implies ( X |- p & X |- q ) )
proof
assume that
A1: X |- p and
A2: X |- q ; ::_thesis: X |- p '&' q
consider f1 being FinSequence of CQC-WFF Al such that
A3: rng f1 c= X and
A4: |- f1 ^ <*p*> by A1, HENMODEL:def_1;
consider f2 being FinSequence of CQC-WFF Al 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  X |- p '&' q by A8, HENMODEL:def_1; ::_thesis: verum
end;
thus  ( X |- p '&' q implies ( X |- p & X |- q ) ) ::_thesis: verum
proof
assume  X |- p '&' q ; ::_thesis: ( X |- p & X |- q )
then consider f1 being FinSequence of CQC-WFF Al 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  ( X |- p & X |- q ) by A9, A11, HENMODEL:def_1; ::_thesis: verum
end;
end;

theorem :: GOEDELCP:7
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX st ( 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 ) ) & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p '&' q iff CX |- p '&' q ) by Th6, VALUAT_1:18;

theorem Th8: :: GOEDELCP:8
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st QuantNbr p <= 0 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proof
let Al be QC-alphabet ; ::_thesis: for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st QuantNbr p <= 0 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let CX be Consistent Subset of (CQC-WFF Al); ::_thesis: for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st QuantNbr p <= 0 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let JH be Henkin_interpretation of CX; ::_thesis: for p being Element of CQC-WFF Al st QuantNbr p <= 0 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
defpred S1[ 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 being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) ) by Def1, Th6, HENMODEL:16, HENMODEL:17, HENMODEL:def_2, VALUAT_1:17, VALUAT_1:18;
A2: for p being Element of CQC-WFF Al st QuantNbr p = 0 holds
S1[p] from SUBSTUT2:sch_3(A1);
now__::_thesis:_for_p_being_Element_of_CQC-WFF_Al_st_QuantNbr_p_<=_0_holds_
S1[p]
let p be Element of CQC-WFF Al; ::_thesis: ( QuantNbr p <= 0 implies S1[p] )
assume  QuantNbr p <= 0 ; ::_thesis: S1[p]
then  QuantNbr p = 0 by NAT_1:2;
hence  S1[p] by A2; ::_thesis: verum
end;
hence  for p being Element of CQC-WFF Al st QuantNbr p <= 0 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ; ::_thesis: verum
end;

theorem Th9: :: GOEDELCP:9
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= Ex (x,p) iff ex a being Element of A st J,v . (x | a) |= p )
proof
let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= Ex (x,p) iff ex a being Element of A st J,v . (x | a) |= p )
let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= Ex (x,p) iff ex a being Element of A st J,v . (x | a) |= p )
let x be bound_QC-variable of Al; ::_thesis: for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= Ex (x,p) iff ex a being Element of A st J,v . (x | a) |= p )
let A be non empty set ; ::_thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= Ex (x,p) iff ex a being Element of A st J,v . (x | a) |= p )
let J be interpretation of Al,A; ::_thesis: for v being Element of Valuations_in (Al,A) holds
( J,v |= Ex (x,p) iff ex a being Element of A st J,v . (x | a) |= p )
let v be Element of Valuations_in (Al,A); ::_thesis: ( J,v |= Ex (x,p) iff ex a being Element of A st J,v . (x | a) |= p )
A1: ( J,v |= 'not' (All (x,('not' p))) iff not J,v |= All (x,('not' p)) ) by VALUAT_1:17;
A2: ( not for a being Element of A holds J,v . (x | a) |= 'not' p implies ex a being Element of A st J,v . (x | a) |= p )
proof
given a being Element of A such that A3: not J,v . (x | a) |= 'not' p ; ::_thesis: ex a being Element of A st J,v . (x | a) |= p
take  a ; ::_thesis: J,v . (x | a) |= p
thus  J,v . (x | a) |= p by A3, VALUAT_1:17; ::_thesis: verum
end;
 ( ex a being Element of A st J,v . (x | a) |= p implies ex a being Element of A st not J,v . (x | a) |= 'not' p )
proof
given a being Element of A such that A4: J,v . (x | a) |= p ; ::_thesis: not for a being Element of A holds J,v . (x | a) |= 'not' p
take  a ; ::_thesis: not J,v . (x | a) |= 'not' p
thus  not J,v . (x | a) |= 'not' p by A4, VALUAT_1:17; ::_thesis: verum
end;
hence  ( J,v |= Ex (x,p) iff ex a being Element of A st J,v . (x | a) |= p ) by A1, A2, QC_LANG2:def_5, SUBLEMMA:50; ::_thesis: verum
end;

theorem Th10: :: GOEDELCP:10
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX holds
( JH, valH Al |= Ex (x,p) iff ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) )
proof
let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX holds
( JH, valH Al |= Ex (x,p) iff ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) )
let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX holds
( JH, valH Al |= Ex (x,p) iff ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) )
let x be bound_QC-variable of Al; ::_thesis: for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX holds
( JH, valH Al |= Ex (x,p) iff ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) )
let CX be Consistent Subset of (CQC-WFF Al); ::_thesis: for JH being Henkin_interpretation of CX holds
( JH, valH Al |= Ex (x,p) iff ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) )
let JH be Henkin_interpretation of CX; ::_thesis: ( JH, valH Al |= Ex (x,p) iff ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) )
thus  ( JH, valH Al |= Ex (x,p) implies ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) ) ::_thesis: ( ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) implies JH, valH Al |= Ex (x,p) )
proof
assume  JH, valH Al |= Ex (x,p) ; ::_thesis: ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y)
then consider x1 being Element of HCar Al such that
A1: JH,(valH Al) . (x | x1) |= p by Th9;
A2: HCar Al = bound_QC-variables Al by HENMODEL:def_4;
 valH Al = id (bound_QC-variables Al) by HENMODEL:def_6;
then  rng (valH Al) = bound_QC-variables Al by RELAT_1:45;
then consider b being set  such that
A3: b in dom (valH Al) and
A4: (valH Al) . b = x1 by FUNCT_1:def_3, A2;
reconsider y = b as bound_QC-variable of Al by A3;
take  y ; ::_thesis: JH, valH Al |= p . (x,y)
thus  JH, valH Al |= p . (x,y) by A1, A4, CALCUL_1:24; ::_thesis: verum
end;
thus  ( ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) implies JH, valH Al |= Ex (x,p) ) ::_thesis: verum
proof
given y being bound_QC-variable of Al such that A5: JH, valH Al |= p . (x,y) ; ::_thesis: JH, valH Al |= Ex (x,p)
 ex x1 being Element of HCar Al st
( (valH Al) . y = x1 & JH,(valH Al) . (x | x1) |= p ) by A5, CALCUL_1:24;
hence  JH, valH Al |= Ex (x,p) by Th9; ::_thesis: verum
end;
end;

theorem Th11: :: GOEDELCP:11
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) )
proof
let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) )
let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) )
let x be bound_QC-variable of Al; ::_thesis: for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) )
let A be non empty set ; ::_thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) )
let J be interpretation of Al,A; ::_thesis: for v being Element of Valuations_in (Al,A) holds
( J,v |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) )
let v be Element of Valuations_in (Al,A); ::_thesis: ( J,v |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) )
A1: ( not J,v |= Ex (x,('not' p)) iff for a being Element of A holds not J,v . (x | a) |= 'not' p ) by Th9;
A2: ( ( for a being Element of A holds not J,v . (x | a) |= 'not' p ) implies for a being Element of A holds J,v . (x | a) |= p )
proof
assume A3: for a being Element of A holds not J,v . (x | a) |= 'not' p ; ::_thesis: for a being Element of A holds J,v . (x | a) |= p
let a be Element of A; ::_thesis: J,v . (x | a) |= p
 not J,v . (x | a) |= 'not' p by A3;
hence  J,v . (x | a) |= p by VALUAT_1:17; ::_thesis: verum
end;
 ( ( for a being Element of A holds J,v . (x | a) |= p ) implies for a being Element of A holds not J,v . (x | a) |= 'not' p )
proof
assume A4: for a being Element of A holds J,v . (x | a) |= p ; ::_thesis: for a being Element of A holds not J,v . (x | a) |= 'not' p
let a be Element of A; ::_thesis: not J,v . (x | a) |= 'not' p
 J,v . (x | a) |= p by A4;
hence  not J,v . (x | a) |= 'not' p by VALUAT_1:17; ::_thesis: verum
end;
hence  ( J,v |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) ) by A1, A2, SUBLEMMA:50, VALUAT_1:17; ::_thesis: verum
end;

theorem Th12: :: GOEDELCP:12
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )
proof
let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )
let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )
let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al holds
( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )
let x be bound_QC-variable of Al; ::_thesis: ( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )
thus  ( X |- 'not' (Ex (x,('not' p))) implies X |- All (x,p) ) ::_thesis: ( X |- All (x,p) implies X |- 'not' (Ex (x,('not' p))) )
proof
assume  X |- 'not' (Ex (x,('not' p))) ; ::_thesis: X |- All (x,p)
then consider f1 being FinSequence of CQC-WFF Al 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  X |- All (x,p) by A1, HENMODEL:def_1; ::_thesis: verum
end;
thus  ( X |- All (x,p) implies X |- 'not' (Ex (x,('not' p))) ) ::_thesis: verum
proof
assume  X |- All (x,p) ; ::_thesis: X |- 'not' (Ex (x,('not' p)))
then consider f1 being FinSequence of CQC-WFF Al 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  X |- 'not' (Ex (x,('not' p))) by A3, HENMODEL:def_1; ::_thesis: verum
end;
end;

theorem :: GOEDELCP:13
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds QuantNbr (Ex (x,p)) = (QuantNbr p) + 1
proof
let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds QuantNbr (Ex (x,p)) = (QuantNbr p) + 1
let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al holds QuantNbr (Ex (x,p)) = (QuantNbr p) + 1
let x be bound_QC-variable of Al; ::_thesis: QuantNbr (Ex (x,p)) = (QuantNbr p) + 1
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  QuantNbr (Ex (x,p)) = (QuantNbr p) + 1 by CQC_SIM1:16; ::_thesis: verum
end;

theorem Th14: :: GOEDELCP:14
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al holds QuantNbr p = QuantNbr (p . (x,y))
proof
let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al holds QuantNbr p = QuantNbr (p . (x,y))
let p be Element of CQC-WFF Al; ::_thesis: for x, y being bound_QC-variable of Al holds QuantNbr p = QuantNbr (p . (x,y))
let x, y be bound_QC-variable of Al; ::_thesis: QuantNbr p = QuantNbr (p . (x,y))
 QuantNbr p = QuantNbr (CQC_Sub [p,(Sbst (x,y))]) by SUBSTUT2:25;
hence  QuantNbr p = QuantNbr (p . (x,y)) by SUBSTUT2:def_1; ::_thesis: verum
end;


theorem Th15: :: GOEDELCP:15
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st QuantNbr p = 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proof
let Al be QC-alphabet ; ::_thesis: for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st QuantNbr p = 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let CX be Consistent Subset of (CQC-WFF Al); ::_thesis: for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st QuantNbr p = 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let JH be Henkin_interpretation of CX; ::_thesis: for p being Element of CQC-WFF Al st QuantNbr p = 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let p be Element of CQC-WFF Al; ::_thesis: ( QuantNbr p = 1 & CX is negation_faithful & CX is with_examples implies ( JH, valH Al |= p iff CX |- p ) )
assume that
A1: QuantNbr p = 1 and
A2: CX is negation_faithful and
A3: CX is with_examples ; ::_thesis: ( JH, valH Al |= p iff CX |- p )
consider q being Element of CQC-WFF Al such that
A4: q is_subformula_of p and
A5: ex x being bound_QC-variable of Al ex r being Element of CQC-WFF Al st q = All (x,r) by A1, SUBSTUT2:32;
consider x being bound_QC-variable of Al, r being Element of CQC-WFF Al 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 the PATH of q,p by A4, SUBSTUT2:def_5;
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len the PATH of q,p implies ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . $1 & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) );
A11: S1[ 0 ] ;
A12: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A13: S1[k] ; ::_thesis: S1[k + 1]
assume that
A14: 1 <= k + 1 and
A15: k + 1 <= len the PATH of q,p ; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
set j = k + 1;
A16: now__::_thesis:_(_k_=_0_implies_ex_q_being_Element_of_CQC-WFF_Al_st_
(_QuantNbr_q_<=_QuantNbr_q_&_ex_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)_)
assume  k = 0 ; ::_thesis: ex q being Element of CQC-WFF Al st
( QuantNbr q <= QuantNbr q & ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) )
then A17: the PATH of q,p . (k + 1) = q by A4, SUBSTUT2:def_5;
take q = q; ::_thesis: ( QuantNbr q <= QuantNbr q & ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) )
thus  QuantNbr q <= QuantNbr q ; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
A18: now__::_thesis:_(_JH,_valH_Al_|=_Ex_(x,('not'_r))_implies_CX_|-_Ex_(x,('not'_r))_)
assume  JH, valH Al |= Ex (x,('not' r)) ; ::_thesis: CX |- Ex (x,('not' r))
then consider y being bound_QC-variable of Al 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; ::_thesis: verum
end;
now__::_thesis:_(_CX_|-_Ex_(x,('not'_r))_implies_JH,_valH_Al_|=_Ex_(x,('not'_r))_)
assume  CX |- Ex (x,('not' r)) ; ::_thesis: JH, valH Al |= Ex (x,('not' r))
then consider y being bound_QC-variable of Al 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; ::_thesis: verum
end;
then  ( JH, valH Al |= 'not' (Ex (x,('not' r))) iff CX |- 'not' (Ex (x,('not' r))) ) by A2, A18, Def1, HENMODEL:def_2, VALUAT_1:17;
then  ( JH, valH Al |= q iff CX |- q ) by A6, Th11, Th12;
hence  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A17; ::_thesis: verum
end;
now__::_thesis:_(_k_<>_0_implies_ex_s,_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)
assume  k <> 0 ; ::_thesis: ex s, p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
then  0 < k by NAT_1:3;
then A21: 0 + 1 <= k by NAT_1:13;
 k < len the PATH of q,p by A15, NAT_1:13;
then consider G1, H1 being Element of QC-WFF Al such that
A22: the PATH of q,p . k = G1 and
A23: the PATH of q,p . (k + 1) = H1 and
A24: G1 is_immediate_constituent_of H1 by A4, A21, SUBSTUT2:def_5;
consider p1 being Element of CQC-WFF Al such that
A25: p1 = the PATH of q,p . 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 being QC-formula of Al st
( F3 = the PATH of q,p . (k + 1) & 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 = s; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
A29: now__::_thesis:_(_s_=_'not'_p1_implies_ex_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)
assume A30: s = 'not' p1 ; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
then A31: QuantNbr q <= QuantNbr s by A26, CQC_SIM1:16;
 ( CX |- s iff JH, valH Al |= s ) by A2, A27, A30, Def1, HENMODEL:def_2, VALUAT_1:17;
hence  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A23, A31; ::_thesis: verum
end;
A32: QuantNbr s <= 1 by A1, A23, A28, SUBSTUT2:30;
A33: now__::_thesis:_(_ex_F1_being_QC-formula_of_Al_st_s_=_p1_'&'_F1_implies_ex_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)
given F1 being QC-formula of Al such that A34: s = p1 '&' F1 ; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
reconsider F1 = 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  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A23, A40; ::_thesis: verum
end;
A41: now__::_thesis:_(_ex_F1_being_QC-formula_of_Al_st_s_=_F1_'&'_p1_implies_ex_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)
given F1 being QC-formula of Al such that A42: s = F1 '&' p1 ; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
reconsider F1 = 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  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A23, A49; ::_thesis: verum
end;
now__::_thesis:_for_x_being_bound_QC-variable_of_Al_holds_not_s_=_All_(x,p1)
given x being bound_QC-variable of Al such that A50: s = All (x,p1) ; ::_thesis: contradiction
 1 < (QuantNbr p1) + 1 by A9, A26, NAT_1:13;
hence  contradiction by A32, A50, CQC_SIM1:18; ::_thesis: verum
end;
hence  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A22, A24, A25, A29, A33, A41, QC_LANG2:def_19; ::_thesis: verum
end;
hence  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A16; ::_thesis: verum
end;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A12);
then  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (len the PATH of q,p) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A10;
hence  ( JH, valH Al |= p iff CX |- p ) by A4, SUBSTUT2:def_5; ::_thesis: verum
end;

theorem Th16: :: GOEDELCP:16
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for n being Element of NAT st ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proof
let Al be QC-alphabet ; ::_thesis: for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for n being Element of NAT st ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let CX be Consistent Subset of (CQC-WFF Al); ::_thesis: for JH being Henkin_interpretation of CX
for n being Element of NAT st ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let JH be Henkin_interpretation of CX; ::_thesis: for n being Element of NAT st ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let n be Element of NAT ; ::_thesis: ( ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) implies for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) )
assume A1: for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ; ::_thesis: for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let p be Element of CQC-WFF Al; ::_thesis: ( QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples implies ( JH, valH Al |= p iff CX |- p ) )
assume that
A2: QuantNbr p <= n + 1 and
A3: CX is negation_faithful and
A4: CX is with_examples ; ::_thesis: ( JH, valH Al |= p iff CX |- p )
A5: ( QuantNbr p <= n implies ( JH, valH Al |= p iff CX |- p ) ) by A1, A3, A4;
now__::_thesis:_(_QuantNbr_p_=_n_+_1_implies_(_JH,_valH_Al_|=_p_iff_CX_|-_p_)_)
assume A6: QuantNbr p = n + 1 ; ::_thesis: ( JH, valH Al |= p iff CX |- p )
then consider q being Element of CQC-WFF Al 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 the PATH of q,p by A7, SUBSTUT2:def_5;
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len the PATH of q,p implies ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . $1 & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) );
A10: S1[ 0 ] ;
A11: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A12: S1[k] ; ::_thesis: S1[k + 1]
assume that
A13: 1 <= k + 1 and
A14: k + 1 <= len the PATH of q,p ; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
set j = k + 1;
A15: now__::_thesis:_(_k_=_0_implies_ex_q,_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)
assume  k = 0 ; ::_thesis: ex q, p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
then A16: the PATH of q,p . (k + 1) = q by A7, SUBSTUT2:def_5;
take q = q; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
 ( JH, valH Al |= q iff CX |- q ) by A3, A4, A8, Th15;
hence  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A16; ::_thesis: verum
end;
now__::_thesis:_(_k_<>_0_implies_ex_s,_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)
assume  k <> 0 ; ::_thesis: ex s, p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
then  0 < k by NAT_1:3;
then A17: 0 + 1 <= k by NAT_1:13;
 k < len the PATH of q,p by A14, NAT_1:13;
then consider G1, H1 being Element of QC-WFF Al such that
A18: the PATH of q,p . k = G1 and
A19: the PATH of q,p . (k + 1) = H1 and
A20: G1 is_immediate_constituent_of H1 by A7, A17, SUBSTUT2:def_5;
consider p1 being Element of CQC-WFF Al such that
A21: QuantNbr q <= QuantNbr p1 and
A22: p1 = the PATH of q,p . k and
A23: ( CX |- p1 iff JH, valH Al |= p1 ) by A12, A14, A17, NAT_1:13;
A24: ex F3 being QC-formula of Al st
( F3 = the PATH of q,p . (k + 1) & 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 = s; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
A25: now__::_thesis:_(_s_=_'not'_p1_implies_ex_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)
assume A26: s = 'not' p1 ; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
then A27: QuantNbr q <= QuantNbr s by A21, CQC_SIM1:16;
 ( CX |- s iff JH, valH Al |= s ) by A3, A23, A26, Def1, HENMODEL:def_2, VALUAT_1:17;
hence  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A19, A27; ::_thesis: verum
end;
A28: QuantNbr s <= n + 1 by A6, A19, A24, SUBSTUT2:30;
A29: now__::_thesis:_(_ex_F1_being_QC-formula_of_Al_st_s_=_p1_'&'_F1_implies_ex_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)
given F1 being QC-formula of Al such that A30: s = p1 '&' F1 ; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
reconsider F1 = 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  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A19, A32; ::_thesis: verum
end;
A33: now__::_thesis:_(_ex_F1_being_QC-formula_of_Al_st_s_=_F1_'&'_p1_implies_ex_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)
given F1 being QC-formula of Al such that A34: s = F1 '&' p1 ; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
reconsider F1 = 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  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A19, A36; ::_thesis: verum
end;
now__::_thesis:_(_ex_x_being_bound_QC-variable_of_Al_st_s_=_All_(x,p1)_implies_ex_p1_being_Element_of_CQC-WFF_Al_st_
(_p1_=_the_PATH_of_q,p_._(k_+_1)_&_QuantNbr_q_<=_QuantNbr_p1_&_(_CX_|-_p1_implies_JH,_valH_Al_|=_p1_)_&_(_JH,_valH_Al_|=_p1_implies_CX_|-_p1_)_)_)
given x being bound_QC-variable of Al such that A37: s = All (x,p1) ; ::_thesis: ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- 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__::_thesis:_(_JH,_valH_Al_|=_Ex_(x,('not'_p1))_implies_CX_|-_Ex_(x,('not'_p1))_)
assume  JH, valH Al |= Ex (x,('not' p1)) ; ::_thesis: CX |- Ex (x,('not' p1))
then consider y being bound_QC-variable of Al 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; ::_thesis: verum
end;
now__::_thesis:_(_CX_|-_Ex_(x,('not'_p1))_implies_JH,_valH_Al_|=_Ex_(x,('not'_p1))_)
assume  CX |- Ex (x,('not' p1)) ; ::_thesis: JH, valH Al |= Ex (x,('not' p1))
then consider y being bound_QC-variable of Al 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; ::_thesis: verum
end;
then  ( JH, valH Al |= 'not' (Ex (x,('not' p1))) iff CX |- 'not' (Ex (x,('not' p1))) ) by A3, A41, Def1, HENMODEL:def_2, VALUAT_1:17;
then  ( JH, valH Al |= s iff CX |- s ) by A37, Th11, Th12;
hence  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A19, A40; ::_thesis: verum
end;
hence  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A18, A20, A22, A25, A29, A33, QC_LANG2:def_19; ::_thesis: verum
end;
hence  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A15; ::_thesis: verum
end;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A10, A11);
then  ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (len the PATH of q,p) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A9;
hence  ( JH, valH Al |= p iff CX |- p ) by A7, SUBSTUT2:def_5; ::_thesis: verum
end;
hence  ( JH, valH Al |= p iff CX |- p ) by A2, A5, NAT_1:8; ::_thesis: verum
end;

theorem Th17: :: GOEDELCP:17
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proof
let Al be QC-alphabet ; ::_thesis: for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let CX be Consistent Subset of (CQC-WFF Al); ::_thesis: for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let JH be Henkin_interpretation of CX; ::_thesis: for p being Element of CQC-WFF Al st CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
defpred S1[ 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 being Element of CQC-WFF Al st QuantNbr p <= 0 holds
S1[p] by Th8;
A2: for k being Element of NAT st ( for p being Element of CQC-WFF Al st QuantNbr p <= k holds
S1[p] ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= k + 1 holds
S1[p] by Th16;
thus  for p being Element of CQC-WFF Al holds S1[p] from SUBSTUT2:sch_2(A1, A2); ::_thesis: verum
end;

begin

theorem Th18: :: GOEDELCP:18
for Al being QC-alphabet st Al is countable holds
QC-WFF Al is countable
proof
let Al be QC-alphabet ; ::_thesis: ( Al is countable implies QC-WFF Al is countable )
assume A1: Al is countable ; ::_thesis: QC-WFF Al is countable
 QC-WFF Al is Al -closed by QC_LANG1:def_11;
then A2: QC-WFF Al is Subset of ([:NAT,(QC-symbols Al):] *) by QC_LANG1:def_10;
 ( [:NAT,(QC-symbols Al):] is non empty set & [:NAT,(QC-symbols Al):] is countable ) by QC_LANG1:5, A1;
then  [:NAT,(QC-symbols Al):] * is countable by CARD_4:13;
hence  QC-WFF Al is countable by A2; ::_thesis: verum
end;

definition
let Al be QC-alphabet ;
func ExCl Al ->  Subset of (CQC-WFF Al) means :Def3: :: GOEDELCP:def 3
 for a being set holds
( a in it iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) );
existence
 ex b1 being Subset of (CQC-WFF Al) st
for a being set holds
( a in b1 iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) )
proof
defpred S1[ set ] means  ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st $1 = Ex (x,p);
consider X being set  such that
A1: for a being set holds
( a in X iff ( a in CQC-WFF Al & S1[a] ) ) from XBOOLE_0:sch_1();
 for a being set st a in X holds
a in CQC-WFF Al by A1;
then reconsider X = X as Subset of (CQC-WFF Al) by TARSKI:def_3;
take  X ; ::_thesis: for a being set holds
( a in X iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) )
thus  for a being set holds
( a in X iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (CQC-WFF Al) st ( for a being set holds
( a in b1 iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) ) & ( for a being set holds
( a in b2 iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st $1 = Ex (x,p);
let A1, A2 be Subset of (CQC-WFF Al); ::_thesis: ( ( for a being set holds
( a in A1 iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) ) & ( for a being set holds
( a in A2 iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) ) implies A1 = A2 )
assume that
A2: for a being set holds
( a in A1 iff S1[a] ) and
A3: for a being set holds
( a in A2 iff S1[a] ) ; ::_thesis: A1 = A2
now__::_thesis:_for_a_being_set_holds_
(_a_in_A1_iff_a_in_A2_)
let a be set ; ::_thesis: ( a in A1 iff a in A2 )
 ( a in A1 iff S1[a] ) by A2;
hence  ( a in A1 iff a in A2 ) by A3; ::_thesis: verum
end;
hence  A1 = A2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines ExCl GOEDELCP:def_3_:_
 for Al being QC-alphabet
for b2 being Subset of (CQC-WFF Al) holds
( b2 = ExCl Al iff for a being set holds
( a in b2 iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) );

theorem Th19: :: GOEDELCP:19
for Al being QC-alphabet st Al is countable holds
CQC-WFF Al is countable
proof
let Al be QC-alphabet ; ::_thesis: ( Al is countable implies CQC-WFF Al is countable )
assume A1: Al is countable ; ::_thesis: CQC-WFF Al is countable
 QC-WFF Al is countable by Th18, A1;
hence  CQC-WFF Al is countable ; ::_thesis: verum
end;

theorem Th20: :: GOEDELCP:20
for Al being QC-alphabet st Al is countable holds
( not ExCl Al is empty & ExCl Al is countable )
proof
let Al be QC-alphabet ; ::_thesis: ( Al is countable implies ( not ExCl Al is empty & ExCl Al is countable ) )
assume A1: Al is countable ; ::_thesis: ( not ExCl Al is empty & ExCl Al is countable )
set x = the bound_QC-variable of Al;
set p = the Element of CQC-WFF Al;
set a = Ex ( the bound_QC-variable of Al, the Element of CQC-WFF Al);
 Ex ( the bound_QC-variable of Al, the Element of CQC-WFF Al) in ExCl Al by Def3;
hence  not ExCl Al is empty ; ::_thesis: ExCl Al is countable
 CQC-WFF Al is countable by Th19, A1;
hence  ExCl Al is countable ; ::_thesis: verum
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 ; ::_thesis: ( A is countable implies ex f being Function st
( dom f = NAT & A = rng f ) )
assume A1: A is countable ; ::_thesis: ex f being Function st
( dom f = NAT & A = rng f )
 A c= A ;
then consider F being Function of NAT,A such that
A2: A = rng F by A1, SUPINF_2:def_8;
 dom F = NAT by FUNCT_2:def_1;
hence  ex f being Function st
( dom f = NAT & A = rng f ) by A2; ::_thesis: verum
end;

definition
let Al be QC-alphabet ;
let p be Element of QC-WFF Al;
assume A1: p is existential ;
func Ex-bound_in p ->  bound_QC-variable of Al means :Def4: :: GOEDELCP:def 4
 ex q being Element of QC-WFF Al st p = Ex (it,q);
existence
 ex b1 being bound_QC-variable of Al ex q being Element of QC-WFF Al st p = Ex (b1,q) by A1, QC_LANG2:def_13;
uniqueness
 for b1, b2 being bound_QC-variable of Al st ex q being Element of QC-WFF Al st p = Ex (b1,q) & ex q being Element of QC-WFF Al st p = Ex (b2,q) holds
b1 = b2 by QC_LANG2:13;
end;

:: deftheorem Def4 defines Ex-bound_in GOEDELCP:def_4_:_
 for Al being QC-alphabet
for p being Element of QC-WFF Al st p is existential holds
for b3 being bound_QC-variable of Al holds
( b3 = Ex-bound_in p iff ex q being Element of QC-WFF Al st p = Ex (b3,q) );

definition
let Al be QC-alphabet ;
let p be Element of CQC-WFF Al;
assume B1: p is existential ;
func Ex-the_scope_of p ->  Element of CQC-WFF Al means :Def5: :: GOEDELCP:def 5
 ex x being bound_QC-variable of Al st p = Ex (x,it);
existence
 ex b1 being Element of CQC-WFF Al ex x being bound_QC-variable of Al st p = Ex (x,b1)
proof
consider x being bound_QC-variable of Al, F1 being QC-formula of Al such that
A1: p = Ex (x,F1) by B1, QC_LANG2:def_13;
 p = 'not' (All (x,('not' F1))) by A1, QC_LANG2:def_5;
then  All (x,('not' F1)) is Element of CQC-WFF Al by CQC_LANG:8;
then A2: 'not' F1 is Element of CQC-WFF Al by CQC_LANG:13;
take  F1 ; ::_thesis: ( F1 is Element of CQC-WFF Al & ex x being bound_QC-variable of Al st p = Ex (x,F1) )
thus  ( F1 is Element of CQC-WFF Al & ex x being bound_QC-variable of Al st p = Ex (x,F1) ) by A1, A2, CQC_LANG:8; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of CQC-WFF Al st ex x being bound_QC-variable of Al st p = Ex (x,b1) & ex x being bound_QC-variable of Al st p = Ex (x,b2) holds
b1 = b2 by QC_LANG2:13;
end;

:: deftheorem Def5 defines Ex-the_scope_of GOEDELCP:def_5_:_
 for Al being QC-alphabet
for p being Element of CQC-WFF Al st p is existential holds
for b3 being Element of CQC-WFF Al holds
( b3 = Ex-the_scope_of p iff ex x being bound_QC-variable of Al st p = Ex (x,b3) );

definition
let Al be QC-alphabet ;
let F be Function of NAT,(CQC-WFF Al);
let a be Element of NAT ;
func bound_in (F,a) ->  bound_QC-variable of Al means :Def6: :: GOEDELCP:def 6
 for p being Element of CQC-WFF Al st p = F . a holds
it = Ex-bound_in p;
existence
 ex b1 being bound_QC-variable of Al st
for p being Element of CQC-WFF Al st p = F . a holds
b1 = Ex-bound_in p
proof
reconsider p = F . a as Element of CQC-WFF Al ;
take  Ex-bound_in p ; ::_thesis: for p being Element of CQC-WFF Al st p = F . a holds
Ex-bound_in p = Ex-bound_in p
thus  for p being Element of CQC-WFF Al st p = F . a holds
Ex-bound_in p = Ex-bound_in p ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being bound_QC-variable of Al st ( for p being Element of CQC-WFF Al st p = F . a holds
b1 = Ex-bound_in p ) & ( for p being Element of CQC-WFF Al st p = F . a holds
b2 = Ex-bound_in p ) holds
b1 = b2
proof
let x1, x2 be bound_QC-variable of Al; ::_thesis: ( ( for p being Element of CQC-WFF Al st p = F . a holds
x1 = Ex-bound_in p ) & ( for p being Element of CQC-WFF Al st p = F . a holds
x2 = Ex-bound_in p ) implies x1 = x2 )
assume that
A1: for p being Element of CQC-WFF Al st p = F . a holds
x1 = Ex-bound_in p and
A2: for p being Element of CQC-WFF Al st p = F . a holds
x2 = Ex-bound_in p ; ::_thesis: x1 = x2
reconsider q = F . a as Element of CQC-WFF Al ;
 x1 = Ex-bound_in q by A1;
hence  x1 = x2 by A2; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines bound_in GOEDELCP:def_6_:_
 for Al being QC-alphabet
for F being Function of NAT,(CQC-WFF Al)
for a being Element of NAT
for b4 being bound_QC-variable of Al holds
( b4 = bound_in (F,a) iff for p being Element of CQC-WFF Al st p = F . a holds
b4 = Ex-bound_in p );

definition
let Al be QC-alphabet ;
let F be Function of NAT,(CQC-WFF Al);
let a be Element of NAT ;
func the_scope_of (F,a) ->  Element of CQC-WFF Al means :Def7: :: GOEDELCP:def 7
 for p being Element of CQC-WFF Al st p = F . a holds
it = Ex-the_scope_of p;
existence
 ex b1 being Element of CQC-WFF Al st
for p being Element of CQC-WFF Al st p = F . a holds
b1 = Ex-the_scope_of p
proof
reconsider p = F . a as Element of CQC-WFF Al ;
take  Ex-the_scope_of p ; ::_thesis: for p being Element of CQC-WFF Al st p = F . a holds
Ex-the_scope_of p = Ex-the_scope_of p
thus  for p being Element of CQC-WFF Al st p = F . a holds
Ex-the_scope_of p = Ex-the_scope_of p ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of CQC-WFF Al st ( for p being Element of CQC-WFF Al st p = F . a holds
b1 = Ex-the_scope_of p ) & ( for p being Element of CQC-WFF Al st p = F . a holds
b2 = Ex-the_scope_of p ) holds
b1 = b2
proof
let q1, q2 be Element of CQC-WFF Al; ::_thesis: ( ( for p being Element of CQC-WFF Al st p = F . a holds
q1 = Ex-the_scope_of p ) & ( for p being Element of CQC-WFF Al st p = F . a holds
q2 = Ex-the_scope_of p ) implies q1 = q2 )
assume that
A1: for p being Element of CQC-WFF Al st p = F . a holds
q1 = Ex-the_scope_of p and
A2: for p being Element of CQC-WFF Al st p = F . a holds
q2 = Ex-the_scope_of p ; ::_thesis: q1 = q2
reconsider q = F . a as Element of CQC-WFF Al ;
 q1 = Ex-the_scope_of q by A1;
hence  q1 = q2 by A2; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines the_scope_of GOEDELCP:def_7_:_
 for Al being QC-alphabet
for F being Function of NAT,(CQC-WFF Al)
for a being Element of NAT
for b4 being Element of CQC-WFF Al holds
( b4 = the_scope_of (F,a) iff for p being Element of CQC-WFF Al st p = F . a holds
b4 = Ex-the_scope_of p );

definition
let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
func still_not-bound_in X ->  Subset of (bound_QC-variables Al) equals :: GOEDELCP:def 8
 union  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  ;
coherence
 union  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  is Subset of (bound_QC-variables Al)
proof
set Y = union  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  ;
now__::_thesis:_for_a_being_set_st_a_in_union__{__(still_not-bound_in_p)_where_p_is_Element_of_CQC-WFF_Al_:_p_in_X__}__holds_
a_in_bound_QC-variables_Al
let a be set ; ::_thesis: ( a in union  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  implies a in bound_QC-variables Al )
assume  a in union  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  ; ::_thesis: a in bound_QC-variables Al
then consider b being set  such that
A1: ( a in b & b in  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  ) by TARSKI:def_4;
 ex p being Element of CQC-WFF Al st
( b = still_not-bound_in p & p in X ) by A1;
hence  a in bound_QC-variables Al by A1; ::_thesis: verum
end;
hence  union  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  is Subset of (bound_QC-variables Al) by TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines still_not-bound_in GOEDELCP:def_8_:_
 for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds still_not-bound_in X = union  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  ;

theorem Th21: :: GOEDELCP:21
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st p in X holds
X |- p
proof
let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st p in X holds
X |- p
let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al st p in X holds
X |- p
let p be Element of CQC-WFF Al; ::_thesis: ( p in X implies X |- p )
assume A1: p in X ; ::_thesis: X |- p
now__::_thesis:_for_a_being_set_st_a_in_rng_<*p*>_holds_
a_in_X
let a be set ; ::_thesis: ( a in rng <*p*> implies a in X )
assume  a in rng <*p*> ; ::_thesis: a in X
then  a in {p} by FINSEQ_1:38;
hence  a in X by A1, TARSKI:def_1; ::_thesis: verum
end;
then A2: rng <*p*> c= X by TARSKI:def_3;
 |- ((<*> (CQC-WFF Al)) ^ <*p*>) ^ <*p*> by CALCUL_2:21;
then  |- <*p*> ^ <*p*> by FINSEQ_1:34;
hence  X |- p by A2, HENMODEL:def_1; ::_thesis: verum
end;

theorem Th22: :: GOEDELCP:22
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( Ex-bound_in (Ex (x,p)) = x & Ex-the_scope_of (Ex (x,p)) = p )
proof
let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( Ex-bound_in (Ex (x,p)) = x & Ex-the_scope_of (Ex (x,p)) = p )
let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al holds
( Ex-bound_in (Ex (x,p)) = x & Ex-the_scope_of (Ex (x,p)) = p )
let x be bound_QC-variable of Al; ::_thesis: ( Ex-bound_in (Ex (x,p)) = x & Ex-the_scope_of (Ex (x,p)) = p )
 Ex (x,p) is existential by QC_LANG2:def_13;
hence  ( Ex-bound_in (Ex (x,p)) = x & Ex-the_scope_of (Ex (x,p)) = p ) by Def4, Def5; ::_thesis: verum
end;

theorem Th23: :: GOEDELCP:23
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds X |- VERUM Al
proof
let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) holds X |- VERUM Al
let X be Subset of (CQC-WFF Al); ::_thesis: X |- VERUM Al
set f = <*> (CQC-WFF Al);
A1: rng (<*> (CQC-WFF Al)) c= X by XBOOLE_1:2;
 |- (<*> (CQC-WFF Al)) ^ <*(VERUM Al)*> by HENMODEL:15;
hence  X |- VERUM Al by A1, HENMODEL:def_1; ::_thesis: verum
end;

theorem Th24: :: GOEDELCP:24
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds
( X |- 'not' (VERUM Al) iff X is Inconsistent )
proof
let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) holds
( X |- 'not' (VERUM Al) iff X is Inconsistent )
let X be Subset of (CQC-WFF Al); ::_thesis: ( X |- 'not' (VERUM Al) iff X is Inconsistent )
thus  ( X |- 'not' (VERUM Al) implies X is Inconsistent ) ::_thesis: ( X is Inconsistent implies X |- 'not' (VERUM Al) )
proof
assume A1: X |- 'not' (VERUM Al) ; ::_thesis: X is Inconsistent
 X |- VERUM Al by Th23;
hence  X is Inconsistent by A1, HENMODEL:def_2; ::_thesis: verum
end;
thus  ( X is Inconsistent implies X |- 'not' (VERUM Al) ) by HENMODEL:6; ::_thesis: verum
end;


theorem Th25: :: GOEDELCP:25
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for f, g being FinSequence of CQC-WFF Al st 0 < len f & |- f ^ <*p*> holds
|- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>
proof
let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al
for f, g being FinSequence of CQC-WFF Al st 0 < len f & |- f ^ <*p*> holds
|- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>
let p be Element of CQC-WFF Al; ::_thesis: for f, g being FinSequence of CQC-WFF Al st 0 < len f & |- f ^ <*p*> holds
|- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>
let f, g be FinSequence of CQC-WFF Al; ::_thesis: ( 0 < len f & |- f ^ <*p*> implies |- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*> )
assume that
A1: 0 < len f and
A2: |- f ^ <*p*> ; ::_thesis: |- (((Ant f) ^ g) ^ <*(Suc 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  |- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*> by A2, A3, CALCUL_1:36; ::_thesis: verum
end;

theorem Th26: :: GOEDELCP:26
for Al being QC-alphabet
for p being Element of CQC-WFF Al holds still_not-bound_in {p} = still_not-bound_in p
proof
let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al holds still_not-bound_in {p} = still_not-bound_in p
let p be Element of CQC-WFF Al; ::_thesis: still_not-bound_in {p} = still_not-bound_in p
A1: now__::_thesis:_for_a_being_set_st_a_in_still_not-bound_in_{p}_holds_
a_in_still_not-bound_in_p
let a be set ; ::_thesis: ( a in still_not-bound_in {p} implies a in still_not-bound_in p )
assume  a in still_not-bound_in {p} ; ::_thesis: a in still_not-bound_in p
then consider b being set  such that
A2: ( a in b & b in  {  (still_not-bound_in q) where q is Element of CQC-WFF Al : q in {p}  }  ) by TARSKI:def_4;
 ex q being Element of CQC-WFF Al 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; ::_thesis: verum
end;
now__::_thesis:_for_a_being_set_st_a_in_still_not-bound_in_p_holds_
a_in_still_not-bound_in_{p}
let a be set ; ::_thesis: ( a in still_not-bound_in p implies a in still_not-bound_in {p} )
assume A3: a in still_not-bound_in p ; ::_thesis: a in still_not-bound_in {p}
set b = still_not-bound_in p;
 p in {p} by TARSKI:def_1;
then  still_not-bound_in p in  {  (still_not-bound_in q) where q is Element of CQC-WFF Al : q in {p}  }  ;
hence  a in still_not-bound_in {p} by A3, TARSKI:def_4; ::_thesis: verum
end;
hence  still_not-bound_in {p} = still_not-bound_in p by A1, TARSKI:1; ::_thesis: verum
end;

theorem Th27: :: GOEDELCP:27
for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al) holds still_not-bound_in (X \/ Y) = (still_not-bound_in X) \/ (still_not-bound_in Y)
proof
let Al be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF Al) holds still_not-bound_in (X \/ Y) = (still_not-bound_in X) \/ (still_not-bound_in Y)
let X, Y be Subset of (CQC-WFF Al); ::_thesis: still_not-bound_in (X \/ Y) = (still_not-bound_in X) \/ (still_not-bound_in Y)
thus  still_not-bound_in (X \/ Y) c= (still_not-bound_in X) \/ (still_not-bound_in Y) :: according to XBOOLE_0:def_10 ::_thesis: (still_not-bound_in X) \/ (still_not-bound_in Y) c= still_not-bound_in (X \/ Y)
proof
set A =  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X \/ Y  }  ;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in still_not-bound_in (X \/ Y) or b in (still_not-bound_in X) \/ (still_not-bound_in Y) )
assume  b in still_not-bound_in (X \/ Y) ; ::_thesis: b in (still_not-bound_in X) \/ (still_not-bound_in Y)
then consider a being set  such that
A1: b in a and
A2: a in  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X \/ Y  }  by TARSKI:def_4;
consider p being Element of CQC-WFF Al such that
A3: a = still_not-bound_in p and
A4: p in X \/ Y by A2;
A5: now__::_thesis:_(_p_in_X_implies_b_in_(still_not-bound_in_X)_\/_(still_not-bound_in_Y)_)
assume  p in X ; ::_thesis: b in (still_not-bound_in X) \/ (still_not-bound_in Y)
then  a in  {  (still_not-bound_in q) where q is Element of CQC-WFF Al : q in X  }  by A3;
then A6: b in union  {  (still_not-bound_in q) where q is Element of CQC-WFF Al : 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  b in (still_not-bound_in X) \/ (still_not-bound_in Y) by A6; ::_thesis: verum
end;
now__::_thesis:_(_p_in_Y_implies_b_in_(still_not-bound_in_X)_\/_(still_not-bound_in_Y)_)
assume  p in Y ; ::_thesis: b in (still_not-bound_in X) \/ (still_not-bound_in Y)
then  a in  {  (still_not-bound_in q) where q is Element of CQC-WFF Al : q in Y  }  by A3;
then A7: b in union  {  (still_not-bound_in q) where q is Element of CQC-WFF Al : 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  b in (still_not-bound_in X) \/ (still_not-bound_in Y) by A7; ::_thesis: verum
end;
hence  b in (still_not-bound_in X) \/ (still_not-bound_in Y) by A4, A5, XBOOLE_0:def_3; ::_thesis: verum
end;
thus  (still_not-bound_in X) \/ (still_not-bound_in Y) c= still_not-bound_in (X \/ Y) ::_thesis: verum
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (still_not-bound_in X) \/ (still_not-bound_in Y) or b in still_not-bound_in (X \/ Y) )
assume A8: b in (still_not-bound_in X) \/ (still_not-bound_in Y) ; ::_thesis: b in still_not-bound_in (X \/ Y)
A9: now__::_thesis:_(_b_in_still_not-bound_in_X_implies_b_in_still_not-bound_in_(X_\/_Y)_)
assume  b in still_not-bound_in X ; ::_thesis: b in still_not-bound_in (X \/ Y)
then consider a being set  such that
A10: ( b in a & a in  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  ) by TARSKI:def_4;
A11: ex p being Element of CQC-WFF Al 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) where q is Element of CQC-WFF Al : q in X \/ Y  }  by A11;
hence  b in still_not-bound_in (X \/ Y) by A10, TARSKI:def_4; ::_thesis: verum
end;
now__::_thesis:_(_b_in_still_not-bound_in_Y_implies_b_in_still_not-bound_in_(X_\/_Y)_)
assume  b in still_not-bound_in Y ; ::_thesis: b in still_not-bound_in (X \/ Y)
then consider a being set  such that
A12: ( b in a & a in  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in Y  }  ) by TARSKI:def_4;
A13: ex p being Element of CQC-WFF Al 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) where q is Element of CQC-WFF Al : q in X \/ Y  }  by A13;
hence  b in still_not-bound_in (X \/ Y) by A12, TARSKI:def_4; ::_thesis: verum
end;
hence  b in still_not-bound_in (X \/ Y) by A8, A9, XBOOLE_0:def_3; ::_thesis: verum
end;
end;

theorem Th28: :: GOEDELCP:28
for Al being QC-alphabet
for A being Subset of (bound_QC-variables Al) st A is finite holds
ex x being bound_QC-variable of Al st not x in A
proof
let Al be QC-alphabet ; ::_thesis: for A being Subset of (bound_QC-variables Al) st A is finite holds
ex x being bound_QC-variable of Al st not x in A
let A be Subset of (bound_QC-variables Al); ::_thesis: ( A is finite implies ex x being bound_QC-variable of Al st not x in A )
A1: not bound_QC-variables Al is finite by CALCUL_1:64;
assume  A is finite ; ::_thesis: not for x being bound_QC-variable of Al holds x in A
then  not for b being set holds
( b in A iff b in bound_QC-variables Al ) by A1, TARSKI:1;
then consider b being set  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 ; ::_thesis: not x in A
thus  not x in A by A2; ::_thesis: verum
end;

theorem Th29: :: GOEDELCP:29
for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al) st X c= Y holds
still_not-bound_in X c= still_not-bound_in Y
proof
let Al be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF Al) st X c= Y holds
still_not-bound_in X c= still_not-bound_in Y
let X, Y be Subset of (CQC-WFF Al); ::_thesis: ( X c= Y implies still_not-bound_in X c= still_not-bound_in Y )
set A =  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  ;
assume A1: X c= Y ; ::_thesis: still_not-bound_in X c= still_not-bound_in Y
now__::_thesis:_for_a_being_set_st_a_in_still_not-bound_in_X_holds_
a_in_still_not-bound_in_Y
let a be set ; ::_thesis: ( a in still_not-bound_in X implies a in still_not-bound_in Y )
assume  a in still_not-bound_in X ; ::_thesis: a in still_not-bound_in Y
then consider b being set  such that
A2: a in b and
A3: b in  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  by TARSKI:def_4;
 ex p being Element of CQC-WFF Al st
( b = still_not-bound_in p & p in X ) by A3;
then  b in  {  (still_not-bound_in q) where q is Element of CQC-WFF Al : q in Y  }  by A1;
hence  a in still_not-bound_in Y by A2, TARSKI:def_4; ::_thesis: verum
end;
hence  still_not-bound_in X c= still_not-bound_in Y by TARSKI:def_3; ::_thesis: verum
end;

theorem Th30: :: GOEDELCP:30
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds still_not-bound_in (rng f) = still_not-bound_in f
proof
let Al be QC-alphabet ; ::_thesis: for f being FinSequence of CQC-WFF Al holds still_not-bound_in (rng f) = still_not-bound_in f
let f be FinSequence of CQC-WFF Al; ::_thesis: still_not-bound_in (rng f) = still_not-bound_in f
set A =  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in rng f  }  ;
A1: now__::_thesis:_for_a_being_set_st_a_in_still_not-bound_in_(rng_f)_holds_
a_in_still_not-bound_in_f
let a be set ; ::_thesis: ( a in still_not-bound_in (rng f) implies a in still_not-bound_in f )
assume  a in still_not-bound_in (rng f) ; ::_thesis: a in still_not-bound_in f
then consider b being set  such that
A2: a in b and
A3: b in  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in rng f  }  by TARSKI:def_4;
consider p being Element of CQC-WFF Al such that
A4: b = still_not-bound_in p and
A5: p in rng f by A3;
 ex c being set 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; ::_thesis: verum
end;
now__::_thesis:_for_a_being_set_st_a_in_still_not-bound_in_f_holds_
a_in_still_not-bound_in_(rng_f)
let a be set ; ::_thesis: ( a in still_not-bound_in f implies a in still_not-bound_in (rng f) )
assume  a in still_not-bound_in f ; ::_thesis: a in still_not-bound_in (rng f)
then consider i being Element of NAT , q being Element of CQC-WFF Al 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  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in rng f  }  ;
hence  a in still_not-bound_in (rng f) by A8, TARSKI:def_4; ::_thesis: verum
end;
hence  still_not-bound_in (rng f) = still_not-bound_in f by A1, TARSKI:1; ::_thesis: verum
end;

theorem Th31: :: GOEDELCP:31
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & still_not-bound_in CX is finite holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples )
proof
let Al be QC-alphabet ; ::_thesis: for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & still_not-bound_in CX is finite holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples )
let CX be Consistent Subset of (CQC-WFF Al); ::_thesis: ( Al is countable & still_not-bound_in CX is finite implies ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples ) )
assume A1: Al is countable ; ::_thesis: ( not still_not-bound_in CX is finite or ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples ) )
assume A2: still_not-bound_in CX is finite ; ::_thesis: ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples )
 ( not ExCl Al is 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 = f as Function of NAT,(CQC-WFF Al) by A3, A4, FUNCT_2:2;
defpred S1[ Element of NAT , set , set ] means  ex K, L being Subset of (bound_QC-variables Al) 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 where t is QC-symbol of Al : 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 where u is QC-symbol of Al : not x. u in L  }  )))))))] );
A5: for n being Element of NAT
for C being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] ex D being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] st S1[n,C,D]
proof
let n be Element of NAT ; ::_thesis: for C being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] ex D being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] st S1[n,C,D]
let C be Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]; ::_thesis: ex D being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] st S1[n,C,D]
set K = C `2 ;
 ex a, b being set st
( a in CQC-WFF Al & b in bool (bound_QC-variables Al) & C = [a,b] ) by ZFMISC_1:def_2;
then reconsider K = C `2 as Subset of (bound_QC-variables Al) by MCART_1:7;
set L = K \/ (still_not-bound_in {(f . (n + 1))});
set D = [(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (n + 1))})  }  ))))),(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 where u is QC-symbol of Al : not x. u in K \/ (still_not-bound_in {(f . (n + 1))})  }  )))))))];
take  [(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (n + 1))})  }  ))))),(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 where u is QC-symbol of Al : not x. u in K \/ (still_not-bound_in {(f . (n + 1))})  }  )))))))] ; ::_thesis: S1[n,C,[(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (n + 1))})  }  ))))),(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 where u is QC-symbol of Al : not x. u in K \/ (still_not-bound_in {(f . (n + 1))})  }  )))))))]]
thus  S1[n,C,[(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (n + 1))})  }  ))))),(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 where u is QC-symbol of Al : not x. u in K \/ (still_not-bound_in {(f . (n + 1))})  }  )))))))]] ; ::_thesis: verum
end;
reconsider A = [(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in  {  u where u is QC-symbol of Al : 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 where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)})  }  )))))}))] as Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] ;
consider h being Function of NAT,[:(CQC-WFF Al),(bool (bound_QC-variables Al)):] such that
A6: ( h . 0 = A & ( for n being Element of NAT holds S1[n,h . n,h . (n + 1)] ) ) from RECDEF_1:sch_2(A5);
set CY = CX \/  {  ((h . n) `1) where n is Element of NAT : verum  }  ;
now__::_thesis:_for_a_being_set_st_a_in_CX_\/__{__((h_._n)_`1)_where_n_is_Element_of_NAT_:_verum__}__holds_
a_in_CQC-WFF_Al
let a be set ; ::_thesis: ( a in CX \/  {  ((h . n) `1) where n is Element of NAT : verum  }  implies a in CQC-WFF Al )
assume A7: a in CX \/  {  ((h . n) `1) where n is Element of NAT : verum  }  ; ::_thesis: a in CQC-WFF Al
now__::_thesis:_(_not_a_in_CX_implies_a_in_CQC-WFF_Al_)
assume  not a in CX ; ::_thesis: a in CQC-WFF Al
then  a in  {  ((h . n) `1) where n is Element of NAT : verum  }  by A7, XBOOLE_0:def_3;
then consider n being Element of NAT  such that
A8: a = (h . n) `1 ;
 ex c, d being set st
( c in CQC-WFF Al & d in bool (bound_QC-variables Al) & h . n = [c,d] ) by ZFMISC_1:def_2;
hence  a in CQC-WFF Al by A8, MCART_1:7; ::_thesis: verum
end;
hence  a in CQC-WFF Al ; ::_thesis: verum
end;
then reconsider CY = CX \/  {  ((h . n) `1) where n is Element of NAT : verum  }  as Subset of (CQC-WFF Al) by TARSKI:def_3;
A9: now__::_thesis:_for_x_being_bound_QC-variable_of_Al
for_p_being_Element_of_CQC-WFF_Al_ex_y_being_bound_QC-variable_of_Al_st_CY_|-_('not'_(Ex_(x,p)))_'or'_(p_._(x,y))
let x be bound_QC-variable of Al; ::_thesis: for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
let p be Element of CQC-WFF Al; ::_thesis: ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
 Ex (x,p) in ExCl Al by Def3;
then consider a being set  such that
A10: a in dom f and
A11: f . a = Ex (x,p) by A4, FUNCT_1:def_3;
reconsider a = a as Element of NAT by A10;
reconsider r9 = f . a as Element of CQC-WFF Al ;
A12: Ex-bound_in r9 = x by A11, Th22;
A13: Ex-the_scope_of r9 = p by A11, Th22;
A14: bound_in (f,a) = x by A12, Def6;
A15: the_scope_of (f,a) = p by A13, Def7;
A16: (h . a) `1 in  {  ((h . n) `1) where n is Element of NAT : verum  }  ;
A17:  {  ((h . n) `1) where n is Element of NAT : verum  }  c= CY by XBOOLE_1:7;
A18: now__::_thesis:_(_a_=_0_implies_ex_y_being_Element_of_bound_QC-variables_Al_st_CY_|-_('not'_(Ex_(x,p)))_'or'_(p_._(x,y))_)
assume A19: a = 0 ; ::_thesis: ex y being Element of bound_QC-variables Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
take y = x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {r9})  }  ); ::_thesis: CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
 (h . a) `1 = ('not' r9) 'or' ((the_scope_of (f,a)) . ((bound_in (f,a)),y)) by A6, A19, MCART_1:7;
hence  CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A11, A14, A15, A16, A17, Th21; ::_thesis: verum
end;
now__::_thesis:_(_a_<>_0_implies_ex_y_being_Element_of_bound_QC-variables_Al_st_CY_|-_('not'_(Ex_(x,p)))_'or'_(p_._(x,y))_)
assume  a <> 0 ; ::_thesis: ex y being Element of bound_QC-variables Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
then consider m being natural number  such that
A20: a = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A21: ex K, L being Subset of (bound_QC-variables Al) 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 where t is QC-symbol of Al : 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 where u is QC-symbol of Al : not x. u in L  }  )))))))] ) by A6, A20;
set K = (h . m) `2 ;
set L = (still_not-bound_in {r9}) \/ ((h . m) `2);
take y = x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in (still_not-bound_in {r9}) \/ ((h . m) `2)  }  ); ::_thesis: CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
 (h . a) `1 = ('not' r9) 'or' ((the_scope_of (f,a)) . ((bound_in (f,a)),y)) by A21, MCART_1:7;
hence  CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A11, A14, A15, A16, A17, Th21; ::_thesis: verum
end;
hence  ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A18; ::_thesis: verum
end;
deffunc H1( set ) ->  set = CX \/  {  ((h . n) `1) where n is Element of NAT : n in $1  }  ;
consider F being Function such that
A22: ( dom F = NAT & ( for a being set st a in NAT holds
F . a = H1(a) ) ) from FUNCT_1:sch_3();
A23: CY c= union (rng F)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CY or a in union (rng F) )
assume A24: a in CY ; ::_thesis: a in union (rng F)
A25: now__::_thesis:_(_a_in_CX_implies_a_in_union_(rng_F)_)
assume A26: a in CX ; ::_thesis: a in union (rng F)
A27: F . 0 = CX \/  {  ((h . n) `1) where n is Element of NAT : n in 0  }  by A22;
now__::_thesis:_for_b_being_set_holds_not_b_in__{__((h_._n)_`1)_where_n_is_Element_of_NAT_:_n_in_0__}_
let b be set ; ::_thesis: not b in  {  ((h . n) `1) where n is Element of NAT : n in 0  }
assume  b in  {  ((h . n) `1) where n is Element of NAT : n in 0  }  ; ::_thesis: contradiction
then  ex n being Element of NAT st
( b = (h . n) `1 & n in 0 ) ;
hence  contradiction ; ::_thesis: verum
end;
then A28:  {  ((h . n) `1) where n is Element of NAT : n in 0  }  = {} by XBOOLE_0:def_1;
 F . 0 in rng F by A22, FUNCT_1:3;
hence  a in union (rng F) by A26, A27, A28, TARSKI:def_4; ::_thesis: verum
end;
now__::_thesis:_(_a_in__{__((h_._n)_`1)_where_n_is_Element_of_NAT_:_verum__}__implies_a_in_union_(rng_F)_)
assume  a in  {  ((h . n) `1) where n is Element of NAT : verum  }  ; ::_thesis: a in union (rng F)
then consider n being Element of NAT  such that
A29: a = (h . n) `1 ;
 n < n + 1 by NAT_1:13;
then  n in n + 1 by NAT_1:44;
then A30: a in  {  ((h . m) `1) where m is Element of NAT : m in n + 1  }  by A29;
 F . (n + 1) = CX \/  {  ((h . m) `1) where m is Element of NAT : m in n + 1  }  by A22;
then A31:  {  ((h . m) `1) where m is Element of NAT : m in n + 1  }  c= F . (n + 1) by XBOOLE_1:7;
 F . (n + 1) in rng F by A22, FUNCT_1:3;
hence  a in union (rng F) by A30, A31, TARSKI:def_4; ::_thesis: verum
end;
hence  a in union (rng F) by A24, A25, XBOOLE_0:def_3; ::_thesis: verum
end;
 union (rng F) c= CY
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union (rng F) or a in CY )
assume  a in union (rng F) ; ::_thesis: a in CY
then consider b being set  such that
A32: a in b and
A33: b in rng F by TARSKI:def_4;
consider c being set  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) where m is Element of NAT : m in n  }  by A22, A32, A35;
A37: now__::_thesis:_(_a_in_CX_implies_a_in_CY_)
assume A38: a in CX ; ::_thesis: a in CY
 CX c= CY by XBOOLE_1:7;
hence  a in CY by A38; ::_thesis: verum
end;
now__::_thesis:_(_a_in__{__((h_._m)_`1)_where_m_is_Element_of_NAT_:_m_in_n__}__implies_a_in_CY_)
assume  a in  {  ((h . m) `1) where m is Element of NAT : m in n  }  ; ::_thesis: a in CY
then  ex m being Element of NAT st
( a = (h . m) `1 & m in n ) ;
then A39: a in  {  ((h . i) `1) where i is Element of NAT : verum  }  ;
  {  ((h . i) `1) where i is Element of NAT : verum  }  c= CY by XBOOLE_1:7;
hence  a in CY by A39; ::_thesis: verum
end;
hence  a in CY by A36, A37, XBOOLE_0:def_3; ::_thesis: verum
end;
then A40: CY = union (rng F) by A23, XBOOLE_0:def_10;
A41: for n, m being Element of NAT st m in dom F & n in dom F & n < m holds
F . n c= F . m
proof
let n, m be Element of NAT ; ::_thesis: ( m in dom F & n in dom F & n < m implies F . n c= F . m )
assume that
 m in dom F and
 n in dom F and
A42: n < m ; ::_thesis: F . n c= F . m
A43: F . n = CX \/  {  ((h . i) `1) where i is Element of NAT : i in n  }  by A22;
A44: F . m = CX \/  {  ((h . i) `1) where i is Element of NAT : i in m  }  by A22;
now__::_thesis:_for_a_being_set_st_a_in_F_._n_holds_
a_in_F_._m
let a be set ; ::_thesis: ( a in F . n implies a in F . m )
assume A45: a in F . n ; ::_thesis: a in F . m
A46: now__::_thesis:_(_a_in_CX_implies_a_in_F_._m_)
assume A47: a in CX ; ::_thesis: a in F . m
 CX c= F . m by A44, XBOOLE_1:7;
hence  a in F . m by A47; ::_thesis: verum
end;
now__::_thesis:_(_a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_n__}__implies_a_in_F_._m_)
assume  a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  ; ::_thesis: a in F . m
then consider i being Element of NAT  such that
A48: (h . i) `1 = a and
A49: i in n ;
 i < n by A49, NAT_1:44;
then  i < m by A42, XXREAL_0:2;
then  i in m by NAT_1:44;
then A50: a in  {  ((h . j) `1) where j is Element of NAT : j in m  }  by A48;
  {  ((h . j) `1) where j is Element of NAT : j in m  }  c= F . m by A44, XBOOLE_1:7;
hence  a in F . m by A50; ::_thesis: verum
end;
hence  a in F . m by A43, A45, A46, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  F . n c= F . m by TARSKI:def_3; ::_thesis: verum
end;
 rng F c= bool (CQC-WFF Al)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng F or a in bool (CQC-WFF Al) )
assume  a in rng F ; ::_thesis: a in bool (CQC-WFF Al)
then consider b being set  such that
A51: b in dom F and
A52: F . b = a by FUNCT_1:def_3;
reconsider b = b as Element of NAT by A22, A51;
A53: F . b = CX \/  {  ((h . i) `1) where i is Element of NAT : i in b  }  by A22;
now__::_thesis:_for_c_being_set_st_c_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_b__}__holds_
c_in_CQC-WFF_Al
let c be set ; ::_thesis: ( c in  {  ((h . i) `1) where i is Element of NAT : i in b  }  implies c in CQC-WFF Al )
assume  c in  {  ((h . i) `1) where i is Element of NAT : i in b  }  ; ::_thesis: c in CQC-WFF Al
then  ex i being Element of NAT st
( (h . i) `1 = c & i in b ) ;
hence  c in CQC-WFF Al by MCART_1:10; ::_thesis: verum
end;
then   {  ((h . i) `1) where i is Element of NAT : i in b  }  c= CQC-WFF Al by TARSKI:def_3;
then  F . b c= CQC-WFF Al by A53, XBOOLE_1:8;
hence  a in bool (CQC-WFF Al) by A52; ::_thesis: verum
end;
then reconsider F = F as Function of NAT,(bool (CQC-WFF Al)) by A22, FUNCT_2:2;
A54: for n being Element of NAT holds F . (n + 1) = (F . n) \/ {((h . n) `1)}
proof
let n be Element of NAT ; ::_thesis: F . (n + 1) = (F . n) \/ {((h . n) `1)}
now__::_thesis:_for_a_being_set_st_a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_n_+_1__}__holds_
a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_n__}__\/_{((h_._n)_`1)}
let a be set ; ::_thesis: ( a in  {  ((h . i) `1) where i is Element of NAT : i in n + 1  }  implies a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} )
assume  a in  {  ((h . i) `1) where i is Element of NAT : i in n + 1  }  ; ::_thesis: a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)}
then consider j being Element of NAT  such that
A55: a = (h . j) `1 and
A56: j in n + 1 ;
 j < n + 1 by A56, NAT_1:44;
then A57: j + 1 <= n + 1 by NAT_1:13;
A58: now__::_thesis:_(_j_+_1_=_n_+_1_implies_a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_n__}__\/_{((h_._n)_`1)}_)
assume  j + 1 = n + 1 ; ::_thesis: a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)}
then A59: a in {((h . n) `1)} by A55, TARSKI:def_1;
 {((h . n) `1)} c=  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} by XBOOLE_1:7;
hence  a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} by A59; ::_thesis: verum
end;
now__::_thesis:_(_j_+_1_<=_n_implies_a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_n__}__\/_{((h_._n)_`1)}_)
assume  j + 1 <= n ; ::_thesis: a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)}
then  j < n by NAT_1:13;
then  j in n by NAT_1:44;
then A60: a in  {  ((h . k) `1) where k is Element of NAT : k in n  }  by A55;
  {  ((h . k) `1) where k is Element of NAT : k in n  }  c=  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} by XBOOLE_1:7;
hence  a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} by A60; ::_thesis: verum
end;
hence  a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} by A57, A58, NAT_1:8; ::_thesis: verum
end;
then A61:  {  ((h . k) `1) where k is Element of NAT : k in n + 1  }  c=  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} by TARSKI:def_3;
now__::_thesis:_for_a_being_set_st_a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_n__}__\/_{((h_._n)_`1)}_holds_
a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_n_+_1__}_
let a be set ; ::_thesis: ( a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} implies a in  {  ((h . i) `1) where i is Element of NAT : i in n + 1  }  )
assume A62: a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} ; ::_thesis: a in  {  ((h . i) `1) where i is Element of NAT : i in n + 1  }
A63: now__::_thesis:_(_a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_n__}__implies_a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_n_+_1__}__)
assume  a in  {  ((h . i) `1) where i is Element of NAT : i in n  }  ; ::_thesis: a in  {  ((h . i) `1) where i is Element of NAT : i in n + 1  }
then consider j being Element of NAT  such that
A64: (h . j) `1 = a and
A65: j in n ;
A66: n <= n + 1 by NAT_1:11;
 j < n by A65, NAT_1:44;
then  j < n + 1 by A66, XXREAL_0:2;
then  j in n + 1 by NAT_1:44;
hence  a in  {  ((h . i) `1) where i is Element of NAT : i in n + 1  }  by A64; ::_thesis: verum
end;
now__::_thesis:_(_a_in_{((h_._n)_`1)}_implies_a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_n_+_1__}__)
assume  a in {((h . n) `1)} ; ::_thesis: a in  {  ((h . i) `1) where i is Element of NAT : i in n + 1  }
then A67: a = (h . n) `1 by TARSKI:def_1;
 n < n + 1 by NAT_1:13;
then  n in n + 1 by NAT_1:44;
hence  a in  {  ((h . i) `1) where i is Element of NAT : i in n + 1  }  by A67; ::_thesis: verum
end;
hence  a in  {  ((h . i) `1) where i is Element of NAT : i in n + 1  }  by A62, A63, XBOOLE_0:def_3; ::_thesis: verum
end;
then   {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} c=  {  ((h . k) `1) where k is Element of NAT : k in n + 1  }  by TARSKI:def_3;
then   {  ((h . i) `1) where i is Element of NAT : i in n  }  \/ {((h . n) `1)} =  {  ((h . k) `1) where k is Element of NAT : k in n + 1  }  by A61, XBOOLE_0:def_10;
then  F . (n + 1) = CX \/ ( {  ((h . k) `1) where k is Element of NAT : k in n  }  \/ {((h . n) `1)}) by A22;
then  F . (n + 1) = (CX \/  {  ((h . k) `1) where k is Element of NAT : k in n  }  ) \/ {((h . n) `1)} by XBOOLE_1:4;
hence  F . (n + 1) = (F . n) \/ {((h . n) `1)} by A22; ::_thesis: verum
end;
defpred S2[ Element of NAT ] means ( (h . $1) `2 is finite & (h . $1) `2 is Subset of (bound_QC-variables Al) );
A68: S2[ 0 ]
proof
A69: (h . 0) `2 = still_not-bound_in (CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)})  }  )))))}) by A6, MCART_1:7;
reconsider s = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in  {  t where t is QC-symbol of Al : 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  S2[ 0 ] by A69, Th27; ::_thesis: verum
end;
A70: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A71: S2[k] ; ::_thesis: S2[k + 1]
A72: ex K, L being Subset of (bound_QC-variables Al) 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 where t is QC-symbol of Al : 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 where u is QC-symbol of Al : not x. u in L  }  )))))))] ) by A6;
set K = (h . k) `2 ;
reconsider K = (h . k) `2 as Subset of (bound_QC-variables Al) by A71;
set L = K \/ (still_not-bound_in {(f . (k + 1))});
set s = ('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))})  }  ))));
 still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))})  }  ))))) is finite by CQC_SIM1:19;
hence  S2[k + 1] by A71, A72, MCART_1:7; ::_thesis: verum
end;
A73: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A68, A70);
defpred S3[ Element of NAT ] means ( still_not-bound_in (F . ($1 + 1)) c= (h . $1) `2 & not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in (still_not-bound_in {(f . ($1 + 1))}) \/ ((h . $1) `2)  }  ) in still_not-bound_in ((F . ($1 + 1)) \/ {(f . ($1 + 1))}) );
A74: for k being Element of NAT holds
( still_not-bound_in (F . (k + 1)) c= (h . k) `2 & not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in (still_not-bound_in {(f . (k + 1))}) \/ ((h . k) `2)  }  ) in still_not-bound_in ((F . (k + 1)) \/ {(f . (k + 1))}) )
proof
A75: S3[ 0 ]
proof
set r = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)})  }  ))));
set A1 = {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)})  }  )))))};
reconsider s = f . 1 as Element of CQC-WFF Al ;
A76: (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 where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)})  }  )))))}) by A6, MCART_1:7;
reconsider B = (h . 0) `2 as Subset of (bound_QC-variables Al) by A6, MCART_1:7;
reconsider C = (still_not-bound_in {s}) \/ B as Element of bool (bound_QC-variables Al) ;
 still_not-bound_in s is finite by CQC_SIM1:19;
then  still_not-bound_in {s} is finite by Th26;
then consider x being bound_QC-variable of Al such that
A77: not x in C by A68, Th28;
consider u being QC-symbol of Al such that
A78: x. u = x by QC_LANG3:30;
 u in  {  t where t is QC-symbol of Al : not x. t in C  }  by A77, A78;
then reconsider A =  {  t where t is QC-symbol of Al : not x. t in C  }  as non empty set ;
now__::_thesis:_for_a_being_set_st_a_in_A_holds_
a_in_QC-symbols_Al
let a be set ; ::_thesis: ( a in A implies a in QC-symbols Al )
assume  a in A ; ::_thesis: a in QC-symbols Al
then  ex t being QC-symbol of Al st
( a = t & not x. t in C ) ;
hence  a in QC-symbols Al ; ::_thesis: verum
end;
then reconsider A =  {  t where t is QC-symbol of Al : not x. t in C  }  as non empty Subset of (QC-symbols Al) by TARSKI:def_3;
set u = Al -one_in A;
 Al -one_in A = the Element of A by QC_LANG1:def_41;
then  Al -one_in A in A ;
then A79: ex t being QC-symbol of Al st
( t = Al -one_in A & not x. t in C ) ;
A80: F . 0 = CX \/  {  ((h . n) `1) where n is Element of NAT : n in 0  }  by A22;
now__::_thesis:_for_b_being_set_holds_not_b_in__{__((h_._n)_`1)_where_n_is_Element_of_NAT_:_n_in_0__}_
let b be set ; ::_thesis: not b in  {  ((h . n) `1) where n is Element of NAT : n in 0  }
assume  b in  {  ((h . n) `1) where n is Element of NAT : n in 0  }  ; ::_thesis: contradiction
then  ex n being Element of NAT st
( b = (h . n) `1 & n in 0 ) ;
hence  contradiction ; ::_thesis: verum
end;
then A81:  {  ((h . n) `1) where n is Element of NAT : n in 0  }  = {} by XBOOLE_0:def_1;
 (h . 0) `1 = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)})  }  )))) by A6, MCART_1:7;
then  F . (0 + 1) = CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)})  }  )))))} by A54, A80, A81;
hence  S3[ 0 ] by A76, A79, Th27; ::_thesis: verum
end;
A82: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
assume A83: S3[k] ; ::_thesis: S3[k + 1]
reconsider s = f . (k + 2) as Element of CQC-WFF Al ;
A84: ex K, L being Subset of (bound_QC-variables Al) 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 where t is QC-symbol of Al : 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 where u is QC-symbol of Al : not x. u in L  }  )))))))] ) by A6;
set K = (h . k) `2 ;
reconsider K = (h . k) `2 as Subset of (bound_QC-variables Al) by A73;
set L = K \/ (still_not-bound_in {(f . (k + 1))});
set r = ('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))})  }  ))));
A85: (h . (k + 1)) `1 = ('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))})  }  )))) by A84, MCART_1:7;
A86: (h . (k + 1)) `2 = 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  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))})  }  )))))) by A84, MCART_1:7;
reconsider B = (h . (k + 1)) `2 as Subset of (bound_QC-variables Al) by A84, MCART_1:7;
reconsider C = (still_not-bound_in {s}) \/ B as Element of bool (bound_QC-variables Al) ;
 still_not-bound_in s is finite by CQC_SIM1:19;
then A87: still_not-bound_in {s} is finite by Th26;
 (h . (k + 1)) `2 is finite by A73;
then consider x being bound_QC-variable of Al such that
A88: not x in C by A87, Th28;
consider u being QC-symbol of Al such that
A89: x. u = x by QC_LANG3:30;
 u in  {  t where t is QC-symbol of Al : not x. t in (still_not-bound_in {s}) \/ B  }  by A88, A89;
then reconsider A =  {  t where t is QC-symbol of Al : not x. t in (still_not-bound_in {s}) \/ B  }  as non empty set ;
now__::_thesis:_for_a_being_set_st_a_in_A_holds_
a_in_QC-symbols_Al
let a be set ; ::_thesis: ( a in A implies a in QC-symbols Al )
assume  a in A ; ::_thesis: a in QC-symbols Al
then  ex t being QC-symbol of Al st
( a = t & not x. t in C ) ;
hence  a in QC-symbols Al ; ::_thesis: verum
end;
then reconsider A =  {  t where t is QC-symbol of Al : 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;
 Al -one_in A = the Element of A by QC_LANG1:def_41;
then  Al -one_in A in A ;
then A90: ex t being QC-symbol of Al st
( t = Al -one_in A & not x. t in C ) ;
then A91: not x. (Al -one_in A) in still_not-bound_in {s} by XBOOLE_0:def_3;
 (still_not-bound_in (F . (k + 1))) \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))})  }  )))))) c= B by A83, A86, XBOOLE_1:9;
then  (still_not-bound_in (F . (k + 1))) \/ (still_not-bound_in {(('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))})  }  )))))}) c= B by Th26;
then A92: still_not-bound_in ((F . (k + 1)) \/ {(('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))})  }  )))))}) c= B by Th27;
then  still_not-bound_in (F . ((k + 1) + 1)) c= B by A54, A85;
then  not x. (Al -one_in A) in still_not-bound_in (F . ((k + 1) + 1)) by A90, XBOOLE_0:def_3;
then  not x. (Al -one_in A) in (still_not-bound_in (F . ((k + 1) + 1))) \/ (still_not-bound_in {s}) by A91, XBOOLE_0:def_3;
hence  S3[k + 1] by A54, A85, A92, Th27; ::_thesis: verum
end;
 for k being Element of NAT holds S3[k] from NAT_1:sch_1(A75, A82);
hence  for k being Element of NAT holds
( still_not-bound_in (F . (k + 1)) c= (h . k) `2 & not x. (Al -one_in  {  t where t is QC-symbol of Al : 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))}) ) ; ::_thesis: verum
end;
defpred S4[ Element of NAT ] means F . $1 is Consistent ;
now__::_thesis:_for_a_being_set_holds_not_a_in__{__((h_._i)_`1)_where_i_is_Element_of_NAT_:_i_in_0__}_
let a be set ; ::_thesis: not a in  {  ((h . i) `1) where i is Element of NAT : i in 0  }
assume  a in  {  ((h . i) `1) where i is Element of NAT : i in 0  }  ; ::_thesis: contradiction
then  ex j being Element of NAT st
( a = (h . j) `1 & j in 0 ) ;
hence  contradiction ; ::_thesis: verum
end;
then   {  ((h . i) `1) where i is Element of NAT : i in 0  }  = {} by XBOOLE_0:def_1;
then A93: F . 0 = CX \/ {} by A22;
then A94: S4[ 0 ] ;
A95: for k being Element of NAT st S4[k] holds
S4[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S4[k] implies S4[k + 1] )
assume A96: S4[k] ; ::_thesis: S4[k + 1]
 ex c, d being set st
( c in CQC-WFF Al & d in bool (bound_QC-variables Al) & h . k = [c,d] ) by ZFMISC_1:def_2;
then reconsider r = (h . k) `1 as Element of CQC-WFF Al by MCART_1:7;
now__::_thesis:_not_F_._(k_+_1)_is_Inconsistent
assume  F . (k + 1) is Inconsistent ; ::_thesis: contradiction
then  F . (k + 1) |- 'not' (VERUM Al) by HENMODEL:6;
then  (F . k) \/ {r} |- 'not' (VERUM Al) by A54;
then consider f1 being FinSequence of CQC-WFF Al such that
A97: rng f1 c= F . k and
A98: |- (f1 ^ <*r*>) ^ <*('not' (VERUM Al))*> by HENMODEL:8;
A99: |- (f1 ^ <*('not' (f . k))*>) ^ <*('not' (f . k))*> by CALCUL_2:21;
A100: now__::_thesis:_not_k_=_0
assume A101: k = 0 ; ::_thesis: contradiction
then A102: r = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)})  }  )))) by A6, MCART_1:7;
reconsider s = (the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)})  }  ))) as Element of CQC-WFF Al ;
A103: |- (f1 ^ <*('not' (f . k))*>) ^ <*(('not' (f . k)) 'or' s)*> by A99, CALCUL_1:51;
 0 + 1 <= len (f1 ^ <*r*>) by CALCUL_1:10;
then  |- (((Ant (f1 ^ <*r*>)) ^ <*('not' (f . k))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*> by A98, Th25;
then  |- ((f1 ^ <*('not' (f . k))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*> by CALCUL_1:5;
then  |- ((f1 ^ <*('not' (f . k))*>) ^ <*r*>) ^ <*('not' (VERUM Al))*> by CALCUL_1:5;
then A104: |- (f1 ^ <*('not' (f . k))*>) ^ <*('not' (VERUM Al))*> by A101, A102, A103, CALCUL_2:24;
 |- (f1 ^ <*s*>) ^ <*s*> by CALCUL_2:21;
then A105: |- (f1 ^ <*s*>) ^ <*(('not' (f . k)) 'or' s)*> by CALCUL_1:52;
 0 + 1 <= len (f1 ^ <*r*>) by CALCUL_1:10;
then  |- (((Ant (f1 ^ <*r*>)) ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*> by A98, Th25;
then  |- ((f1 ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*> by CALCUL_1:5;
then  |- ((f1 ^ <*s*>) ^ <*r*>) ^ <*('not' (VERUM Al))*> by CALCUL_1:5;
then A106: |- (f1 ^ <*s*>) ^ <*('not' (VERUM Al))*> by A101, A102, A105, CALCUL_2:24;
reconsider r1 = f . 0 as Element of CQC-WFF Al ;
set C = still_not-bound_in (CX \/ {r1});
 still_not-bound_in r1 is finite by CQC_SIM1:19;
then  still_not-bound_in {r1} is finite by Th26;
then  (still_not-bound_in {r1}) \/ (still_not-bound_in CX) is finite by A2;
then  still_not-bound_in (CX \/ {r1}) is finite by Th27;
then consider x being bound_QC-variable of Al such that
A107: not x in still_not-bound_in (CX \/ {r1}) by Th28;
consider u being QC-symbol of Al such that
A108: x. u = x by QC_LANG3:30;
 u in  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {r1})  }  by A107, A108;
then reconsider A =  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {r1})  }  as non empty set ;
now__::_thesis:_for_a_being_set_st_a_in_A_holds_
a_in_QC-symbols_Al
let a be set ; ::_thesis: ( a in A implies a in QC-symbols Al )
assume  a in A ; ::_thesis: a in QC-symbols Al
then  ex t being QC-symbol of Al st
( a = t & not x. t in still_not-bound_in (CX \/ {r1}) ) ;
hence  a in QC-symbols Al ; ::_thesis: verum
end;
then reconsider A =  {  t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {r1})  }  as non empty Subset of (QC-symbols Al) by TARSKI:def_3;
set u = Al -one_in A;
 Al -one_in A = the Element of A by QC_LANG1:def_41;
then  Al -one_in A in A ;
then consider t being QC-symbol of Al such that
A109: t = Al -one_in A and
A110: not x. t in still_not-bound_in (CX \/ {r1}) ;
A111: not x. t in (still_not-bound_in CX) \/ (still_not-bound_in {r1}) by A110, Th27;
then A112: not x. t in still_not-bound_in {r1} by XBOOLE_0:def_3;
A113: F . 0 = CX \/  {  ((h . n) `1) where n is Element of NAT : n in 0  }  by A22;
now__::_thesis:_for_b_being_set_holds_not_b_in__{__((h_._n)_`1)_where_n_is_Element_of_NAT_:_n_in_0__}_
let b be set ; ::_thesis: not b in  {  ((h . n) `1) where n is Element of NAT : n in 0  }
assume  b in  {  ((h . n) `1) where n is Element of NAT : n in 0  }  ; ::_thesis: contradiction
then  ex n being Element of NAT st
( b = (h . n) `1 & n in 0 ) ;
hence  contradiction ; ::_thesis: verum
end;
then   {  ((h . n) `1) where n is Element of NAT : n in 0  }  = {} by XBOOLE_0:def_1;
then  still_not-bound_in (rng f1) c= still_not-bound_in CX by A97, A101, A113, Th29;
then  not x. t in still_not-bound_in (rng f1) by A111, XBOOLE_0:def_3;
then A114: not x. (Al -one_in A) in still_not-bound_in f1 by A109, Th30;
reconsider r2 = the_scope_of (f,0) as Element of CQC-WFF Al ;
reconsider y2 = bound_in (f,0) as bound_QC-variable of Al ;
 r1 in ExCl Al by A3, A4, FUNCT_1:3;
then consider y1 being bound_QC-variable of Al, s1 being Element of CQC-WFF Al such that
A115: r1 = Ex (y1,s1) by Def3;
A116: s1 = Ex-the_scope_of r1 by A115, Th22;
A117: r2 = Ex-the_scope_of r1 by Def7;
A118: y1 = Ex-bound_in r1 by A115, Th22;
A119: y2 = Ex-bound_in r1 by Def6;
 not x. (Al -one_in A) in still_not-bound_in r1 by A109, A112, Th26;
then  not x. (Al -one_in A) in still_not-bound_in <*r1*> by CALCUL_1:60;
then  not x. (Al -one_in A) in (still_not-bound_in f1) \/ (still_not-bound_in <*r1*>) by A114, XBOOLE_0:def_3;
then A120: not x. (Al -one_in A) in still_not-bound_in (f1 ^ <*r1*>) by CALCUL_1:59;
 still_not-bound_in (VERUM Al) = {} by QC_LANG3:3;
then  not x. (Al -one_in A) in still_not-bound_in ('not' (VERUM Al)) by QC_LANG3:7;
then  not x. (Al -one_in A) in still_not-bound_in <*('not' (VERUM Al))*> by CALCUL_1:60;
then  not x. (Al -one_in A) in (still_not-bound_in (f1 ^ <*r1*>)) \/ (still_not-bound_in <*('not' (VERUM Al))*>) by A120, XBOOLE_0:def_3;
then  not x. (Al -one_in A) in still_not-bound_in ((f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*>) by CALCUL_1:59;
then  |- (f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*> by A106, A115, A116, A117, A118, A119, CALCUL_1:61;
then  |- f1 ^ <*('not' (VERUM Al))*> by A101, A104, CALCUL_2:26;
then  F . k |- 'not' (VERUM Al) by A97, HENMODEL:def_1;
hence  contradiction by A93, A101, Th24; ::_thesis: verum
end;
now__::_thesis:_not_k_<>_0
assume  k <> 0 ; ::_thesis: contradiction
then consider k1 being natural number  such that
A121: k = k1 + 1 by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12;
A122: ex K, L being Subset of (bound_QC-variables Al) 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 where t is QC-symbol of Al : 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 where u is QC-symbol of Al : not x. u in L  }  )))))))] ) by A6;
set K = (h . k1) `2 ;
set r1 = f . (k1 + 1);
set L = ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))});
set p1 = ('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ))));
A123: r = ('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  )))) by A121, A122, MCART_1:7;
reconsider s = (the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ))) as Element of CQC-WFF Al ;
A124: |- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  )))))*> by A99, A121, CALCUL_1:51;
 0 + 1 <= len (f1 ^ <*r*>) by CALCUL_1:10;
then  |- (((Ant (f1 ^ <*r*>)) ^ <*('not' (f . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*> by A98, Th25;
then  |- ((f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*> by CALCUL_1:5;
then  |- ((f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*r*>) ^ <*('not' (VERUM Al))*> by CALCUL_1:5;
then A125: |- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*('not' (VERUM Al))*> by A123, A124, CALCUL_2:24;
 |- (f1 ^ <*s*>) ^ <*s*> by CALCUL_2:21;
then A126: |- (f1 ^ <*s*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  )))))*> by CALCUL_1:52;
 0 + 1 <= len (f1 ^ <*r*>) by CALCUL_1:10;
then  |- (((Ant (f1 ^ <*r*>)) ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*> by A98, Th25;
then  |- ((f1 ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*> by CALCUL_1:5;
then  |- ((f1 ^ <*s*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  )))))*>) ^ <*('not' (VERUM Al))*> by A123, CALCUL_1:5;
then A127: |- (f1 ^ <*s*>) ^ <*('not' (VERUM Al))*> by A126, CALCUL_2:24;
set y = x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  );
set u = Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ;
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 = f . (k1 + 1) as Element of CQC-WFF Al ;
 r1 in ExCl Al by A3, A4, FUNCT_1:3;
then consider y1 being bound_QC-variable of Al, s1 being Element of CQC-WFF Al such that
A128: r1 = Ex (y1,s1) by Def3;
A129: s1 = Ex-the_scope_of r1 by A128, Th22;
A130: r2 = Ex-the_scope_of r1 by Def7;
A131: y1 = Ex-bound_in r1 by A128, Th22;
A132: y2 = Ex-bound_in r1 by Def6;
reconsider Z = F . k as Subset of (CQC-WFF Al) ;
 not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in still_not-bound_in (Z \/ {r1}) by A74, A121;
then A133: not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in (still_not-bound_in Z) \/ (still_not-bound_in {r1}) by Th27;
then A134: not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in still_not-bound_in {r1} by XBOOLE_0:def_3;
 still_not-bound_in (rng f1) c= still_not-bound_in Z by A97, Th29;
then  not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in still_not-bound_in (rng f1) by A133, XBOOLE_0:def_3;
then A135: not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in still_not-bound_in f1 by Th30;
 not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in still_not-bound_in r1 by A134, Th26;
then  not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in still_not-bound_in <*r1*> by CALCUL_1:60;
then  not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in (still_not-bound_in f1) \/ (still_not-bound_in <*r1*>) by A135, XBOOLE_0:def_3;
then A136: not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in still_not-bound_in (f1 ^ <*r1*>) by CALCUL_1:59;
 still_not-bound_in (VERUM Al) = {} by QC_LANG3:3;
then  not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in still_not-bound_in ('not' (VERUM Al)) by QC_LANG3:7;
then  not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in still_not-bound_in <*('not' (VERUM Al))*> by CALCUL_1:60;
then  not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in (still_not-bound_in (f1 ^ <*r1*>)) \/ (still_not-bound_in <*('not' (VERUM Al))*>) by A136, XBOOLE_0:def_3;
then  not x. (Al -one_in  {  t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))})  }  ) in still_not-bound_in ((f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*>) by CALCUL_1:59;
then  |- (f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*> by A127, A128, A129, A130, A131, A132, CALCUL_1:61;
then  |- f1 ^ <*('not' (VERUM Al))*> by A125, CALCUL_2:26;
then  F . k |- 'not' (VERUM Al) by A97, HENMODEL:def_1;
hence  contradiction by A96, Th24; ::_thesis: verum
end;
hence  contradiction by A100; ::_thesis: verum
end;
hence  S4[k + 1] ; ::_thesis: verum
end;
 for n being Element of NAT holds S4[n] from NAT_1:sch_1(A94, A95);
then  for n, m being Element of NAT 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 = CY as Consistent Subset of (CQC-WFF Al) by A40, HENMODEL:11;
take  CY ; ::_thesis: ( CX c= CY & CY is with_examples )
thus  ( CX c= CY & CY is with_examples ) by A9, Def2, XBOOLE_1:7; ::_thesis: verum
end;

theorem Th32: :: GOEDELCP:32
for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st X |- p & X c= Y holds
Y |- p
proof
let Al be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st X |- p & X c= Y holds
Y |- p
let X, Y be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al st X |- p & X c= Y holds
Y |- p
let p be Element of CQC-WFF Al; ::_thesis: ( X |- p & X c= Y implies Y |- p )
assume that
A1: X |- p and
A2: X c= Y ; ::_thesis: Y |- p
consider f being FinSequence of CQC-WFF Al such that
A3: rng f c= X and
A4: |- f ^ <*p*> by A1, HENMODEL:def_1;
 rng f c= Y by A2, A3, XBOOLE_1:1;
hence  Y |- p by A4, HENMODEL:def_1; ::_thesis: verum
end;


theorem Th33: :: GOEDELCP:33
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & CX is with_examples holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples )
proof
let Al be QC-alphabet ; ::_thesis: for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & CX is with_examples holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples )
let CX be Consistent Subset of (CQC-WFF Al); ::_thesis: ( Al is countable & CX is with_examples implies ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples ) )
assume A1: Al is countable ; ::_thesis: ( not CX is with_examples or ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples ) )
assume A2: CX is with_examples ; ::_thesis: ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples )
 ( not CQC-WFF Al is 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 = f as Function of NAT,(CQC-WFF Al) by A3, A4, FUNCT_2:2;
defpred S1[ set , set , set ] means  ex X being Subset of (CQC-WFF Al) st
( X = $2 \/ {(f . $1)} & ( X is Consistent implies $3 = X ) & ( not X is Consistent implies $3 = $2 ) );
A5: for n being Element of NAT
for C being Subset of (CQC-WFF Al) ex D being Subset of (CQC-WFF Al) st S1[n,C,D]
proof
let n be Element of NAT ; ::_thesis: for C being Subset of (CQC-WFF Al) ex D being Subset of (CQC-WFF Al) st S1[n,C,D]
reconsider p = f . n as Element of CQC-WFF Al ;
let C be Subset of (CQC-WFF Al); ::_thesis: ex D being Subset of (CQC-WFF Al) st S1[n,C,D]
set X = C \/ {p};
reconsider X = C \/ {p} as Subset of (CQC-WFF Al) ;
 ( not X is Consistent implies ex D being Subset of (CQC-WFF Al) st
( D = C & ex X being Subset of (CQC-WFF Al) st
( X = C \/ {p} & ( X is Consistent implies D = X ) & ( not X is Consistent implies D = C ) ) ) ) ;
hence  ex D being Subset of (CQC-WFF Al) st S1[n,C,D] ; ::_thesis: verum
end;
consider h being Function of NAT,(bool (CQC-WFF Al)) such that
A6: ( h . 0 = CX & ( for n being Element of NAT holds S1[n,h . n,h . (n + 1)] ) ) from RECDEF_1:sch_2(A5);
set CY = union (rng h);
A7: now__::_thesis:_for_a_being_set_st_a_in_CX_holds_
a_in_union_(rng_h)
let a be set ; ::_thesis: ( a in CX implies a in union (rng h) )
assume A8: a in CX ; ::_thesis: a in union (rng h)
 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; ::_thesis: verum
end;
then A9: CX c= union (rng h) by TARSKI:def_3;
A10: for n being Element of NAT holds h . n c= h . (n + 1)
proof
let n be Element of NAT ; ::_thesis: h . n c= h . (n + 1)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in h . n or a in h . (n + 1) )
assume A11: a in h . n ; ::_thesis: a in h . (n + 1)
reconsider p = f . n as Element of CQC-WFF Al ;
set X = (h . n) \/ {p};
reconsider X = (h . n) \/ {p} as Subset of (CQC-WFF Al) ;
A12: h . n c= X by XBOOLE_1:7;
 ex Y being Subset of (CQC-WFF Al) 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  a in h . (n + 1) by A11, A12; ::_thesis: verum
end;
A13: for n, m being Element of NAT st m in dom h & n in dom h & n < m holds
h . n c= h . m
proof
let n, m be Element of NAT ; ::_thesis: ( m in dom h & n in dom h & n < m implies h . n c= h . m )
assume that
 m in dom h and
 n in dom h and
A14: n < m ; ::_thesis: h . n c= h . m
defpred S2[ Element of NAT ] means ( n <= $1 implies h . n c= h . $1 );
A15: S2[ 0 ]
proof
assume  n <= 0 ; ::_thesis: h . n c= h . 0
then  n = 0 by NAT_1:2;
hence  h . n c= h . 0 ; ::_thesis: verum
end;
A16: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A17: S2[k] ; ::_thesis: S2[k + 1]
assume A18: n <= k + 1 ; ::_thesis: h . n c= h . (k + 1)
now__::_thesis:_(_n_<=_k_implies_h_._n_c=_h_._(k_+_1)_)
assume A19: n <= k ; ::_thesis: h . n c= h . (k + 1)
 h . k c= h . (k + 1) by A10;
hence  h . n c= h . (k + 1) by A17, A19, XBOOLE_1:1; ::_thesis: verum
end;
hence  h . n c= h . (k + 1) by A18, NAT_1:8; ::_thesis: verum
end;
 for k being Element of NAT holds S2[k] from NAT_1:sch_1(A15, A16);
hence  h . n c= h . m by A14; ::_thesis: verum
end;
defpred S2[ Element of NAT ] means h . $1 is Consistent ;
A20: S2[ 0 ] by A6;
A21: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A22: S2[n] ; ::_thesis: S2[n + 1]
 ex Y being Subset of (CQC-WFF Al) 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  S2[n + 1] by A22; ::_thesis: verum
end;
set CY = union (rng h);
 for n being Element of NAT holds S2[n] from NAT_1:sch_1(A20, A21);
then  for n, m being Element of NAT 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 = union (rng h) as Consistent Subset of (CQC-WFF Al) by HENMODEL:11;
A23: CY is negation_faithful
proof
let p be Element of CQC-WFF Al; :: according to GOEDELCP:def_1 ::_thesis: ( CY |- p or CY |- 'not' p )
consider a being set  such that
A24: a in dom f and
A25: f . a = p by A4, FUNCT_1:def_3;
reconsider n = a as Element of NAT by A24;
now__::_thesis:_(_not_CY_|-_'not'_p_implies_CY_|-_p_)
assume  not CY |- 'not' p ; ::_thesis: CY |- p
then A26: not CY \/ {p} is Inconsistent by HENMODEL:10;
A27: now__::_thesis:_not_(h_._n)_\/_{p}_is_Inconsistent
assume  (h . n) \/ {p} is Inconsistent ; ::_thesis: contradiction
then A28: (h . n) \/ {p} |- 'not' (VERUM Al) by Th24;
now__::_thesis:_for_a_being_set_st_a_in_h_._n_holds_
a_in_CY
let a be set ; ::_thesis: ( a in h . n implies a in CY )
assume A29: a in h . n ; ::_thesis: a in CY
 dom h = NAT by FUNCT_2:def_1;
then  h . n in rng h by FUNCT_1:3;
hence  a in CY by A29, TARSKI:def_4; ::_thesis: verum
end;
then  h . n c= CY by TARSKI:def_3;
then  CY \/ {p} |- 'not' (VERUM Al) by A28, Th32, XBOOLE_1:9;
hence  contradiction by A26, Th24; ::_thesis: verum
end;
A30: ex Y being Subset of (CQC-WFF Al) 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__::_thesis:_for_a_being_set_st_a_in_h_._(n_+_1)_holds_
a_in_CY
let a be set ; ::_thesis: ( a in h . (n + 1) implies a in CY )
assume A31: a in h . (n + 1) ; ::_thesis: a in CY
 dom h = NAT by FUNCT_2:def_1;
then  h . (n + 1) in rng h by FUNCT_1:3;
hence  a in CY by A31, TARSKI:def_4; ::_thesis: verum
end;
then A32: h . (n + 1) c= CY by TARSKI:def_3;
 {p} c= h . (n + 1) by A25, A27, A30, XBOOLE_1:7;
then  {p} c= CY by A32, XBOOLE_1:1;
then  p in CY by ZFMISC_1:31;
hence  CY |- p by Th21; ::_thesis: verum
end;
hence  ( CY |- p or CY |- 'not' p ) ; ::_thesis: verum
end;
A33: CY is with_examples
proof
let x be bound_QC-variable of Al; :: according to GOEDELCP:def_2 ::_thesis: for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
let p be Element of CQC-WFF Al; ::_thesis: ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
consider y being bound_QC-variable of Al such that
A34: CX |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A2, Def2;
take  y ; ::_thesis: CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
thus  CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A9, A34, Th32; ::_thesis: verum
end;
take  CY ; ::_thesis: ( CX c= CY & CY is negation_faithful & CY is with_examples )
thus  ( CX c= CY & CY is negation_faithful & CY is with_examples ) by A7, A23, A33, TARSKI:def_3; ::_thesis: verum
end;


theorem Th34: :: GOEDELCP:34
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & still_not-bound_in CX is finite holds
ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX
proof
let Al be QC-alphabet ; ::_thesis: for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & still_not-bound_in CX is finite holds
ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX
let CX be Consistent Subset of (CQC-WFF Al); ::_thesis: ( Al is countable & still_not-bound_in CX is finite implies ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX )
assume A1: Al is countable ; ::_thesis: ( not still_not-bound_in CX is finite or ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX )
assume  still_not-bound_in CX is finite ; ::_thesis: ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX
then consider CY being Consistent Subset of (CQC-WFF Al) such that
A2: CX c= CY and
A3: CY is with_examples by Th31, A1;
consider CZ being Consistent Subset of (CQC-WFF Al) such that
A4: CY c= CZ and
A5: CZ is negation_faithful and
A6: CZ is with_examples by A1, A3, Th33;
A7: CX c= CZ by A2, A4, XBOOLE_1:1;
set JH1 = the Henkin_interpretation of CZ;
A8: now__::_thesis:_for_p_being_Element_of_CQC-WFF_Al_st_p_in_CX_holds_
the_Henkin_interpretation_of_CZ,_valH_Al_|=_p
let p be Element of CQC-WFF Al; ::_thesis: ( p in CX implies the Henkin_interpretation of CZ, valH Al |= p )
assume  p in CX ; ::_thesis: the Henkin_interpretation of CZ, valH Al |= p
then  CZ |- p by A7, Th21;
hence  the Henkin_interpretation of CZ, valH Al |= p by A5, A6, Th17; ::_thesis: verum
end;
take  CZ ; ::_thesis: ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX
take  the Henkin_interpretation of CZ ; ::_thesis: the Henkin_interpretation of CZ, valH Al |= CX
thus  the Henkin_interpretation of CZ, valH Al |= CX by A8, CALCUL_1:def_11; ::_thesis: verum
end;

begin

theorem Th35: :: GOEDELCP:35
for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al)
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= X & Y c= X holds
J,v |= Y
proof
let Al be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF Al)
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= X & Y c= X holds
J,v |= Y
let X, Y be Subset of (CQC-WFF Al); ::_thesis: for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= X & Y c= X holds
J,v |= Y
let A be non empty set ; ::_thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= X & Y c= X holds
J,v |= Y
let J be interpretation of Al,A; ::_thesis: for v being Element of Valuations_in (Al,A) st J,v |= X & Y c= X holds
J,v |= Y
let v be Element of Valuations_in (Al,A); ::_thesis: ( J,v |= X & Y c= X implies J,v |= Y )
assume A1: J,v |= X ; ::_thesis: ( not Y c= X or J,v |= Y )
assume  Y c= X ; ::_thesis: J,v |= Y
then  for p being Element of CQC-WFF Al st p in Y holds
J,v |= p by A1, CALCUL_1:def_11;
hence  J,v |= Y by CALCUL_1:def_11; ::_thesis: verum
end;

theorem Th36: :: GOEDELCP:36
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st still_not-bound_in X is finite holds
still_not-bound_in (X \/ {p}) is finite
proof
let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st still_not-bound_in X is finite holds
still_not-bound_in (X \/ {p}) is finite
let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al st still_not-bound_in X is finite holds
still_not-bound_in (X \/ {p}) is finite
let p be Element of CQC-WFF Al; ::_thesis: ( still_not-bound_in X is finite implies still_not-bound_in (X \/ {p}) is finite )
assume A1: still_not-bound_in X is finite ; ::_thesis: still_not-bound_in (X \/ {p}) 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  still_not-bound_in (X \/ {p}) is finite by Th27; ::_thesis: verum
end;

theorem Th37: :: GOEDELCP:37
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
proof
let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
let p be Element of CQC-WFF Al; ::_thesis: for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
let A be non empty set ; ::_thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
let J be interpretation of Al,A; ::_thesis: for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
let v be Element of Valuations_in (Al,A); ::_thesis: ( X |= p implies not J,v |= X \/ {('not' p)} )
assume A1: X |= p ; ::_thesis: not J,v |= X \/ {('not' p)}
assume A2: J,v |= X \/ {('not' p)} ; ::_thesis: contradiction
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; ::_thesis: verum
end;

theorem :: GOEDELCP:38
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st Al is countable & still_not-bound_in X is finite & X |= p holds
X |- p
proof
let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st Al is countable & still_not-bound_in X is finite & X |= p holds
X |- p
let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al st Al is countable & still_not-bound_in X is finite & X |= p holds
X |- p
let p be Element of CQC-WFF Al; ::_thesis: ( Al is countable & still_not-bound_in X is finite & X |= p implies X |- p )
assume A1: Al is countable ; ::_thesis: ( not still_not-bound_in X is finite or not X |= p or X |- p )
assume A2: still_not-bound_in X is finite ; ::_thesis: ( not X |= p or X |- p )
assume A3: X |= p ; ::_thesis: X |- p
assume A4: not X |- p ; ::_thesis: contradiction
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 being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= Y by A1, A5, Th34;
hence  contradiction by A3, Th37; ::_thesis: verum
end;