goedelcp.miz



    begin

    registration

      cluster countable for QC-alphabet;

      existence

      proof

        

         A1: [: NAT , NAT :] is QC-alphabet by QC_LANG1:def 1;

         [: NAT , NAT :] is countable by CARD_4: 7;

        hence thesis by A1;

      end;

    end

    reserve Al for QC-alphabet;

    reserve b,c,d for set,

X,Y for Subset of ( CQC-WFF Al),

i,j,k,m,n for Nat,

p,p1,q,r,s,s1 for Element of ( CQC-WFF Al),

x,x1,x2,y,y1 for bound_QC-variable of Al,

A for non empty set,

J for interpretation of Al, A,

v for Element of ( Valuations_in (Al,A)),

f1,f2 for FinSequence of ( CQC-WFF Al),

CX,CY,CZ for Consistent Subset of ( CQC-WFF Al),

JH for Henkin_interpretation of CX,

a for Element of A,

t,u for QC-symbol of Al;

    definition

      let Al, X;

      :: GOEDELCP:def1

      attr X is negation_faithful means

      : Def1: X |- p or X |- ( 'not' p);

    end

    definition

      let Al, X;

      :: GOEDELCP:def2

      attr X is with_examples means for x, p holds ex y st X |- (( 'not' ( Ex (x,p))) 'or' (p . (x,y)));

    end

    theorem :: GOEDELCP:1

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

    theorem :: GOEDELCP:2

    

     Th2: for f be FinSequence of ( CQC-WFF Al) holds |- (f ^ <*(( 'not' p) 'or' q)*>) & |- (f ^ <*p*>) implies |- (f ^ <*q*>)

    proof

      let f be FinSequence of ( CQC-WFF Al) such that

       A1: |- (f ^ <*(( 'not' p) 'or' q)*>) and

       A2: |- (f ^ <*p*>);

      set f1 = ((f ^ <*( 'not' p)*>) ^ <*p*>);

      

       A3: ( Ant f1) = (f ^ <*( 'not' p)*>) by CALCUL_1: 5;

      

       A4: ( Ant (f ^ <*p*>)) = f by CALCUL_1: 5;

      ( Suc (f ^ <*p*>)) = p by CALCUL_1: 5;

      then ( Suc (f ^ <*p*>)) = ( Suc f1) by CALCUL_1: 5;

      then

       A5: |- f1 by A2, A3, A4, CALCUL_1: 8, CALCUL_1: 36;

      set f2 = ((f ^ <*( 'not' p)*>) ^ <*( 'not' p)*>);

      

       A6: ( Ant f2) = (f ^ <*( 'not' p)*>) by CALCUL_1: 5;

      

       A7: ( Suc f2) = ( 'not' p) by CALCUL_1: 5;

      

       A8: (( Ant f2) . (( len f) + 1)) = ( 'not' p) by A6, FINSEQ_1: 42;

      (( len f) + 1) = (( len f) + ( len <*( 'not' p)*>)) by FINSEQ_1: 39;

      then (( len f) + 1) = ( len ( Ant f2)) by A6, FINSEQ_1: 22;

      then (( len f) + 1) in ( dom ( Ant f2)) by A6, CALCUL_1: 10;

      then ( Suc f2) is_tail_of ( Ant f2) by A7, A8, CALCUL_1:def 16;

      then

       A9: |- f2 by CALCUL_1: 33;

      

       A10: ( 0 + 1) <= ( len f2) by CALCUL_1: 10;

      

       A11: ( Ant f1) = ( Ant f2) by A6, CALCUL_1: 5;

      ( 'not' ( Suc f1)) = ( Suc f2) by A7, CALCUL_1: 5;

      then |- (( Ant f1) ^ <*( 'not' ( Suc f1))*>) by A9, A10, A11, CALCUL_1: 3;

      then

       A12: |- (( Ant f1) ^ <*q*>) by A5, CALCUL_1: 44;

      set f3 = ((f ^ <*q*>) ^ <*q*>);

      

       A13: ( Ant f3) = (f ^ <*q*>) by CALCUL_1: 5;

      

       A14: ( Suc f3) = q by CALCUL_1: 5;

      

       A15: (( Ant f3) . (( len f) + 1)) = q by A13, FINSEQ_1: 42;

      (( len f) + 1) = (( len f) + ( len <*q*>)) by FINSEQ_1: 39;

      then (( len f) + 1) = ( len ( Ant f3)) by A13, FINSEQ_1: 22;

      then (( len f) + 1) in ( dom ( Ant f3)) by A13, CALCUL_1: 10;

      then ( Suc f3) is_tail_of ( Ant f3) by A14, A15, CALCUL_1:def 16;

      then |- f3 by CALCUL_1: 33;

      then |- ((f ^ <*(( 'not' p) 'or' q)*>) ^ <*q*>) by A3, A12, CALCUL_1: 53;

      then

       A16: |- ((f ^ <*( 'not' (( 'not' ( 'not' p)) '&' ( 'not' q)))*>) ^ <*q*>) by QC_LANG2:def 3;

      set f4 = ((f ^ <*( 'not' q)*>) ^ <*(( 'not' ( 'not' p)) '&' ( 'not' q))*>);

      

       A17: ( Suc f4) = (( 'not' ( 'not' p)) '&' ( 'not' q)) by CALCUL_1: 5;

      then

       A18: |- (( Ant f4) ^ <*( 'not' ( 'not' p))*>) by A16, CALCUL_1: 40, CALCUL_1: 48;

      

       A19: |- (( Ant f4) ^ <*( 'not' q)*>) by A16, A17, CALCUL_1: 41, CALCUL_1: 48;

      set f5 = (( Ant f4) ^ <*( 'not' ( 'not' p))*>);

      set f6 = (( Ant f4) ^ <*( 'not' q)*>);

      

       A20: ( Ant f5) = ( Ant f4) by CALCUL_1: 5;

      

       A21: ( Suc f5) = ( 'not' ( 'not' p)) by CALCUL_1: 5;

      

       A22: ( Ant f6) = ( Ant f4) by CALCUL_1: 5;

      ( Suc f6) = ( 'not' q) by CALCUL_1: 5;

      then |- (( Ant f4) ^ <*(( 'not' ( 'not' p)) '&' ( 'not' q))*>) by A18, A19, A20, A21, A22, CALCUL_1: 39;

      then |- ((f ^ <*( 'not' q)*>) ^ <*(( 'not' ( 'not' p)) '&' ( 'not' q))*>) by CALCUL_1: 5;

      then |- ((f ^ <*( 'not' (( 'not' ( 'not' p)) '&' ( 'not' q)))*>) ^ <*q*>) by CALCUL_1: 48;

      then

       A23: |- ((f ^ <*(( 'not' p) 'or' q)*>) ^ <*q*>) by QC_LANG2:def 3;

      1 <= ( len (f ^ <*(( 'not' p) 'or' q)*>)) by CALCUL_1: 10;

      then |- (( Ant (f ^ <*(( 'not' p) 'or' q)*>)) ^ <*q*>) by A1, A23, CALCUL_1: 45;

      hence thesis by CALCUL_1: 5;

    end;

    theorem :: GOEDELCP:3

    

     Th3: X is with_examples implies (X |- ( Ex (x,p)) iff ex y st X |- (p . (x,y)))

    proof

      assume

       A1: X is with_examples;

      thus X |- ( Ex (x,p)) implies ex y st X |- (p . (x,y))

      proof

        assume X |- ( Ex (x,p));

        then

        consider f1 such that

         A2: ( rng f1) c= X and

         A3: |- (f1 ^ <*( Ex (x,p))*>) by HENMODEL:def 1;

        consider y such that

         A4: X |- (( 'not' ( Ex (x,p))) 'or' (p . (x,y))) by A1;

        consider f2 such that

         A5: ( rng f2) c= X and

         A6: |- (f2 ^ <*(( 'not' ( Ex (x,p))) 'or' (p . (x,y)))*>) by A4, HENMODEL:def 1;

        take y;

        

         A7: |- ((f1 ^ f2) ^ <*( Ex (x,p))*>) by A3, HENMODEL: 5;

         |- ((f1 ^ f2) ^ <*(( 'not' ( Ex (x,p))) 'or' (p . (x,y)))*>) by A6, CALCUL_2: 20;

        then

         A8: |- ((f1 ^ f2) ^ <*(p . (x,y))*>) by A7, Th2;

        ( rng (f1 ^ f2)) = (( rng f1) \/ ( rng f2)) by FINSEQ_1: 31;

        then ( rng (f1 ^ f2)) c= X by A2, A5, XBOOLE_1: 8;

        hence thesis by A8, HENMODEL:def 1;

      end;

      thus (ex y st X |- (p . (x,y))) implies X |- ( Ex (x,p))

      proof

        given y such that

         A9: X |- (p . (x,y));

        consider f1 such that

         A10: ( rng f1) c= X and

         A11: |- (f1 ^ <*(p . (x,y))*>) by A9, HENMODEL:def 1;

         |- (f1 ^ <*( Ex (x,p))*>) by A11, CALCUL_1: 58;

        hence thesis by A10, HENMODEL:def 1;

      end;

    end;

    theorem :: GOEDELCP:4

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

    theorem :: GOEDELCP:5

    

     Th5: |- (f1 ^ <*p*>) & |- (f1 ^ <*q*>) implies |- (f1 ^ <*(p '&' q)*>)

    proof

      set g = (f1 ^ <*p*>);

      set g1 = (f1 ^ <*q*>);

      assume that

       A1: |- g and

       A2: |- g1;

      

       A3: ( Ant g) = f1 by CALCUL_1: 5;

      

       A4: ( Suc g) = p by CALCUL_1: 5;

      

       A5: ( Suc g1) = q by CALCUL_1: 5;

      ( Ant g) = ( Ant g1) by A3, CALCUL_1: 5;

      hence thesis by A1, A2, A3, A4, A5, CALCUL_1: 39;

    end;

    theorem :: GOEDELCP:6

    

     Th6: X |- p & X |- q iff X |- (p '&' q)

    proof

      thus X |- p & X |- q implies X |- (p '&' q)

      proof

        assume that

         A1: X |- p and

         A2: X |- q;

        consider f1 such that

         A3: ( rng f1) c= X and

         A4: |- (f1 ^ <*p*>) by A1, HENMODEL:def 1;

        consider f2 such that

         A5: ( rng f2) c= X and

         A6: |- (f2 ^ <*q*>) by A2, HENMODEL:def 1;

        

         A7: |- ((f1 ^ f2) ^ <*p*>) by A4, HENMODEL: 5;

         |- ((f1 ^ f2) ^ <*q*>) by A6, CALCUL_2: 20;

        then

         A8: |- ((f1 ^ f2) ^ <*(p '&' q)*>) by A7, Th5;

        ( rng (f1 ^ f2)) = (( rng f1) \/ ( rng f2)) by FINSEQ_1: 31;

        then ( rng (f1 ^ f2)) c= X by A3, A5, XBOOLE_1: 8;

        hence thesis by A8, HENMODEL:def 1;

      end;

      thus X |- (p '&' q) implies X |- p & X |- q

      proof

        assume X |- (p '&' q);

        then

        consider f1 such that

         A9: ( rng f1) c= X and

         A10: |- (f1 ^ <*(p '&' q)*>) by HENMODEL:def 1;

        

         A11: |- (f1 ^ <*p*>) by A10, CALCUL_2: 22;

         |- (f1 ^ <*q*>) by A10, CALCUL_2: 23;

        hence thesis by A9, A11, HENMODEL:def 1;

      end;

    end;

    theorem :: GOEDELCP:7

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

    theorem :: GOEDELCP:8

    

     Th8: for p st ( QuantNbr p) <= 0 holds CX is negation_faithful & CX is with_examples implies ((JH,( valH Al)) |= p iff CX |- p)

    proof

      defpred P[ Element of ( CQC-WFF Al)] means CX is negation_faithful & CX is with_examples implies ((JH,( valH Al)) |= $1 iff CX |- $1);

      

       A1: for r, s, x, k holds for l be CQC-variable_list of k, Al holds for P be QC-pred_symbol of k, Al holds P[( VERUM Al)] & P[(P ! l)] & ( P[r] implies P[( 'not' r)]) & ( P[r] & P[s] implies P[(r '&' s)]) by Def1, Th6, HENMODEL: 16, HENMODEL: 17, HENMODEL:def 2, VALUAT_1: 17, VALUAT_1: 18;

      

       A2: for p st ( QuantNbr p) = 0 holds P[p] from SUBSTUT2:sch 3( A1);

      now

        let p;

        assume ( QuantNbr p) <= 0 ;

        then ( QuantNbr p) = 0 by NAT_1: 2;

        hence P[p] by A2;

      end;

      hence thesis;

    end;

    theorem :: GOEDELCP:9

    

     Th9: (J,v) |= ( Ex (x,p)) iff ex a st (J,(v . (x | a))) |= p

    proof

      

       A1: (J,v) |= ( 'not' ( All (x,( 'not' p)))) iff not (J,v) |= ( All (x,( 'not' p))) by VALUAT_1: 17;

      

       A2: (ex a st not (J,(v . (x | a))) |= ( 'not' p)) implies ex a st (J,(v . (x | a))) |= p by VALUAT_1: 17;

      (ex a st (J,(v . (x | a))) |= p) implies ex a st not (J,(v . (x | a))) |= ( 'not' p)

      proof

        given a such that

         A3: (J,(v . (x | a))) |= p;

        take a;

        thus thesis by A3, VALUAT_1: 17;

      end;

      hence thesis by A1, A2, QC_LANG2:def 5, SUBLEMMA: 50;

    end;

    theorem :: GOEDELCP:10

    

     Th10: (JH,( valH Al)) |= ( Ex (x,p)) iff ex y st (JH,( valH Al)) |= (p . (x,y))

    proof

      thus (JH,( valH Al)) |= ( Ex (x,p)) implies ex y st (JH,( valH Al)) |= (p . (x,y))

      proof

        assume (JH,( valH Al)) |= ( Ex (x,p));

        then

        consider x1 be Element of ( HCar Al) such that

         A1: (JH,(( valH Al) . (x | x1))) |= p by Th9;

        

         A2: ( HCar Al) = ( bound_QC-variables Al) by HENMODEL:def 4;

        ( valH Al) = ( id ( bound_QC-variables Al)) by HENMODEL:def 6;

        then ( rng ( valH Al)) = ( bound_QC-variables Al);

        then

        consider b be object such that

         A3: b in ( dom ( valH Al)) and

         A4: (( valH Al) . b) = x1 by A2, FUNCT_1:def 3;

        reconsider y = b as bound_QC-variable of Al by A3;

        take y;

        thus thesis by A1, A4, CALCUL_1: 24;

      end;

      thus (ex y st (JH,( valH Al)) |= (p . (x,y))) implies (JH,( valH Al)) |= ( Ex (x,p))

      proof

        given y such that

         A5: (JH,( valH Al)) |= (p . (x,y));

        ex x1 be Element of ( HCar Al) st ((( valH Al) . y) = x1) & ((JH,(( valH Al) . (x | x1))) |= p) by A5, CALCUL_1: 24;

        hence thesis by Th9;

      end;

    end;

    theorem :: GOEDELCP:11

    

     Th11: (J,v) |= ( 'not' ( Ex (x,( 'not' p)))) iff (J,v) |= ( All (x,p))

    proof

      

       A1: not (J,v) |= ( Ex (x,( 'not' p))) iff for a holds not (J,(v . (x | a))) |= ( 'not' p) by Th9;

      

       A2: (for a holds not (J,(v . (x | a))) |= ( 'not' p)) implies for a holds (J,(v . (x | a))) |= p

      proof

        assume

         A3: for a holds not (J,(v . (x | a))) |= ( 'not' p);

        let a;

         not (J,(v . (x | a))) |= ( 'not' p) by A3;

        hence thesis by VALUAT_1: 17;

      end;

      (for a holds (J,(v . (x | a))) |= p) implies for a holds not (J,(v . (x | a))) |= ( 'not' p) by VALUAT_1: 17;

      hence thesis by A1, A2, SUBLEMMA: 50, VALUAT_1: 17;

    end;

    theorem :: GOEDELCP:12

    

     Th12: X |- ( 'not' ( Ex (x,( 'not' p)))) iff X |- ( All (x,p))

    proof

      thus X |- ( 'not' ( Ex (x,( 'not' p)))) implies X |- ( All (x,p))

      proof

        assume X |- ( 'not' ( Ex (x,( 'not' p))));

        then

        consider f1 such that

         A1: ( rng f1) c= X and

         A2: |- (f1 ^ <*( 'not' ( Ex (x,( 'not' p))))*>) by HENMODEL:def 1;

         |- (f1 ^ <*( All (x,p))*>) by A2, CALCUL_1: 68;

        hence thesis by A1, HENMODEL:def 1;

      end;

      thus X |- ( All (x,p)) implies X |- ( 'not' ( Ex (x,( 'not' p))))

      proof

        assume X |- ( All (x,p));

        then

        consider f1 such that

         A3: ( rng f1) c= X and

         A4: |- (f1 ^ <*( All (x,p))*>) by HENMODEL:def 1;

         |- (f1 ^ <*( 'not' ( Ex (x,( 'not' p))))*>) by A4, CALCUL_1: 68;

        hence thesis by A3, HENMODEL:def 1;

      end;

    end;

    theorem :: GOEDELCP:13

    ( QuantNbr ( Ex (x,p))) = (( QuantNbr p) + 1)

    proof

      ( QuantNbr ( Ex (x,p))) = ( QuantNbr ( 'not' ( All (x,( 'not' p))))) by QC_LANG2:def 5

      .= ( QuantNbr ( All (x,( 'not' p)))) by CQC_SIM1: 16

      .= (( QuantNbr ( 'not' p)) + 1) by CQC_SIM1: 18;

      hence thesis by CQC_SIM1: 16;

    end;

    theorem :: GOEDELCP:14

    

     Th14: ( QuantNbr p) = ( QuantNbr (p . (x,y)))

    proof

      ( QuantNbr p) = ( QuantNbr ( CQC_Sub [p, ( Sbst (x,y))])) by SUBSTUT2: 25;

      hence thesis by SUBSTUT2:def 1;

    end;

    reserve L for PATH of q, p,

F1,F3 for QC-formula of Al,

a for set;

    theorem :: GOEDELCP:15

    

     Th15: for p st ( QuantNbr p) = 1 holds (CX is negation_faithful & CX is with_examples implies ((JH,( valH Al)) |= p iff CX |- p))

    proof

      let p such that

       A1: ( QuantNbr p) = 1 and

       A2: CX is negation_faithful and

       A3: CX is with_examples;

      consider q such that

       A4: q is_subformula_of p and

       A5: ex x, r st q = ( All (x,r)) by A1, SUBSTUT2: 32;

      consider x, r such that

       A6: q = ( All (x,r)) by A5;

      

       A7: ( QuantNbr q) <= 1 by A1, A4, SUBSTUT2: 30;

      

       A8: ( QuantNbr q) = (( QuantNbr r) + 1) by A6, CQC_SIM1: 18;

      then 1 <= ( QuantNbr q) by NAT_1: 11;

      then

       A9: 1 = ( QuantNbr q) by A7, XXREAL_0: 1;

      set L = the PATH of q, p;

      

       A10: 1 <= ( len L) by A4, SUBSTUT2:def 5;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len L) implies ex p1 st p1 = (L . $1) & ( QuantNbr q) <= ( QuantNbr p1) & (CX |- p1 iff (JH,( valH Al)) |= p1);

      

       A11: P[ 0 ];

      

       A12: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A13: P[k];

        assume that

         A14: 1 <= (k + 1) and

         A15: (k + 1) <= ( len L);

        set j = (k + 1);

         A16:

        now

          assume k = 0 ;

          then

           A17: (L . j) = q by A4, SUBSTUT2:def 5;

          take q;

          thus ( QuantNbr q) <= ( QuantNbr q);

           A18:

          now

            assume (JH,( valH Al)) |= ( Ex (x,( 'not' r)));

            then

            consider y such that

             A19: (JH,( valH Al)) |= (( 'not' r) . (x,y)) by Th10;

            ( QuantNbr ( 'not' r)) = 0 by A8, A9, CQC_SIM1: 16;

            then ( QuantNbr (( 'not' r) . (x,y))) = 0 by Th14;

            then CX |- (( 'not' r) . (x,y)) by A2, A3, A19, Th8;

            hence CX |- ( Ex (x,( 'not' r))) by A3, Th3;

          end;

          now

            assume CX |- ( Ex (x,( 'not' r)));

            then

            consider y such that

             A20: CX |- (( 'not' r) . (x,y)) by A3, Th3;

            ( QuantNbr ( 'not' r)) = 0 by A8, A9, CQC_SIM1: 16;

            then ( QuantNbr (( 'not' r) . (x,y))) = 0 by Th14;

            then (JH,( valH Al)) |= (( 'not' r) . (x,y)) by A2, A3, A20, Th8;

            hence (JH,( valH Al)) |= ( Ex (x,( 'not' r))) by Th10;

          end;

          then (JH,( valH Al)) |= ( 'not' ( Ex (x,( 'not' r)))) iff CX |- ( 'not' ( Ex (x,( 'not' r)))) by A2, A18, HENMODEL:def 2, VALUAT_1: 17;

          then (JH,( valH Al)) |= q iff CX |- q by A6, Th11, Th12;

          hence thesis by A17;

        end;

        now

          assume k <> 0 ;

          then 0 < k by NAT_1: 3;

          then

           A21: ( 0 + 1) <= k by NAT_1: 13;

          k < ( len L) by A15, NAT_1: 13;

          then

          consider G1,H1 be Element of ( QC-WFF Al) such that

           A22: (L . k) = G1 and

           A23: (L . j) = H1 and

           A24: G1 is_immediate_constituent_of H1 by A4, A21, SUBSTUT2:def 5;

          consider p1 such that

           A25: p1 = (L . k) and

           A26: ( QuantNbr q) <= ( QuantNbr p1) and

           A27: CX |- p1 iff (JH,( valH Al)) |= p1 by A13, A15, A21, NAT_1: 13;

          

           A28: ex F3 st (F3 = (L . j)) & (F3 is_subformula_of p) by A4, A14, A15, SUBSTUT2: 27;

          reconsider s = H1 as Element of ( CQC-WFF Al) by A4, A14, A15, A23, SUBSTUT2: 28;

          take s;

           A29:

          now

            assume

             A30: s = ( 'not' p1);

            then

             A31: ( QuantNbr q) <= ( QuantNbr s) by A26, CQC_SIM1: 16;

            CX |- s iff (JH,( valH Al)) |= s by A2, A27, A30, HENMODEL:def 2, VALUAT_1: 17;

            hence thesis by A23, A31;

          end;

          

           A32: ( QuantNbr s) <= 1 by A1, A23, A28, SUBSTUT2: 30;

           A33:

          now

            given F1 such that

             A34: s = (p1 '&' F1);

            reconsider F1 as Element of ( CQC-WFF Al) by A34, CQC_LANG: 9;

            ( QuantNbr s) = (( QuantNbr p1) + ( QuantNbr F1)) by A34, CQC_SIM1: 17;

            then

             A35: ( QuantNbr p1) <= ( QuantNbr s) by NAT_1: 11;

            then

             A36: ( QuantNbr p1) <= 1 by A32, XXREAL_0: 2;

            

             A37: 1 <= ( QuantNbr s) by A9, A26, A35, XXREAL_0: 2;

            

             A38: ( QuantNbr p1) = 1 by A9, A26, A36, XXREAL_0: 1;

            ( QuantNbr s) = 1 by A32, A37, XXREAL_0: 1;

            then (1 - 1) = ((( QuantNbr F1) + 1) - 1) by A34, A38, CQC_SIM1: 17;

            then

             A39: CX |- F1 iff (JH,( valH Al)) |= F1 by A2, A3, Th8;

            

             A40: ( QuantNbr q) <= ( QuantNbr s) by A26, A35, XXREAL_0: 2;

            CX |- s iff (JH,( valH Al)) |= s by A27, A34, A39, Th6, VALUAT_1: 18;

            hence thesis by A23, A40;

          end;

           A41:

          now

            given F1 such that

             A42: s = (F1 '&' p1);

            reconsider F1 as Element of ( CQC-WFF Al) by A42, CQC_LANG: 9;

            

             A43: ( QuantNbr s) = (( QuantNbr p1) + ( QuantNbr F1)) by A42, CQC_SIM1: 17;

            then

             A44: ( QuantNbr p1) <= ( QuantNbr s) by NAT_1: 11;

            then

             A45: ( QuantNbr p1) <= 1 by A32, XXREAL_0: 2;

            

             A46: 1 <= ( QuantNbr s) by A9, A26, A44, XXREAL_0: 2;

            

             A47: ( QuantNbr p1) = 1 by A9, A26, A45, XXREAL_0: 1;

            ( QuantNbr s) = 1 by A32, A46, XXREAL_0: 1;

            then

             A48: CX |- F1 iff (JH,( valH Al)) |= F1 by A2, A3, A43, A47, Th8;

            

             A49: ( QuantNbr q) <= ( QuantNbr s) by A26, A44, XXREAL_0: 2;

            CX |- s iff (JH,( valH Al)) |= s by A27, A42, A48, Th6, VALUAT_1: 18;

            hence thesis by A23, A49;

          end;

          now

            given x such that

             A50: s = ( All (x,p1));

            1 < (( QuantNbr p1) + 1) by A9, A26, NAT_1: 13;

            hence contradiction by A32, A50, CQC_SIM1: 18;

          end;

          hence thesis by A22, A24, A25, A29, A33, A41, QC_LANG2:def 19;

        end;

        hence thesis by A16;

      end;

      for k holds P[k] from NAT_1:sch 2( A11, A12);

      then ex p1 st (p1 = (L . ( len L))) & (( QuantNbr q) <= ( QuantNbr p1)) & (CX |- p1 iff (JH,( valH Al)) |= p1) by A10;

      hence thesis by A4, SUBSTUT2:def 5;

    end;

    theorem :: GOEDELCP:16

    

     Th16: for n st for p st ( QuantNbr p) <= n holds (CX is negation_faithful & CX is with_examples implies ((JH,( valH Al)) |= p iff CX |- p)) holds for p st ( QuantNbr p) <= (n + 1) holds (CX is negation_faithful & CX is with_examples implies ((JH,( valH Al)) |= p iff CX |- p))

    proof

      let n such that

       A1: for p st ( QuantNbr p) <= n holds CX is negation_faithful & CX is with_examples implies ((JH,( valH Al)) |= p iff CX |- p);

      let p such that

       A2: ( QuantNbr p) <= (n + 1) and

       A3: CX is negation_faithful and

       A4: CX is with_examples;

      

       A5: ( QuantNbr p) <= n implies thesis by A1, A3, A4;

      now

        assume

         A6: ( QuantNbr p) = (n + 1);

        then

        consider q such that

         A7: q is_subformula_of p and

         A8: ( QuantNbr q) = 1 by NAT_1: 11, SUBSTUT2: 34;

        set L = the PATH of q, p;

        

         A9: 1 <= ( len L) by A7, SUBSTUT2:def 5;

        defpred P[ Nat] means 1 <= $1 & $1 <= ( len L) implies ex p1 st p1 = (L . $1) & ( QuantNbr q) <= ( QuantNbr p1) & (CX |- p1 iff (JH,( valH Al)) |= p1);

        

         A10: P[ 0 ];

        

         A11: for k st P[k] holds P[(k + 1)]

        proof

          let k such that

           A12: P[k];

          assume that

           A13: 1 <= (k + 1) and

           A14: (k + 1) <= ( len L);

          set j = (k + 1);

           A15:

          now

            assume k = 0 ;

            then

             A16: (L . j) = q by A7, SUBSTUT2:def 5;

            take q;

            (JH,( valH Al)) |= q iff CX |- q by A3, A4, A8, Th15;

            hence thesis by A16;

          end;

          now

            assume k <> 0 ;

            then 0 < k by NAT_1: 3;

            then

             A17: ( 0 + 1) <= k by NAT_1: 13;

            k < ( len L) by A14, NAT_1: 13;

            then

            consider G1,H1 be Element of ( QC-WFF Al) such that

             A18: (L . k) = G1 and

             A19: (L . j) = H1 and

             A20: G1 is_immediate_constituent_of H1 by A7, A17, SUBSTUT2:def 5;

            consider p1 such that

             A21: ( QuantNbr q) <= ( QuantNbr p1) and

             A22: p1 = (L . k) and

             A23: CX |- p1 iff (JH,( valH Al)) |= p1 by A12, A14, A17, NAT_1: 13;

            

             A24: ex F3 st (F3 = (L . j)) & (F3 is_subformula_of p) by A7, A13, A14, SUBSTUT2: 27;

            reconsider s = H1 as Element of ( CQC-WFF Al) by A7, A13, A14, A19, SUBSTUT2: 28;

            take s;

             A25:

            now

              assume

               A26: s = ( 'not' p1);

              then

               A27: ( QuantNbr q) <= ( QuantNbr s) by A21, CQC_SIM1: 16;

              CX |- s iff (JH,( valH Al)) |= s by A3, A23, A26, HENMODEL:def 2, VALUAT_1: 17;

              hence thesis by A19, A27;

            end;

            

             A28: ( QuantNbr s) <= (n + 1) by A6, A19, A24, SUBSTUT2: 30;

             A29:

            now

              given F1 such that

               A30: s = (p1 '&' F1);

              reconsider F1 as Element of ( CQC-WFF Al) by A30, CQC_LANG: 9;

              

               A31: ( QuantNbr s) = (( QuantNbr p1) + ( QuantNbr F1)) by A30, CQC_SIM1: 17;

              then (1 + ( QuantNbr F1)) <= ( QuantNbr s) by A8, A21, XREAL_1: 6;

              then (1 + ( QuantNbr F1)) <= (n + 1) by A28, XXREAL_0: 2;

              then ((( QuantNbr F1) + 1) + ( - 1)) <= ((n + 1) + ( - 1)) by XREAL_1: 6;

              then CX |- F1 iff (JH,( valH Al)) |= F1 by A1, A3, A4;

              then

               A32: CX |- s iff (JH,( valH Al)) |= s by A23, A30, Th6, VALUAT_1: 18;

              ( QuantNbr p1) <= ( QuantNbr s) by A31, NAT_1: 11;

              then ( QuantNbr q) <= ( QuantNbr s) by A21, XXREAL_0: 2;

              hence thesis by A19, A32;

            end;

             A33:

            now

              given F1 such that

               A34: s = (F1 '&' p1);

              reconsider F1 as Element of ( CQC-WFF Al) by A34, CQC_LANG: 9;

              

               A35: ( QuantNbr s) = (( QuantNbr p1) + ( QuantNbr F1)) by A34, CQC_SIM1: 17;

              then (1 + ( QuantNbr F1)) <= ( QuantNbr s) by A8, A21, XREAL_1: 6;

              then (1 + ( QuantNbr F1)) <= (n + 1) by A28, XXREAL_0: 2;

              then ((( QuantNbr F1) + 1) + ( - 1)) <= ((n + 1) + ( - 1)) by XREAL_1: 6;

              then CX |- F1 iff (JH,( valH Al)) |= F1 by A1, A3, A4;

              then

               A36: CX |- s iff (JH,( valH Al)) |= s by A23, A34, Th6, VALUAT_1: 18;

              ( QuantNbr p1) <= ( QuantNbr s) by A35, NAT_1: 11;

              then ( QuantNbr q) <= ( QuantNbr s) by A21, XXREAL_0: 2;

              hence thesis by A19, A36;

            end;

            now

              given x such that

               A37: s = ( All (x,p1));

              

               A38: ( QuantNbr s) = (( QuantNbr p1) + 1) by A37, CQC_SIM1: 18;

              then ( QuantNbr p1) < (n + 1) by A28, NAT_1: 13;

              then ( QuantNbr p1) <= n by NAT_1: 13;

              then

               A39: ( QuantNbr ( 'not' p1)) <= n by CQC_SIM1: 16;

              

               A40: ( QuantNbr q) <= ( QuantNbr s) by A21, A38, NAT_1: 13;

               A41:

              now

                assume (JH,( valH Al)) |= ( Ex (x,( 'not' p1)));

                then

                consider y such that

                 A42: (JH,( valH Al)) |= (( 'not' p1) . (x,y)) by Th10;

                ( QuantNbr (( 'not' p1) . (x,y))) <= n by A39, Th14;

                then CX |- (( 'not' p1) . (x,y)) by A1, A3, A4, A42;

                hence CX |- ( Ex (x,( 'not' p1))) by A4, Th3;

              end;

              now

                assume CX |- ( Ex (x,( 'not' p1)));

                then

                consider y such that

                 A43: CX |- (( 'not' p1) . (x,y)) by A4, Th3;

                ( QuantNbr (( 'not' p1) . (x,y))) <= n by A39, Th14;

                then (JH,( valH Al)) |= (( 'not' p1) . (x,y)) by A1, A3, A4, A43;

                hence (JH,( valH Al)) |= ( Ex (x,( 'not' p1))) by Th10;

              end;

              then (JH,( valH Al)) |= ( 'not' ( Ex (x,( 'not' p1)))) iff CX |- ( 'not' ( Ex (x,( 'not' p1)))) by A3, A41, HENMODEL:def 2, VALUAT_1: 17;

              then (JH,( valH Al)) |= s iff CX |- s by A37, Th11, Th12;

              hence thesis by A19, A40;

            end;

            hence thesis by A18, A20, A22, A25, A29, A33, QC_LANG2:def 19;

          end;

          hence thesis by A15;

        end;

        for k holds P[k] from NAT_1:sch 2( A10, A11);

        then ex p1 st (p1 = (L . ( len L))) & (( QuantNbr q) <= ( QuantNbr p1)) & (CX |- p1 iff (JH,( valH Al)) |= p1) by A9;

        hence thesis by A7, SUBSTUT2:def 5;

      end;

      hence thesis by A2, A5, NAT_1: 8;

    end;

    theorem :: GOEDELCP:17

    

     Th17: for p holds (CX is negation_faithful & CX is with_examples implies ((JH,( valH Al)) |= p iff CX |- p))

    proof

      defpred P[ Element of ( CQC-WFF Al)] means CX is negation_faithful & CX is with_examples implies ((JH,( valH Al)) |= $1 iff CX |- $1);

      

       A1: for p st ( QuantNbr p) <= 0 holds P[p] by Th8;

      

       A2: for k st for p st ( QuantNbr p) <= k holds P[p] holds for p st ( QuantNbr p) <= (k + 1) holds P[p] by Th16;

      thus for p holds P[p] from SUBSTUT2:sch 2( A1, A2);

    end;

    begin

    theorem :: GOEDELCP:18

    

     Th18: Al is countable implies ( QC-WFF Al) is countable

    proof

      assume

       A1: Al is countable;

      ( QC-WFF Al) is Al -closed by QC_LANG1:def 11;

      then

       A2: ( QC-WFF Al) is Subset of ( [: NAT , ( QC-symbols Al):] * ) by QC_LANG1:def 10;

       [: NAT , ( QC-symbols Al):] is non empty set & [: NAT , ( QC-symbols Al):] is countable by A1, QC_LANG1: 5;

      then ( [: NAT , ( QC-symbols Al):] * ) is countable by CARD_4: 13;

      hence thesis by A2;

    end;

    definition

      let Al;

      :: GOEDELCP:def3

      func ExCl (Al) -> Subset of ( CQC-WFF Al) means

      : Def3: a in it iff ex x, p st a = ( Ex (x,p));

      existence

      proof

        defpred P[ object] means ex x, p st $1 = ( Ex (x,p));

        consider X be set such that

         A1: for a be object holds a in X iff a in ( CQC-WFF Al) & P[a] from XBOOLE_0:sch 1;

        for a be object st a in X holds a in ( CQC-WFF Al) by A1;

        then

        reconsider X as Subset of ( CQC-WFF Al) by TARSKI:def 3;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        defpred P[ object] means ex x, p st $1 = ( Ex (x,p));

        let A1,A2 be Subset of ( CQC-WFF Al) such that

         A2: a in A1 iff P[a] and

         A3: a in A2 iff P[a];

        now

          let a be object;

          a in A1 iff P[a] by A2;

          hence a in A1 iff a in A2 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: GOEDELCP:19

    

     Th19: Al is countable implies ( CQC-WFF Al) is countable

    proof

      assume

       A1: Al is countable;

      ( QC-WFF Al) is countable by Th18, A1;

      hence thesis;

    end;

    theorem :: GOEDELCP:20

    

     Th20: Al is countable implies ( ExCl Al) is non empty & ( ExCl Al) is countable

    proof

      assume

       A1: Al is countable;

      set x = the bound_QC-variable of Al, p = the Element of ( CQC-WFF Al);

      set a = ( Ex (x,p));

      a in ( ExCl Al) by Def3;

      hence ( ExCl Al) is non empty;

      ( CQC-WFF Al) is countable by Th19, A1;

      hence thesis;

    end;

    

     Lm1: for A be non empty set st A is countable holds ex f be Function st ( dom f) = NAT & A = ( rng f)

    proof

      let A be non empty set such that

       A1: A is countable;

      A c= A;

      then

      consider F be sequence of A such that

       A2: A = ( rng F) by A1, SUPINF_2:def 8;

      ( dom F) = NAT by FUNCT_2:def 1;

      hence thesis by A2;

    end;

    definition

      let Al;

      let p be Element of ( QC-WFF Al);

      :: GOEDELCP:def4

      func Ex-bound_in p -> bound_QC-variable of Al means

      : Def4: ex q be Element of ( QC-WFF Al) st p = ( Ex (it ,q));

      existence by A1, QC_LANG2:def 13;

      uniqueness by QC_LANG2: 13;

    end

    definition

      let Al;

      let p be Element of ( CQC-WFF Al);

      :: GOEDELCP:def5

      func Ex-the_scope_of p -> Element of ( CQC-WFF Al) means

      : Def5: ex x st p = ( Ex (x,it ));

      existence

      proof

        consider x, F1 such that

         A2: p = ( Ex (x,F1)) by A1, QC_LANG2:def 13;

        p = ( 'not' ( All (x,( 'not' F1)))) by A2, QC_LANG2:def 5;

        then ( All (x,( 'not' F1))) is Element of ( CQC-WFF Al) by CQC_LANG: 8;

        then

         A3: ( 'not' F1) is Element of ( CQC-WFF Al) by CQC_LANG: 13;

        take F1;

        thus thesis by A2, A3, CQC_LANG: 8;

      end;

      uniqueness by QC_LANG2: 13;

    end

    definition

      let Al;

      let F be sequence of ( CQC-WFF Al), a be Nat;

      :: GOEDELCP:def6

      func bound_in (F,a) -> bound_QC-variable of Al means

      : Def6: p = (F . a) implies it = ( Ex-bound_in p);

      existence

      proof

        reconsider p = (F . a) as Element of ( CQC-WFF Al);

        take ( Ex-bound_in p);

        thus thesis;

      end;

      uniqueness

      proof

        let x1, x2 such that

         A1: p = (F . a) implies x1 = ( Ex-bound_in p) and

         A2: p = (F . a) implies x2 = ( Ex-bound_in p);

        reconsider q = (F . a) as Element of ( CQC-WFF Al);

        x1 = ( Ex-bound_in q) by A1;

        hence thesis by A2;

      end;

    end

    definition

      let Al;

      let F be sequence of ( CQC-WFF Al), a be Nat;

      :: GOEDELCP:def7

      func the_scope_of (F,a) -> Element of ( CQC-WFF Al) means

      : Def7: p = (F . a) implies it = ( Ex-the_scope_of p);

      existence

      proof

        reconsider p = (F . a) as Element of ( CQC-WFF Al);

        take ( Ex-the_scope_of p);

        thus thesis;

      end;

      uniqueness

      proof

        let q1,q2 be Element of ( CQC-WFF Al) such that

         A1: p = (F . a) implies q1 = ( Ex-the_scope_of p) and

         A2: p = (F . a) implies q2 = ( Ex-the_scope_of p);

        reconsider q = (F . a) as Element of ( CQC-WFF Al);

        q1 = ( Ex-the_scope_of q) by A1;

        hence thesis by A2;

      end;

    end

    definition

      let Al, X;

      :: GOEDELCP:def8

      func still_not-bound_in X -> Subset of ( bound_QC-variables Al) equals ( union { ( still_not-bound_in p) : p in X });

      coherence

      proof

        set Y = ( union { ( still_not-bound_in p) : p in X });

        now

          let a be object;

          assume a in Y;

          then

          consider b such that

           A1: a in b & b in { ( still_not-bound_in p) : p in X } by TARSKI:def 4;

          ex p st (b = ( still_not-bound_in p)) & (p in X) by A1;

          hence a in ( bound_QC-variables Al) by A1;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: GOEDELCP:21

    

     Th21: p in X implies X |- p

    proof

      assume

       A1: p in X;

      now

        let a be object;

        assume a in ( rng <*p*>);

        then a in {p} by FINSEQ_1: 38;

        hence a in X by A1, TARSKI:def 1;

      end;

      then

       A2: ( rng <*p*>) c= X;

       |- ((( <*> ( CQC-WFF Al)) ^ <*p*>) ^ <*p*>) by CALCUL_2: 21;

      then |- ( <*p*> ^ <*p*>) by FINSEQ_1: 34;

      hence thesis by A2, HENMODEL:def 1;

    end;

    theorem :: GOEDELCP:22

    

     Th22: ( Ex-bound_in ( Ex (x,p))) = x & ( Ex-the_scope_of ( Ex (x,p))) = p

    proof

      ( Ex (x,p)) is existential by QC_LANG2:def 13;

      hence thesis by Def4, Def5;

    end;

    theorem :: GOEDELCP:23

    

     Th23: X |- ( VERUM Al)

    proof

      set f = ( <*> ( CQC-WFF Al));

      

       A1: ( rng f) c= X;

       |- (f ^ <*( VERUM Al)*>) by HENMODEL: 15;

      hence thesis by A1, HENMODEL:def 1;

    end;

    theorem :: GOEDELCP:24

    

     Th24: X |- ( 'not' ( VERUM Al)) iff X is Inconsistent by Th23, HENMODEL: 6, HENMODEL:def 2;

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

    reserve K,L for Subset of ( bound_QC-variables Al);

    theorem :: GOEDELCP:25

    

     Th25: for f,g be FinSequence of ( CQC-WFF Al) st 0 < ( len f) & |- (f ^ <*p*>) holds |- (((( Ant f) ^ g) ^ <*( Suc f)*>) ^ <*p*>)

    proof

      let f,g be FinSequence of ( CQC-WFF Al) such that

       A1: 0 < ( len f) and

       A2: |- (f ^ <*p*>);

      f is_Subsequence_of ((( Ant f) ^ g) ^ <*( Suc f)*>) by A1, CALCUL_1: 13;

      then ( Ant (f ^ <*p*>)) is_Subsequence_of ((( Ant f) ^ g) ^ <*( Suc f)*>) by CALCUL_1: 5;

      then

       A3: ( Ant (f ^ <*p*>)) is_Subsequence_of ( Ant (((( Ant f) ^ g) ^ <*( Suc f)*>) ^ <*p*>)) by CALCUL_1: 5;

      ( Suc (f ^ <*p*>)) = p by CALCUL_1: 5;

      then ( Suc (f ^ <*p*>)) = ( Suc (((( Ant f) ^ g) ^ <*( Suc f)*>) ^ <*p*>)) by CALCUL_1: 5;

      hence thesis by A2, A3, CALCUL_1: 36;

    end;

    theorem :: GOEDELCP:26

    

     Th26: ( still_not-bound_in {p}) = ( still_not-bound_in p)

    proof

       A1:

      now

        let a be object;

        assume a in ( still_not-bound_in {p});

        then

        consider b such that

         A2: a in b & b in { ( still_not-bound_in q) : q in {p} } by TARSKI:def 4;

        ex q st (b = ( still_not-bound_in q)) & (q in {p}) by A2;

        hence a in ( still_not-bound_in p) by A2, TARSKI:def 1;

      end;

      now

        let a be object such that

         A3: a in ( still_not-bound_in p);

        set b = ( still_not-bound_in p);

        p in {p} by TARSKI:def 1;

        then b in { ( still_not-bound_in q) : q in {p} };

        hence a in ( still_not-bound_in {p}) by A3, TARSKI:def 4;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: GOEDELCP:27

    

     Th27: ( still_not-bound_in (X \/ Y)) = (( still_not-bound_in X) \/ ( still_not-bound_in Y))

    proof

      thus ( still_not-bound_in (X \/ Y)) c= (( still_not-bound_in X) \/ ( still_not-bound_in Y))

      proof

        set A = { ( still_not-bound_in p) : p in (X \/ Y) };

        let b be object;

        assume b in ( still_not-bound_in (X \/ Y));

        then

        consider a such that

         A1: b in a and

         A2: a in A by TARSKI:def 4;

        consider p such that

         A3: a = ( still_not-bound_in p) and

         A4: p in (X \/ Y) by A2;

         A5:

        now

          assume p in X;

          then a in { ( still_not-bound_in q) : q in X } by A3;

          then

           A6: b in ( union { ( still_not-bound_in q) : q in X }) by A1, TARSKI:def 4;

          ( still_not-bound_in X) c= (( still_not-bound_in X) \/ ( still_not-bound_in Y)) by XBOOLE_1: 7;

          hence thesis by A6;

        end;

        now

          assume p in Y;

          then a in { ( still_not-bound_in q) : q in Y } by A3;

          then

           A7: b in ( union { ( still_not-bound_in q) : q in Y }) by A1, TARSKI:def 4;

          ( still_not-bound_in Y) c= (( still_not-bound_in X) \/ ( still_not-bound_in Y)) by XBOOLE_1: 7;

          hence thesis by A7;

        end;

        hence thesis by A4, A5, XBOOLE_0:def 3;

      end;

      thus (( still_not-bound_in X) \/ ( still_not-bound_in Y)) c= ( still_not-bound_in (X \/ Y))

      proof

        let b be object such that

         A8: b in (( still_not-bound_in X) \/ ( still_not-bound_in Y));

         A9:

        now

          assume b in ( still_not-bound_in X);

          then

          consider a such that

           A10: b in a & a in { ( still_not-bound_in p) : p in X } by TARSKI:def 4;

          

           A11: ex p st (a = ( still_not-bound_in p)) & (p in X) by A10;

          X c= (X \/ Y) by XBOOLE_1: 7;

          then a in { ( still_not-bound_in q) : q in (X \/ Y) } by A11;

          hence thesis by A10, TARSKI:def 4;

        end;

        now

          assume b in ( still_not-bound_in Y);

          then

          consider a such that

           A12: b in a & a in { ( still_not-bound_in p) : p in Y } by TARSKI:def 4;

          

           A13: ex p st (a = ( still_not-bound_in p)) & (p in Y) by A12;

          Y c= (X \/ Y) by XBOOLE_1: 7;

          then a in { ( still_not-bound_in q) : q in (X \/ Y) } by A13;

          hence thesis by A12, TARSKI:def 4;

        end;

        hence thesis by A8, A9, XBOOLE_0:def 3;

      end;

    end;

    theorem :: GOEDELCP:28

    

     Th28: for A be Subset of ( bound_QC-variables Al) st A is finite holds ex x st not x in A

    proof

      let A be Subset of ( bound_QC-variables Al);

      

       A1: not ( bound_QC-variables Al) is finite by CALCUL_1: 64;

      assume A is finite;

      then not (for b be object holds b in A iff b in ( bound_QC-variables Al)) by A1, TARSKI: 2;

      then

      consider b such that

       A2: not b in A and

       A3: b in ( bound_QC-variables Al);

      reconsider x = b as bound_QC-variable of Al by A3;

      take x;

      thus thesis by A2;

    end;

    theorem :: GOEDELCP:29

    

     Th29: X c= Y implies ( still_not-bound_in X) c= ( still_not-bound_in Y)

    proof

      set A = { ( still_not-bound_in p) : p in X };

      assume

       A1: X c= Y;

      let a be object;

      assume a in ( still_not-bound_in X);

      then

      consider b such that

       A2: a in b and

       A3: b in A by TARSKI:def 4;

      ex p st (b = ( still_not-bound_in p)) & (p in X) by A3;

      then b in { ( still_not-bound_in q) : q in Y } by A1;

      hence a in ( still_not-bound_in Y) by A2, TARSKI:def 4;

    end;

    theorem :: GOEDELCP:30

    

     Th30: for f be FinSequence of ( CQC-WFF Al) holds ( still_not-bound_in ( rng f)) = ( still_not-bound_in f)

    proof

      let f be FinSequence of ( CQC-WFF Al);

      set A = { ( still_not-bound_in p) : p in ( rng f) };

       A1:

      now

        let a be object;

        assume a in ( still_not-bound_in ( rng f));

        then

        consider b be set such that

         A2: a in b and

         A3: b in A by TARSKI:def 4;

        consider p such that

         A4: b = ( still_not-bound_in p) and

         A5: p in ( rng f) by A3;

        ex c be object st (c in ( dom f)) & ((f . c) = p) by A5, FUNCT_1:def 3;

        hence a in ( still_not-bound_in f) by A2, A4, CALCUL_1:def 5;

      end;

      now

        let a be object;

        assume a in ( still_not-bound_in f);

        then

        consider i be Nat, q such that

         A6: i in ( dom f) and

         A7: q = (f . i) and

         A8: a in ( still_not-bound_in q) by CALCUL_1:def 5;

        q in ( rng f) by A6, A7, FUNCT_1:def 3;

        then ( still_not-bound_in q) in A;

        hence a in ( still_not-bound_in ( rng f)) by A8, TARSKI:def 4;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: GOEDELCP:31

    

     Th31: (Al is countable & ( still_not-bound_in CX) is finite) implies ex CY st CX c= CY & CY is with_examples

    proof

      assume

       A1: Al is countable;

      assume

       A2: ( still_not-bound_in CX) is finite;

      ( ExCl Al) is non empty & ( ExCl Al) is countable by A1, Th20;

      then

      consider f be Function such that

       A3: ( dom f) = NAT and

       A4: ( ExCl Al) = ( rng f) by Lm1;

      reconsider f as sequence of ( CQC-WFF Al) by A3, A4, FUNCT_2: 2;

      defpred P[ Nat, set, set] means ex K, L st K = ($2 `2 ) & L = (K \/ ( still_not-bound_in {(f . ($1 + 1))})) & $3 = [(( 'not' (f . ($1 + 1))) 'or' (( the_scope_of (f,($1 + 1))) . (( bound_in (f,($1 + 1))),( x. (Al -one_in { t : not ( x. t) in L }))))), (K \/ ( still_not-bound_in (( 'not' (f . ($1 + 1))) 'or' (( the_scope_of (f,($1 + 1))) . (( bound_in (f,($1 + 1))),( x. (Al -one_in { u : not ( x. u) in L })))))))];

      

       A5: for n be Nat holds for C holds ex D st P[n, C, D]

      proof

        let n be Nat, C;

        set K = (C `2 );

        ex a,b be object st (a in ( CQC-WFF Al)) & (b in ( bool ( bound_QC-variables Al))) & (C = [a, b]) by ZFMISC_1:def 2;

        then

        reconsider K as Subset of ( bound_QC-variables Al);

        set L = (K \/ ( still_not-bound_in {(f . (n + 1))}));

        set D = [(( 'not' (f . (n + 1))) 'or' (( the_scope_of (f,(n + 1))) . (( bound_in (f,(n + 1))),( x. (Al -one_in { t : not ( x. t) in L }))))), (K \/ ( still_not-bound_in (( 'not' (f . (n + 1))) 'or' (( the_scope_of (f,(n + 1))) . (( bound_in (f,(n + 1))),( x. (Al -one_in { u : not ( x. u) in L })))))))];

        take D;

        thus thesis;

      end;

      reconsider A = [(( 'not' (f . 0 )) 'or' (( the_scope_of (f, 0 )) . (( bound_in (f, 0 )),( x. (Al -one_in { u : not ( x. u) in ( still_not-bound_in (CX \/ {(f . 0 )})) }))))), ( still_not-bound_in (CX \/ {(( 'not' (f . 0 )) 'or' (( the_scope_of (f, 0 )) . (( bound_in (f, 0 )),( x. (Al -one_in { t : not ( x. t) in ( still_not-bound_in (CX \/ {(f . 0 )})) })))))}))] as Element of [:( CQC-WFF Al), ( bool ( bound_QC-variables Al)):];

      consider h be sequence of [:( CQC-WFF Al), ( bool ( bound_QC-variables Al)):] such that

       A6: (h . 0 ) = A & for n be Nat holds P[n, (h . n), (h . (n + 1))] from RECDEF_1:sch 2( A5);

      set CY = (CX \/ the set of all ((h . n) `1 ));

      now

        let a be object such that

         A7: a in CY;

        now

          assume not a in CX;

          then a in the set of all ((h . n) `1 ) by A7, XBOOLE_0:def 3;

          then

          consider n such that

           A8: a = ((h . n) `1 );

          ex c,d be object st (c in ( CQC-WFF Al)) & (d in ( bool ( bound_QC-variables Al))) & ((h . n) = [c, d]) by ZFMISC_1:def 2;

          hence a in ( CQC-WFF Al) by A8;

        end;

        hence a in ( CQC-WFF Al);

      end;

      then

      reconsider CY as Subset of ( CQC-WFF Al) by TARSKI:def 3;

       A9:

      now

        let x, p;

        ( Ex (x,p)) in ( ExCl Al) by Def3;

        then

        consider a be object such that

         A10: a in ( dom f) and

         A11: (f . a) = ( Ex (x,p)) by A4, FUNCT_1:def 3;

        reconsider a as Nat by A10;

        reconsider r9 = (f . a) as Element of ( CQC-WFF Al);

        

         A12: ( Ex-bound_in r9) = x by A11, Th22;

        

         A13: ( Ex-the_scope_of r9) = p by A11, Th22;

        

         A14: ( bound_in (f,a)) = x by A12, Def6;

        

         A15: ( the_scope_of (f,a)) = p by A13, Def7;

        

         A16: ((h . a) `1 ) in the set of all ((h . n) `1 );

        

         A17: the set of all ((h . n) `1 ) c= CY by XBOOLE_1: 7;

        

         A18: a = 0 implies ex y be bound_QC-variable of Al st CY |- (( 'not' ( Ex (x,p))) 'or' (p . (x,y))) by A6, A11, A14, A15, A16, A17, Th21;

        now

          assume a <> 0 ;

          then

          consider m be Nat such that

           A20: a = (m + 1) by NAT_1: 6;

          reconsider m as Nat;

          

           A21: ex K, L st K = ((h . m) `2 ) & L = (K \/ ( still_not-bound_in {r9})) & (h . a) = [(( 'not' r9) 'or' (( the_scope_of (f,a)) . (( bound_in (f,a)),( x. (Al -one_in { t : not ( x. t) in L }))))), (K \/ ( still_not-bound_in (( 'not' r9) 'or' (( the_scope_of (f,a)) . (( bound_in (f,a)),( x. (Al -one_in { u : not ( x. u) in L })))))))] by A6, A20;

          set K = ((h . m) `2 );

          set L = (( still_not-bound_in {r9}) \/ K);

          take y = ( x. (Al -one_in { t : not ( x. t) in L }));

          ((h . a) `1 ) = (( 'not' r9) 'or' (( the_scope_of (f,a)) . (( bound_in (f,a)),y))) by A21;

          hence CY |- (( 'not' ( Ex (x,p))) 'or' (p . (x,y))) by A11, A14, A15, A16, A17, Th21;

        end;

        hence ex y st CY |- (( 'not' ( Ex (x,p))) 'or' (p . (x,y))) by A18;

      end;

      deffunc G( set) = (CX \/ { ((h . n) `1 ) : n in $1 });

      consider F be Function such that

       A22: ( dom F) = NAT & for a st a in NAT holds (F . a) = G(a) from FUNCT_1:sch 5;

      

       A23: CY c= ( union ( rng F))

      proof

        let a be object;

        assume

         A24: a in CY;

         A25:

        now

          assume

           A26: a in CX;

          

           A27: (F . 0 ) = (CX \/ { ((h . n) `1 ) : n in 0 }) by A22;

          now

            let b be object;

            assume b in { ((h . n) `1 ) : n in 0 };

            then ex n st (b = ((h . n) `1 )) & (n in 0 );

            hence contradiction;

          end;

          then

           A28: { ((h . n) `1 ) : n in 0 } = {} by XBOOLE_0:def 1;

          (F . 0 ) in ( rng F) by A22, FUNCT_1: 3;

          hence thesis by A26, A27, A28, TARSKI:def 4;

        end;

        now

          assume a in the set of all ((h . n) `1 );

          then

          consider n such that

           A29: a = ((h . n) `1 );

          n < (n + 1) by NAT_1: 13;

          then n in ( Segm (n + 1)) by NAT_1: 44;

          then

           A30: a in { ((h . m) `1 ) : m in (n + 1) } by A29;

          (F . (n + 1)) = (CX \/ { ((h . m) `1 ) : m in (n + 1) }) by A22;

          then

           A31: { ((h . m) `1 ) : m in (n + 1) } c= (F . (n + 1)) by XBOOLE_1: 7;

          (F . (n + 1)) in ( rng F) by A22, FUNCT_1: 3;

          hence thesis by A30, A31, TARSKI:def 4;

        end;

        hence thesis by A24, A25, XBOOLE_0:def 3;

      end;

      ( union ( rng F)) c= CY

      proof

        let a be object;

        assume a in ( union ( rng F));

        then

        consider b such that

         A32: a in b and

         A33: b in ( rng F) by TARSKI:def 4;

        consider c be object such that

         A34: c in ( dom F) and

         A35: (F . c) = b by A33, FUNCT_1:def 3;

        reconsider n = c as Element of NAT by A22, A34;

        

         A36: a in (CX \/ { ((h . m) `1 ) : m in n }) by A22, A32, A35;

         A37:

        now

          assume

           A38: a in CX;

          CX c= CY by XBOOLE_1: 7;

          hence thesis by A38;

        end;

        now

          assume a in { ((h . m) `1 ) : m in n };

          then ex m st (a = ((h . m) `1 )) & (m in n);

          then

           A39: a in the set of all ((h . i) `1 );

           the set of all ((h . i) `1 ) c= CY by XBOOLE_1: 7;

          hence thesis by A39;

        end;

        hence thesis by A36, A37, XBOOLE_0:def 3;

      end;

      then

       A40: CY = ( union ( rng F)) by A23;

      

       A41: for n, m st m in ( dom F) & n in ( dom F) & n < m holds (F . n) c= (F . m)

      proof

        let n, m such that m in ( dom F) and n in ( dom F) and

         A42: n < m;

        reconsider n, m as Element of NAT by ORDINAL1:def 12;

        

         A43: (F . n) = (CX \/ { ((h . i) `1 ) : i in n }) by A22;

        

         A44: (F . m) = (CX \/ { ((h . i) `1 ) : i in m }) by A22;

        now

          let a be object such that

           A45: a in (F . n);

           A46:

          now

            assume

             A47: a in CX;

            CX c= (F . m) by A44, XBOOLE_1: 7;

            hence a in (F . m) by A47;

          end;

          now

            assume a in { ((h . i) `1 ) : i in n };

            then

            consider i such that

             A48: ((h . i) `1 ) = a and

             A49: i in ( Segm n);

            i < n by A49, NAT_1: 44;

            then i < m by A42, XXREAL_0: 2;

            then i in ( Segm m) by NAT_1: 44;

            then

             A50: a in { ((h . j) `1 ) : j in m } by A48;

            { ((h . j) `1 ) : j in m } c= (F . m) by A44, XBOOLE_1: 7;

            hence a in (F . m) by A50;

          end;

          hence a in (F . m) by A43, A45, A46, XBOOLE_0:def 3;

        end;

        hence thesis;

      end;

      ( rng F) c= ( bool ( CQC-WFF Al))

      proof

        let a be object;

        assume a in ( rng F);

        then

        consider b be object such that

         A51: b in ( dom F) and

         A52: (F . b) = a by FUNCT_1:def 3;

        reconsider b as Element of NAT by A22, A51;

        

         A53: (F . b) = (CX \/ { ((h . i) `1 ) : i in b }) by A22;

        now

          let c be object;

          assume c in { ((h . i) `1 ) : i in b };

          then ex i st (((h . i) `1 ) = c) & (i in b);

          hence c in ( CQC-WFF Al) by MCART_1: 10;

        end;

        then { ((h . i) `1 ) : i in b } c= ( CQC-WFF Al);

        then (F . b) c= ( CQC-WFF Al) by A53, XBOOLE_1: 8;

        hence thesis by A52;

      end;

      then

      reconsider F as sequence of ( bool ( CQC-WFF Al)) by A22, FUNCT_2: 2;

      

       A54: for n holds (F . (n + 1)) = ((F . n) \/ {((h . n) `1 )})

      proof

        let n;

        

         A55: n in NAT by ORDINAL1:def 12;

        now

          let a be object;

          assume a in { ((h . i) `1 ) : i in (n + 1) };

          then

          consider j such that

           A56: a = ((h . j) `1 ) and

           A57: j in ( Segm (n + 1));

          j < (n + 1) by A57, NAT_1: 44;

          then

           A58: (j + 1) <= (n + 1) by NAT_1: 13;

           A59:

          now

            assume (j + 1) = (n + 1);

            then

             A60: a in {((h . n) `1 )} by A56, TARSKI:def 1;

             {((h . n) `1 )} c= ({ ((h . i) `1 ) : i in n } \/ {((h . n) `1 )}) by XBOOLE_1: 7;

            hence a in ({ ((h . i) `1 ) : i in n } \/ {((h . n) `1 )}) by A60;

          end;

          now

            assume (j + 1) <= n;

            then j < n by NAT_1: 13;

            then j in ( Segm n) by NAT_1: 44;

            then

             A61: a in { ((h . k) `1 ) : k in n } by A56;

            { ((h . k) `1 ) : k in n } c= ({ ((h . i) `1 ) : i in n } \/ {((h . n) `1 )}) by XBOOLE_1: 7;

            hence a in ({ ((h . i) `1 ) : i in n } \/ {((h . n) `1 )}) by A61;

          end;

          hence a in ({ ((h . i) `1 ) : i in n } \/ {((h . n) `1 )}) by A58, A59, NAT_1: 8;

        end;

        then

         A62: { ((h . k) `1 ) : k in (n + 1) } c= ({ ((h . i) `1 ) : i in n } \/ {((h . n) `1 )});

        now

          let a be object;

          assume

           A63: a in ({ ((h . i) `1 ) : i in n } \/ {((h . n) `1 )});

           A64:

          now

            assume a in { ((h . i) `1 ) : i in n };

            then

            consider j such that

             A65: ((h . j) `1 ) = a and

             A66: j in ( Segm n);

            

             A67: n <= (n + 1) by NAT_1: 11;

            j < n by A66, NAT_1: 44;

            then j < (n + 1) by A67, XXREAL_0: 2;

            then j in ( Segm (n + 1)) by NAT_1: 44;

            hence a in { ((h . i) `1 ) : i in (n + 1) } by A65;

          end;

          now

            assume a in {((h . n) `1 )};

            then

             A68: a = ((h . n) `1 ) by TARSKI:def 1;

            n < (n + 1) by NAT_1: 13;

            then n in ( Segm (n + 1)) by NAT_1: 44;

            hence a in { ((h . i) `1 ) : i in (n + 1) } by A68;

          end;

          hence a in { ((h . i) `1 ) : i in (n + 1) } by A63, A64, XBOOLE_0:def 3;

        end;

        then ({ ((h . i) `1 ) : i in n } \/ {((h . n) `1 )}) c= { ((h . k) `1 ) : k in (n + 1) };

        then ({ ((h . i) `1 ) : i in n } \/ {((h . n) `1 )}) = { ((h . k) `1 ) : k in (n + 1) } by A62;

        then (F . (n + 1)) = (CX \/ ({ ((h . k) `1 ) : k in n } \/ {((h . n) `1 )})) by A22;

        then (F . (n + 1)) = ( G(n) \/ {((h . n) `1 )}) by XBOOLE_1: 4;

        hence (F . (n + 1)) = ((F . n) \/ {((h . n) `1 )}) by A22, A55;

      end;

      defpred P[ Nat] means ((h . $1) `2 ) is finite & ((h . $1) `2 ) is Subset of ( bound_QC-variables Al);

      

       A69: P[ 0 ]

      proof

        

         A70: ((h . 0 ) `2 ) = ( still_not-bound_in (CX \/ {(( 'not' (f . 0 )) 'or' (( the_scope_of (f, 0 )) . (( bound_in (f, 0 )),( x. (Al -one_in { t : not ( x. t) in ( still_not-bound_in (CX \/ {(f . 0 )})) })))))})) by A6;

        reconsider s = (( 'not' (f . 0 )) 'or' (( the_scope_of (f, 0 )) . (( bound_in (f, 0 )),( x. (Al -one_in { t : not ( x. t) in ( still_not-bound_in (CX \/ {(f . 0 )})) }))))) as Element of ( CQC-WFF Al);

        ( still_not-bound_in s) is finite by CQC_SIM1: 19;

        then ( still_not-bound_in {s}) is finite by Th26;

        then (( still_not-bound_in {s}) \/ ( still_not-bound_in CX)) is finite by A2;

        hence thesis by A70, Th27;

      end;

      

       A71: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A72: P[k];

        

         A73: ex K, L st K = ((h . k) `2 ) & L = (K \/ ( still_not-bound_in {(f . (k + 1))})) & (h . (k + 1)) = [(( 'not' (f . (k + 1))) 'or' (( the_scope_of (f,(k + 1))) . (( bound_in (f,(k + 1))),( x. (Al -one_in { t : not ( x. t) in L }))))), (K \/ ( still_not-bound_in (( 'not' (f . (k + 1))) 'or' (( the_scope_of (f,(k + 1))) . (( bound_in (f,(k + 1))),( x. (Al -one_in { u : not ( x. u) in L })))))))] by A6;

        set K = ((h . k) `2 );

        reconsider K as Subset of ( bound_QC-variables Al) by A72;

        set L = (K \/ ( still_not-bound_in {(f . (k + 1))}));

        set s = (( 'not' (f . (k + 1))) 'or' (( the_scope_of (f,(k + 1))) . (( bound_in (f,(k + 1))),( x. (Al -one_in { t : not ( x. t) in L })))));

        ( still_not-bound_in s) is finite by CQC_SIM1: 19;

        hence thesis by A72, A73;

      end;

      

       A74: for k holds P[k] from NAT_1:sch 2( A69, A71);

      defpred P[ Nat] means ( still_not-bound_in (F . ($1 + 1))) c= ((h . $1) `2 ) & not ( x. (Al -one_in { t : not ( x. t) in (( still_not-bound_in {(f . ($1 + 1))}) \/ ((h . $1) `2 )) })) in ( still_not-bound_in ((F . ($1 + 1)) \/ {(f . ($1 + 1))}));

      

       A75: for k holds ( still_not-bound_in (F . (k + 1))) c= ((h . k) `2 ) & not ( x. (Al -one_in { t : not ( x. t) in (( still_not-bound_in {(f . (k + 1))}) \/ ((h . k) `2 )) })) in ( still_not-bound_in ((F . (k + 1)) \/ {(f . (k + 1))}))

      proof

        

         A76: P[ 0 ]

        proof

          set r = (( 'not' (f . 0 )) 'or' (( the_scope_of (f, 0 )) . (( bound_in (f, 0 )),( x. (Al -one_in { t : not ( x. t) in ( still_not-bound_in (CX \/ {(f . 0 )})) })))));

          set A1 = {r};

          reconsider s = (f . 1) as Element of ( CQC-WFF Al);

          

           A77: ((h . 0 ) `2 ) = ( still_not-bound_in (CX \/ A1)) by A6;

          reconsider B = ((h . 0 ) `2 ) as Subset of ( bound_QC-variables Al) by A6;

          reconsider C = (( still_not-bound_in {s}) \/ B) as Element of ( bool ( bound_QC-variables Al));

          ( still_not-bound_in s) is finite by CQC_SIM1: 19;

          then ( still_not-bound_in {s}) is finite by Th26;

          then

          consider x such that

           A78: not x in C by A69, Th28;

          consider u such that

           A79: ( x. u) = x by QC_LANG3: 30;

          u in { t : not ( x. t) in C } by A78, A79;

          then

          reconsider A = { t : not ( x. t) in C } as non empty set;

          now

            let a be object;

            assume a in A;

            then ex t st (a = t) & ( not ( x. t) in C);

            hence a in ( QC-symbols Al);

          end;

          then

          reconsider A = { t : not ( x. t) in C } as non empty Subset of ( QC-symbols Al) by TARSKI:def 3;

          set u = (Al -one_in A);

          u = the Element of A by QC_LANG1:def 41;

          then u in A;

          then

           A80: ex t st (t = u) & ( not ( x. t) in C);

          

           A81: (F . 0 ) = (CX \/ { ((h . n) `1 ) : n in 0 }) by A22;

          now

            let b be object;

            assume b in { ((h . n) `1 ) : n in 0 };

            then ex n st (b = ((h . n) `1 )) & (n in 0 );

            hence contradiction;

          end;

          then

           A82: { ((h . n) `1 ) : n in 0 } = {} by XBOOLE_0:def 1;

          ((h . 0 ) `1 ) = r by A6;

          then (F . ( 0 + 1)) = (CX \/ {r}) by A54, A81, A82;

          hence thesis by A77, A80, Th27;

        end;

        

         A83: for k st P[k] holds P[(k + 1)]

        proof

          let k such that

           A84: P[k];

          reconsider s = (f . (k + 2)) as Element of ( CQC-WFF Al);

          

           A85: ex K, L st K = ((h . k) `2 ) & L = (K \/ ( still_not-bound_in {(f . (k + 1))})) & (h . (k + 1)) = [(( 'not' (f . (k + 1))) 'or' (( the_scope_of (f,(k + 1))) . (( bound_in (f,(k + 1))),( x. (Al -one_in { t : not ( x. t) in L }))))), (K \/ ( still_not-bound_in (( 'not' (f . (k + 1))) 'or' (( the_scope_of (f,(k + 1))) . (( bound_in (f,(k + 1))),( x. (Al -one_in { u : not ( x. u) in L })))))))] by A6;

          set K = ((h . k) `2 );

          reconsider K as Subset of ( bound_QC-variables Al) by A74;

          set L = (K \/ ( still_not-bound_in {(f . (k + 1))}));

          set r = (( 'not' (f . (k + 1))) 'or' (( the_scope_of (f,(k + 1))) . (( bound_in (f,(k + 1))),( x. (Al -one_in { t : not ( x. t) in L })))));

          

           A86: ((h . (k + 1)) `1 ) = r by A85;

          

           A87: ((h . (k + 1)) `2 ) = (K \/ ( still_not-bound_in r)) by A85;

          reconsider B = ((h . (k + 1)) `2 ) as Subset of ( bound_QC-variables Al) by A85;

          reconsider C = (( still_not-bound_in {s}) \/ B) as Element of ( bool ( bound_QC-variables Al));

          ( still_not-bound_in s) is finite by CQC_SIM1: 19;

          then

           A88: ( still_not-bound_in {s}) is finite by Th26;

          ((h . (k + 1)) `2 ) is finite by A74;

          then

          consider x such that

           A89: not x in C by A88, Th28;

          consider u such that

           A90: ( x. u) = x by QC_LANG3: 30;

          u in { t : not ( x. t) in (( still_not-bound_in {s}) \/ B) } by A89, A90;

          then

          reconsider A = { t : not ( x. t) in (( still_not-bound_in {s}) \/ B) } as non empty set;

          now

            let a be object;

            assume a in A;

            then ex t st (a = t) & ( not ( x. t) in C);

            hence a in ( QC-symbols Al);

          end;

          then

          reconsider A = { t : not ( x. t) in (( still_not-bound_in {s}) \/ B) } as non empty Subset of ( QC-symbols Al) by TARSKI:def 3;

          set u = (Al -one_in A);

          u = the Element of A by QC_LANG1:def 41;

          then u in A;

          then

           A91: ex t st (t = u) & ( not ( x. t) in C);

          then

           A92: not ( x. u) in ( still_not-bound_in {s}) by XBOOLE_0:def 3;

          (( still_not-bound_in (F . (k + 1))) \/ ( still_not-bound_in r)) c= B by A84, A87, XBOOLE_1: 9;

          then (( still_not-bound_in (F . (k + 1))) \/ ( still_not-bound_in {r})) c= B by Th26;

          then

           A93: ( still_not-bound_in ((F . (k + 1)) \/ {r})) c= B by Th27;

          then ( still_not-bound_in (F . ((k + 1) + 1))) c= B by A54, A86;

          then not ( x. u) in ( still_not-bound_in (F . ((k + 1) + 1))) by A91, XBOOLE_0:def 3;

          then not ( x. u) in (( still_not-bound_in (F . ((k + 1) + 1))) \/ ( still_not-bound_in {s})) by A92, XBOOLE_0:def 3;

          hence thesis by A54, A86, A93, Th27;

        end;

        for k holds P[k] from NAT_1:sch 2( A76, A83);

        hence thesis;

      end;

      defpred P[ Nat] means (F . $1) is Consistent;

      now

        let a be object;

        assume a in { ((h . i) `1 ) : i in 0 };

        then ex j st (a = ((h . j) `1 )) & (j in 0 );

        hence contradiction;

      end;

      then { ((h . i) `1 ) : i in 0 } = {} by XBOOLE_0:def 1;

      then

       A94: (F . 0 ) = (CX \/ {} ) by A22;

      then

       A95: P[ 0 ];

      

       A96: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A97: P[k];

        ex c,d be object st (c in ( CQC-WFF Al)) & (d in ( bool ( bound_QC-variables Al))) & ((h . k) = [c, d]) by ZFMISC_1:def 2;

        then

        reconsider r = ((h . k) `1 ) as Element of ( CQC-WFF Al);

        now

          assume (F . (k + 1)) is Inconsistent;

          then (F . (k + 1)) |- ( 'not' ( VERUM Al)) by HENMODEL: 6;

          then ((F . k) \/ {r}) |- ( 'not' ( VERUM Al)) by A54;

          then

          consider f1 be FinSequence of ( CQC-WFF Al) such that

           A98: ( rng f1) c= (F . k) and

           A99: |- ((f1 ^ <*r*>) ^ <*( 'not' ( VERUM Al))*>) by HENMODEL: 8;

          

           A100: |- ((f1 ^ <*( 'not' (f . k))*>) ^ <*( 'not' (f . k))*>) by CALCUL_2: 21;

           A101:

          now

            assume

             A102: k = 0 ;

            then

             A103: r = (( 'not' (f . 0 )) 'or' (( the_scope_of (f, 0 )) . (( bound_in (f, 0 )),( x. (Al -one_in { t : not ( x. t) in ( still_not-bound_in (CX \/ {(f . 0 )})) }))))) by A6;

            reconsider s = (( the_scope_of (f, 0 )) . (( bound_in (f, 0 )),( x. (Al -one_in { t : not ( x. t) in ( still_not-bound_in (CX \/ {(f . 0 )})) })))) as Element of ( CQC-WFF Al);

            

             A104: |- ((f1 ^ <*( 'not' (f . k))*>) ^ <*(( 'not' (f . k)) 'or' s)*>) by A100, CALCUL_1: 51;

            ( 0 + 1) <= ( len (f1 ^ <*r*>)) by CALCUL_1: 10;

            then |- (((( Ant (f1 ^ <*r*>)) ^ <*( 'not' (f . k))*>) ^ <*( Suc (f1 ^ <*r*>))*>) ^ <*( 'not' ( VERUM Al))*>) by A99, Th25;

            then |- (((f1 ^ <*( 'not' (f . k))*>) ^ <*( Suc (f1 ^ <*r*>))*>) ^ <*( 'not' ( VERUM Al))*>) by CALCUL_1: 5;

            then |- (((f1 ^ <*( 'not' (f . k))*>) ^ <*r*>) ^ <*( 'not' ( VERUM Al))*>) by CALCUL_1: 5;

            then

             A105: |- ((f1 ^ <*( 'not' (f . k))*>) ^ <*( 'not' ( VERUM Al))*>) by A102, A103, A104, CALCUL_2: 24;

             |- ((f1 ^ <*s*>) ^ <*s*>) by CALCUL_2: 21;

            then

             A106: |- ((f1 ^ <*s*>) ^ <*(( 'not' (f . k)) 'or' s)*>) by CALCUL_1: 52;

            ( 0 + 1) <= ( len (f1 ^ <*r*>)) by CALCUL_1: 10;

            then |- (((( Ant (f1 ^ <*r*>)) ^ <*s*>) ^ <*( Suc (f1 ^ <*r*>))*>) ^ <*( 'not' ( VERUM Al))*>) by A99, Th25;

            then |- (((f1 ^ <*s*>) ^ <*( Suc (f1 ^ <*r*>))*>) ^ <*( 'not' ( VERUM Al))*>) by CALCUL_1: 5;

            then |- (((f1 ^ <*s*>) ^ <*r*>) ^ <*( 'not' ( VERUM Al))*>) by CALCUL_1: 5;

            then

             A107: |- ((f1 ^ <*s*>) ^ <*( 'not' ( VERUM Al))*>) by A102, A103, A106, CALCUL_2: 24;

            reconsider r1 = (f . 0 ) as Element of ( CQC-WFF Al);

            set C = ( still_not-bound_in (CX \/ {r1}));

            ( still_not-bound_in r1) is finite by CQC_SIM1: 19;

            then ( still_not-bound_in {r1}) is finite by Th26;

            then (( still_not-bound_in {r1}) \/ ( still_not-bound_in CX)) is finite by A2;

            then C is finite by Th27;

            then

            consider x such that

             A108: not x in C by Th28;

            consider u such that

             A109: ( x. u) = x by QC_LANG3: 30;

            u in { t : not ( x. t) in C } by A108, A109;

            then

            reconsider A = { t : not ( x. t) in C } as non empty set;

            now

              let a be object;

              assume a in A;

              then ex t st (a = t) & ( not ( x. t) in C);

              hence a in ( QC-symbols Al);

            end;

            then

            reconsider A = { t : not ( x. t) in C } as non empty Subset of ( QC-symbols Al) by TARSKI:def 3;

            set u = (Al -one_in A);

            u = the Element of A by QC_LANG1:def 41;

            then u in A;

            then

            consider t such that

             A110: t = u and

             A111: not ( x. t) in C;

            

             A112: not ( x. t) in (( still_not-bound_in CX) \/ ( still_not-bound_in {r1})) by A111, Th27;

            then

             A113: not ( x. t) in ( still_not-bound_in {r1}) by XBOOLE_0:def 3;

            

             A114: (F . 0 ) = (CX \/ { ((h . n) `1 ) : n in 0 }) by A22;

            now

              let b be object;

              assume b in { ((h . n) `1 ) : n in 0 };

              then ex n st (b = ((h . n) `1 )) & (n in 0 );

              hence contradiction;

            end;

            then { ((h . n) `1 ) : n in 0 } = {} by XBOOLE_0:def 1;

            then ( still_not-bound_in ( rng f1)) c= ( still_not-bound_in CX) by A98, A102, A114, Th29;

            then not ( x. t) in ( still_not-bound_in ( rng f1)) by A112, XBOOLE_0:def 3;

            then

             A115: not ( x. u) in ( still_not-bound_in f1) by A110, Th30;

            reconsider r2 = ( the_scope_of (f, 0 )) as Element of ( CQC-WFF Al);

            reconsider y2 = ( bound_in (f, 0 )) as bound_QC-variable of Al;

            r1 in ( ExCl Al) by A3, A4, FUNCT_1: 3;

            then

            consider y1, s1 such that

             A116: r1 = ( Ex (y1,s1)) by Def3;

            

             A117: s1 = ( Ex-the_scope_of r1) by A116, Th22;

            

             A118: r2 = ( Ex-the_scope_of r1) by Def7;

            

             A119: y1 = ( Ex-bound_in r1) by A116, Th22;

            

             A120: y2 = ( Ex-bound_in r1) by Def6;

             not ( x. u) in ( still_not-bound_in r1) by A110, A113, Th26;

            then not ( x. u) in ( still_not-bound_in <*r1*>) by CALCUL_1: 60;

            then not ( x. u) in (( still_not-bound_in f1) \/ ( still_not-bound_in <*r1*>)) by A115, XBOOLE_0:def 3;

            then

             A121: not ( x. u) in ( still_not-bound_in (f1 ^ <*r1*>)) by CALCUL_1: 59;

            ( still_not-bound_in ( VERUM Al)) = {} by QC_LANG3: 3;

            then not ( x. u) in ( still_not-bound_in ( 'not' ( VERUM Al))) by QC_LANG3: 7;

            then not ( x. u) in ( still_not-bound_in <*( 'not' ( VERUM Al))*>) by CALCUL_1: 60;

            then not ( x. u) in (( still_not-bound_in (f1 ^ <*r1*>)) \/ ( still_not-bound_in <*( 'not' ( VERUM Al))*>)) by A121, XBOOLE_0:def 3;

            then not ( x. u) in ( still_not-bound_in ((f1 ^ <*r1*>) ^ <*( 'not' ( VERUM Al))*>)) by CALCUL_1: 59;

            then |- ((f1 ^ <*r1*>) ^ <*( 'not' ( VERUM Al))*>) by A107, A116, A117, A118, A119, A120, CALCUL_1: 61;

            then |- (f1 ^ <*( 'not' ( VERUM Al))*>) by A102, A105, CALCUL_2: 26;

            then (F . k) |- ( 'not' ( VERUM Al)) by A98, HENMODEL:def 1;

            hence contradiction by A94, A102, Th24;

          end;

          now

            assume k <> 0 ;

            then

            consider k1 be Nat such that

             A122: k = (k1 + 1) by NAT_1: 6;

            reconsider k1 as Nat;

            

             A123: ex K, L st K = ((h . k1) `2 ) & L = (K \/ ( still_not-bound_in {(f . (k1 + 1))})) & (h . (k1 + 1)) = [(( 'not' (f . (k1 + 1))) 'or' (( the_scope_of (f,(k1 + 1))) . (( bound_in (f,(k1 + 1))),( x. (Al -one_in { t : not ( x. t) in L }))))), (K \/ ( still_not-bound_in (( 'not' (f . (k1 + 1))) 'or' (( the_scope_of (f,(k1 + 1))) . (( bound_in (f,(k1 + 1))),( x. (Al -one_in { u : not ( x. u) in L })))))))] by A6;

            set K = ((h . k1) `2 );

            set r1 = (f . (k1 + 1));

            set L = (K \/ ( still_not-bound_in {r1}));

            set p1 = (( 'not' r1) 'or' (( the_scope_of (f,(k1 + 1))) . (( bound_in (f,(k1 + 1))),( x. (Al -one_in { t : not ( x. t) in L })))));

            

             A124: r = p1 by A122, A123;

            reconsider s = (( the_scope_of (f,(k1 + 1))) . (( bound_in (f,(k1 + 1))),( x. (Al -one_in { t : not ( x. t) in L })))) as Element of ( CQC-WFF Al);

            

             A125: |- ((f1 ^ <*( 'not' r1)*>) ^ <*p1*>) by A100, A122, CALCUL_1: 51;

            ( 0 + 1) <= ( len (f1 ^ <*r*>)) by CALCUL_1: 10;

            then |- (((( Ant (f1 ^ <*r*>)) ^ <*( 'not' r1)*>) ^ <*( Suc (f1 ^ <*r*>))*>) ^ <*( 'not' ( VERUM Al))*>) by A99, Th25;

            then |- (((f1 ^ <*( 'not' r1)*>) ^ <*( Suc (f1 ^ <*r*>))*>) ^ <*( 'not' ( VERUM Al))*>) by CALCUL_1: 5;

            then |- (((f1 ^ <*( 'not' r1)*>) ^ <*r*>) ^ <*( 'not' ( VERUM Al))*>) by CALCUL_1: 5;

            then

             A126: |- ((f1 ^ <*( 'not' r1)*>) ^ <*( 'not' ( VERUM Al))*>) by A124, A125, CALCUL_2: 24;

             |- ((f1 ^ <*s*>) ^ <*s*>) by CALCUL_2: 21;

            then

             A127: |- ((f1 ^ <*s*>) ^ <*p1*>) by CALCUL_1: 52;

            ( 0 + 1) <= ( len (f1 ^ <*r*>)) by CALCUL_1: 10;

            then |- (((( Ant (f1 ^ <*r*>)) ^ <*s*>) ^ <*( Suc (f1 ^ <*r*>))*>) ^ <*( 'not' ( VERUM Al))*>) by A99, Th25;

            then |- (((f1 ^ <*s*>) ^ <*( Suc (f1 ^ <*r*>))*>) ^ <*( 'not' ( VERUM Al))*>) by CALCUL_1: 5;

            then |- (((f1 ^ <*s*>) ^ <*p1*>) ^ <*( 'not' ( VERUM Al))*>) by A124, CALCUL_1: 5;

            then

             A128: |- ((f1 ^ <*s*>) ^ <*( 'not' ( VERUM Al))*>) by A127, CALCUL_2: 24;

            set y = ( x. (Al -one_in { t : not ( x. t) in L }));

            set u = (Al -one_in { t : not ( x. t) in L });

            reconsider r2 = ( the_scope_of (f,(k1 + 1))) as Element of ( CQC-WFF Al);

            reconsider y2 = ( bound_in (f,(k1 + 1))) as bound_QC-variable of Al;

            reconsider r1 as Element of ( CQC-WFF Al);

            r1 in ( ExCl Al) by A3, A4, FUNCT_1: 3;

            then

            consider y1, s1 such that

             A129: r1 = ( Ex (y1,s1)) by Def3;

            

             A130: s1 = ( Ex-the_scope_of r1) by A129, Th22;

            

             A131: r2 = ( Ex-the_scope_of r1) by Def7;

            

             A132: y1 = ( Ex-bound_in r1) by A129, Th22;

            

             A133: y2 = ( Ex-bound_in r1) by Def6;

            reconsider Z = (F . k) as Subset of ( CQC-WFF Al);

             not y in ( still_not-bound_in (Z \/ {r1})) by A75, A122;

            then

             A134: not y in (( still_not-bound_in Z) \/ ( still_not-bound_in {r1})) by Th27;

            then

             A135: not y in ( still_not-bound_in {r1}) by XBOOLE_0:def 3;

            ( still_not-bound_in ( rng f1)) c= ( still_not-bound_in Z) by A98, Th29;

            then not y in ( still_not-bound_in ( rng f1)) by A134, XBOOLE_0:def 3;

            then

             A136: not y in ( still_not-bound_in f1) by Th30;

             not y in ( still_not-bound_in r1) by A135, Th26;

            then not y in ( still_not-bound_in <*r1*>) by CALCUL_1: 60;

            then not y in (( still_not-bound_in f1) \/ ( still_not-bound_in <*r1*>)) by A136, XBOOLE_0:def 3;

            then

             A137: not y in ( still_not-bound_in (f1 ^ <*r1*>)) by CALCUL_1: 59;

            ( still_not-bound_in ( VERUM Al)) = {} by QC_LANG3: 3;

            then not ( x. u) in ( still_not-bound_in ( 'not' ( VERUM Al))) by QC_LANG3: 7;

            then not ( x. u) in ( still_not-bound_in <*( 'not' ( VERUM Al))*>) by CALCUL_1: 60;

            then not ( x. u) in (( still_not-bound_in (f1 ^ <*r1*>)) \/ ( still_not-bound_in <*( 'not' ( VERUM Al))*>)) by A137, XBOOLE_0:def 3;

            then not ( x. u) in ( still_not-bound_in ((f1 ^ <*r1*>) ^ <*( 'not' ( VERUM Al))*>)) by CALCUL_1: 59;

            then |- ((f1 ^ <*r1*>) ^ <*( 'not' ( VERUM Al))*>) by A128, A129, A130, A131, A132, A133, CALCUL_1: 61;

            then |- (f1 ^ <*( 'not' ( VERUM Al))*>) by A126, CALCUL_2: 26;

            then (F . k) |- ( 'not' ( VERUM Al)) by A98, HENMODEL:def 1;

            hence contradiction by A97, Th24;

          end;

          hence contradiction by A101;

        end;

        hence thesis;

      end;

      for n holds P[n] from NAT_1:sch 2( A95, A96);

      then for n, m st m in ( dom F) & n in ( dom F) & n < m holds (F . n) is Consistent & (F . n) c= (F . m) by A41;

      then

      reconsider CY as Consistent Subset of ( CQC-WFF Al) by A40, HENMODEL: 11;

      take CY;

      thus thesis by A9, XBOOLE_1: 7;

    end;

    theorem :: GOEDELCP:32

    

     Th32: X |- p & X c= Y implies Y |- p

    proof

      assume that

       A1: X |- p and

       A2: X c= Y;

      consider f be FinSequence of ( CQC-WFF Al) such that

       A3: ( rng f) c= X and

       A4: |- (f ^ <*p*>) by A1, HENMODEL:def 1;

      ( rng f) c= Y by A2, A3;

      hence thesis by A4, HENMODEL:def 1;

    end;

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

    theorem :: GOEDELCP:33

    

     Th33: (Al is countable & CX is with_examples) implies (ex CY st CX c= CY & CY is negation_faithful & CY is with_examples)

    proof

      assume

       A1: Al is countable;

      assume

       A2: CX is with_examples;

      ( CQC-WFF Al) is non empty & ( CQC-WFF Al) is countable by Th19, A1;

      then

      consider f be Function such that

       A3: ( dom f) = NAT and

       A4: ( CQC-WFF Al) = ( rng f) by Lm1;

      reconsider f as sequence of ( CQC-WFF Al) by A3, A4, FUNCT_2: 2;

      defpred P[ set, set, set] means ex X st X = ($2 \/ {(f . $1)}) & (X is Consistent implies $3 = X) & ( not X is Consistent implies $3 = $2);

      

       A5: for n be Nat holds for C holds ex D st P[n, C, D]

      proof

        let n be Nat;

        reconsider p = (f . n) as Element of ( CQC-WFF Al);

        let C;

        set X = (C \/ {p});

        reconsider X as Subset of ( CQC-WFF Al);

         not X is Consistent implies ex D st D = C & ex X st X = (C \/ {p}) & (X is Consistent implies D = X) & ( not X is Consistent implies D = C);

        hence thesis;

      end;

      consider h be sequence of ( bool ( CQC-WFF Al)) such that

       A6: (h . 0 ) = CX & for n be Nat holds P[n, (h . n), (h . (n + 1))] from RECDEF_1:sch 2( A5);

      set CY = ( union ( rng h));

       A7:

      now

        let a be object such that

         A8: a in CX;

        ( dom h) = NAT by FUNCT_2:def 1;

        then (h . 0 ) in ( rng h) by FUNCT_1: 3;

        hence a in ( union ( rng h)) by A6, A8, TARSKI:def 4;

      end;

      then

       A9: CX c= CY;

      

       A10: for n holds (h . n) c= (h . (n + 1))

      proof

        let n;

        let a be object such that

         A11: a in (h . n);

        reconsider p = (f . n) as Element of ( CQC-WFF Al);

        set X = ((h . n) \/ {p});

        reconsider X as Subset of ( CQC-WFF Al);

        

         A12: (h . n) c= X by XBOOLE_1: 7;

        ex Y st Y = ((h . n) \/ {(f . n)}) & (Y is Consistent implies (h . (n + 1)) = Y) & ( not Y is Consistent implies (h . (n + 1)) = (h . n)) by A6;

        hence thesis by A11, A12;

      end;

      

       A13: for n, m st m in ( dom h) & n in ( dom h) & n < m holds (h . n) c= (h . m)

      proof

        let n, m such that m in ( dom h) and n in ( dom h) and

         A14: n < m;

        defpred P[ Nat] means n <= $1 implies (h . n) c= (h . $1);

        

         A15: P[ 0 ]

        proof

          assume n <= 0 ;

          then n = 0 by NAT_1: 2;

          hence thesis;

        end;

        

         A16: for k st P[k] holds P[(k + 1)]

        proof

          let k such that

           A17: P[k];

          assume

           A18: n <= (k + 1);

          now

            assume

             A19: n <= k;

            (h . k) c= (h . (k + 1)) by A10;

            hence thesis by A17, A19;

          end;

          hence thesis by A18, NAT_1: 8;

        end;

        for k holds P[k] from NAT_1:sch 2( A15, A16);

        hence thesis by A14;

      end;

      defpred P[ Nat] means (h . $1) is Consistent;

      

       A20: P[ 0 ] by A6;

      

       A21: for k st P[k] holds P[(k + 1)]

      proof

        let n such that

         A22: P[n];

        ex Y st Y = ((h . n) \/ {(f . n)}) & (Y is Consistent implies (h . (n + 1)) = Y) & ( not Y is Consistent implies (h . (n + 1)) = (h . n)) by A6;

        hence thesis by A22;

      end;

      set CY = ( union ( rng h));

      for n holds P[n] from NAT_1:sch 2( A20, A21);

      then for n, m st m in ( dom h) & n in ( dom h) & n < m holds (h . n) is Consistent & (h . n) c= (h . m) by A13;

      then

      reconsider CY as Consistent Subset of ( CQC-WFF Al) by HENMODEL: 11;

      

       A23: CY is negation_faithful

      proof

        let p;

        consider a be object such that

         A24: a in ( dom f) and

         A25: (f . a) = p by A4, FUNCT_1:def 3;

        reconsider n = a as Nat by A24;

        now

          assume not CY |- ( 'not' p);

          then

           A26: not (CY \/ {p}) is Inconsistent by HENMODEL: 10;

           A27:

          now

            assume ((h . n) \/ {p}) is Inconsistent;

            then

             A28: ((h . n) \/ {p}) |- ( 'not' ( VERUM Al)) by Th24;

            now

              let a be object such that

               A29: a in (h . n);

              

               A30: n in NAT by ORDINAL1:def 12;

              ( dom h) = NAT by FUNCT_2:def 1;

              then (h . n) in ( rng h) by FUNCT_1: 3, A30;

              hence a in CY by A29, TARSKI:def 4;

            end;

            then (h . n) c= CY;

            then (CY \/ {p}) |- ( 'not' ( VERUM Al)) by A28, Th32, XBOOLE_1: 9;

            hence contradiction by A26, Th24;

          end;

          

           A31: ex Y st Y = ((h . n) \/ {(f . n)}) & (Y is Consistent implies (h . (n + 1)) = Y) & ( not Y is Consistent implies (h . (n + 1)) = (h . n)) by A6;

          now

            let a be object such that

             A32: a in (h . (n + 1));

            ( dom h) = NAT by FUNCT_2:def 1;

            then (h . (n + 1)) in ( rng h) by FUNCT_1: 3;

            hence a in CY by A32, TARSKI:def 4;

          end;

          then

           A33: (h . (n + 1)) c= CY;

           {p} c= (h . (n + 1)) by A25, A27, A31, XBOOLE_1: 7;

          then {p} c= CY by A33;

          then p in CY by ZFMISC_1: 31;

          hence CY |- p by Th21;

        end;

        hence thesis;

      end;

      

       A34: CY is with_examples

      proof

        let x, p;

        consider y such that

         A35: CX |- (( 'not' ( Ex (x,p))) 'or' (p . (x,y))) by A2;

        take y;

        thus thesis by A9, A35, Th32;

      end;

      take CY;

      thus thesis by A7, A23, A34;

    end;

    reserve JH1 for Henkin_interpretation of CZ,

J for interpretation of Al, A,

v for Element of ( Valuations_in (Al,A));

    theorem :: GOEDELCP:34

    

     Th34: (Al is countable & ( still_not-bound_in CX) is finite) implies ex CZ, JH1 st (JH1,( valH Al)) |= CX

    proof

      assume

       A1: Al is countable;

      assume ( still_not-bound_in CX) is finite;

      then

      consider CY such that

       A2: CX c= CY and

       A3: CY is with_examples by Th31, A1;

      consider CZ such that

       A4: CY c= CZ and

       A5: CZ is negation_faithful and

       A6: CZ is with_examples by A1, A3, Th33;

      

       A7: CX c= CZ by A2, A4;

      set JH1 = the Henkin_interpretation of CZ;

       A8:

      now

        let p;

        assume p in CX;

        then CZ |- p by A7, Th21;

        hence (JH1,( valH Al)) |= p by A5, A6, Th17;

      end;

      take CZ, JH1;

      thus thesis by A8, CALCUL_1:def 11;

    end;

    begin

    theorem :: GOEDELCP:35

    

     Th35: (J,v) |= X & Y c= X implies (J,v) |= Y

    proof

      assume

       A1: (J,v) |= X;

      assume Y c= X;

      then p in Y implies (J,v) |= p by A1, CALCUL_1:def 11;

      hence thesis by CALCUL_1:def 11;

    end;

    theorem :: GOEDELCP:36

    

     Th36: ( still_not-bound_in X) is finite implies ( still_not-bound_in (X \/ {p})) is finite

    proof

      assume

       A1: ( still_not-bound_in X) is finite;

      ( still_not-bound_in p) is finite by CQC_SIM1: 19;

      then ( still_not-bound_in {p}) is finite by Th26;

      then (( still_not-bound_in X) \/ ( still_not-bound_in {p})) is finite by A1;

      hence thesis by Th27;

    end;

    theorem :: GOEDELCP:37

    

     Th37: X |= p implies not (J,v) |= (X \/ {( 'not' p)})

    proof

      assume

       A1: X |= p;

      assume

       A2: (J,v) |= (X \/ {( 'not' p)});

      then

       A3: (J,v) |= X by Th35, XBOOLE_1: 7;

      

       A4: {( 'not' p)} c= (X \/ {( 'not' p)}) by XBOOLE_1: 7;

      ( 'not' p) in {( 'not' p)} by TARSKI:def 1;

      then (J,v) |= ( 'not' p) by A2, A4, CALCUL_1:def 11;

      then not (J,v) |= p by VALUAT_1: 17;

      hence contradiction by A1, A3, CALCUL_1:def 12;

    end;

    ::$Notion-Name

    theorem :: GOEDELCP:38

    (Al is countable & ( still_not-bound_in X) is finite & X |= p) implies X |- p

    proof

      assume

       A1: Al is countable;

      assume

       A2: ( still_not-bound_in X) is finite;

      assume

       A3: X |= p;

      assume

       A4: not X |- p;

      reconsider Y = (X \/ {( 'not' p)}) as Subset of ( CQC-WFF Al);

      

       A5: ( still_not-bound_in Y) is finite by A2, Th36;

      Y is Consistent by A4, HENMODEL: 9;

      then ex CZ, JH1 st ((JH1,( valH Al)) |= Y) by A1, A5, Th34;

      hence contradiction by A3, Th37;

    end;