goedcpuc.miz



    begin

    reserve Al for QC-alphabet,

PHI for Consistent Subset of ( CQC-WFF Al),

PSI for Subset of ( CQC-WFF Al),

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

A for non empty set,

J for interpretation of Al, A,

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

m,n,i,j,k for Element of NAT ,

l for CQC-variable_list of k, Al,

P for QC-pred_symbol of k, Al,

x,y for bound_QC-variable of Al,

z for QC-symbol of Al,

Al2 for Al -expanding QC-alphabet;

    definition

      let Al;

      let PHI be Subset of ( CQC-WFF Al);

      :: GOEDCPUC:def1

      attr PHI is satisfiable means

      : Def1: ex A, J, v st (J,v) |= PHI;

    end

    reserve J2 for interpretation of Al2, A,

Jp for interpretation of Al, A,

v2 for Element of ( Valuations_in (Al2,A)),

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

    theorem :: GOEDCPUC:1

    

     Th1: ex s be set st for p, x holds not [s, [x, p]] in ( QC-symbols Al)

    proof

      assume

       A1: for s be set holds ex p, x st [s, [x, p]] in ( QC-symbols Al);

      for s be set holds s in ( union ( union ( QC-symbols Al)))

      proof

        let s be set;

        consider p, x such that

         A2: [s, [x, p]] in ( QC-symbols Al) by A1;

        

         A3: {s} in { {s, [x, p]}, {s}} by TARSKI:def 2;

        

         A4: s in {s} by TARSKI:def 1;

         { {s, [x, p]}, {s}} c= ( union ( QC-symbols Al)) by A2, ZFMISC_1: 74;

        then {s} c= ( union ( union ( QC-symbols Al))) by A3, ZFMISC_1: 74;

        hence thesis by A4;

      end;

      then ( union ( union ( QC-symbols Al))) in ( union ( union ( QC-symbols Al))) & for X be set holds not X in X;

      hence contradiction;

    end;

    definition

      let Al;

      :: GOEDCPUC:def2

      mode free_symbol of Al -> set means

      : Def2: for p, x holds not [it , [x, p]] in ( QC-symbols Al);

      existence by Th1;

    end

    definition

      let Al;

      :: GOEDCPUC:def3

      func FCEx (Al) -> Al -expanding QC-alphabet equals [: NAT , (( QC-symbols Al) \/ the set of all [ the free_symbol of Al, [x, p]]):];

      coherence

      proof

        set Al2 = [: NAT , (( QC-symbols Al) \/ the set of all [ the free_symbol of Al, [x, p]]):];

        set X = (( QC-symbols Al) \/ the set of all [ the free_symbol of Al, [x, p]]);

        Al2 is non empty set & NAT c= X & Al2 = [: NAT , X:] by QC_LANG1: 3, XBOOLE_1: 10;

        then

        reconsider Al2 as QC-alphabet by QC_LANG1:def 1;

         [: NAT , ( QC-symbols Al):] c= ( [: NAT , ( QC-symbols Al):] \/ [: NAT , the set of all [ the free_symbol of Al, [x, p]]:]) by XBOOLE_1: 7;

        then [: NAT , ( QC-symbols Al):] c= [: NAT , X:] by ZFMISC_1: 97;

        then Al c= Al2 by QC_LANG1: 5;

        hence thesis by QC_TRANS:def 1;

      end;

    end

    definition

      let Al, p, x;

      :: GOEDCPUC:def4

      func Example_of (p,x) -> bound_QC-variable of ( FCEx Al) equals [4, [ the free_symbol of Al, [x, p]]];

      coherence

      proof

        set Al2 = ( FCEx Al);

         [: NAT , ( QC-symbols Al2):] = [: NAT , (( QC-symbols Al) \/ the set of all [ the free_symbol of Al, [y, q]]):] by QC_LANG1: 5;

        then

         A1: ( QC-symbols Al2) = (( QC-symbols Al) \/ the set of all [ the free_symbol of Al, [y, q]]) by ZFMISC_1: 110;

         [ the free_symbol of Al, [x, p]] in the set of all [ the free_symbol of Al, [y, q]];

        then

         A2: [ the free_symbol of Al, [x, p]] in ( QC-symbols Al2) by A1, XBOOLE_0:def 3;

        4 in {4} by TARSKI:def 1;

        then [4, [ the free_symbol of Al, [x, p]]] in [: {4}, ( QC-symbols Al2):] by A2, ZFMISC_1: 87;

        hence thesis by QC_LANG1:def 4;

      end;

    end

    definition

      let Al, p, x;

      :: GOEDCPUC:def5

      func Example_Formula_of (p,x) -> Element of ( CQC-WFF ( FCEx Al)) equals (( 'not' ( Ex ((( FCEx Al) -Cast x),(( FCEx Al) -Cast p)))) 'or' ((( FCEx Al) -Cast p) . ((( FCEx Al) -Cast x),( Example_of (p,x)))));

      coherence ;

    end

    definition

      let Al;

      :: GOEDCPUC:def6

      func Example_Formulae_of (Al) -> Subset of ( CQC-WFF ( FCEx Al)) equals the set of all ( Example_Formula_of (p,x));

      coherence

      proof

        for z be object st z in the set of all ( Example_Formula_of (p,x)) holds z in ( CQC-WFF ( FCEx Al))

        proof

          let z be object such that

           A1: z in the set of all ( Example_Formula_of (p,x));

          ex p, x st z = ( Example_Formula_of (p,x)) by A1;

          hence thesis;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: GOEDCPUC:2

    

     Th2: for k be Element of NAT st k > 0 holds ex F be k -element FinSequence st (for n be Nat st n <= k & 1 <= n holds (F . n) is QC-alphabet) & (F . 1) = Al & for n be Nat st n < k & 1 <= n holds ex Al2 be QC-alphabet st (F . n) = Al2 & (F . (n + 1)) = ( FCEx Al2)

    proof

      defpred A[ Nat] means $1 > 0 implies ex F be $1 -element FinSequence st (for n be Nat st n <= $1 & 1 <= n holds (F . n) is QC-alphabet) & (F . 1) = Al & (for n be Nat st n < $1 & 1 <= n holds ex Al2 be QC-alphabet st (F . n) = Al2 & (F . (n + 1)) = ( FCEx Al2));

      

       A1: for k be Nat st A[k] holds A[(k + 1)]

      proof

        let k be Nat;

        assume

         A2: A[k];

        per cases ;

          suppose

           A3: k = 0 ;

          

           A4: <*Al*> is 1 -element FinSequence & ( <*Al*> . 1) = Al by FINSEQ_1: 40;

          

           A5: for n be Nat st n < 1 & 1 <= n holds ex Al2 be QC-alphabet st ( <*Al*> . n) = Al2 & ( <*Al*> . (n + 1)) = ( FCEx Al2);

          for n be Nat st n <= 1 & 1 <= n holds ( <*Al*> . n) is QC-alphabet by A4, XXREAL_0: 1;

          hence thesis by A3, A4, A5;

        end;

          suppose

           A6: k <> 0 ;

          then

          consider F be k -element FinSequence such that

           A7: (for n be Nat st n <= k & 1 <= n holds (F . n) is QC-alphabet) & ((F . 1) = Al) & (for n be Nat st n < k & 1 <= n holds ex Al2 be QC-alphabet st (F . n) = Al2 & (F . (n + 1)) = ( FCEx Al2)) by A2;

          set K = (F . k);

          K is QC-alphabet

          proof

            per cases ;

              suppose k = 1;

              hence thesis by A7;

            end;

              suppose

               A8: k <> 1;

              consider j be Nat such that

               A9: k = (j + 1) by NAT_1: 6, A6;

              j <> 0 by A8, A9;

              then j >= 1 & j < k by A9, NAT_1: 25, NAT_1: 19;

              then ex Al2 be QC-alphabet st (F . j) = Al2 & (F . k) = ( FCEx Al2) by A7, A9;

              hence thesis;

            end;

          end;

          then

          reconsider K as QC-alphabet;

          set K2 = <*( FCEx K)*>;

          set F2 = (F ^ K2);

          reconsider F2 as (k + 1) -element FinSequence;

          

           A10: 1 <= k & ( len F) = k by A6, NAT_1: 25, CARD_1:def 7;

          

           A11: for n be Nat st n < k & 1 <= n holds ex Al2 be QC-alphabet st (F2 . n) = Al2 & (F2 . (n + 1)) = ( FCEx Al2)

          proof

            let n be Nat such that

             A12: n < k & 1 <= n;

            consider Al2 be QC-alphabet such that

             A13: (F . n) = Al2 & (F . (n + 1)) = ( FCEx Al2) by A7, A12;

            1 <= (n + 1) & (n + 1) <= k & k = ( len F) by A12, NAT_1: 13, CARD_1:def 7;

            then (F2 . n) = (F . n) & (F2 . (n + 1)) = (F . (n + 1)) by A12, FINSEQ_1: 64;

            hence thesis by A13;

          end;

          

           A14: K is QC-alphabet & (F2 . k) = K by A10, FINSEQ_1: 64;

          

           A15: for n be Nat st n < (k + 1) & 1 <= n holds ex Al2 be QC-alphabet st (F2 . n) = Al2 & (F2 . (n + 1)) = ( FCEx Al2)

          proof

            let n be Nat such that

             A16: n < (k + 1) & 1 <= n;

            per cases ;

              suppose n <> k;

              hence thesis by A11, A16, NAT_1: 22;

            end;

              suppose n = k;

              hence thesis by A10, A14, FINSEQ_1: 42;

            end;

          end;

          

           A17: for n be Nat st n <= (k + 1) & 1 <= n holds (F2 . n) is QC-alphabet

          proof

            let n be Nat such that

             A18: n <= (k + 1) & 1 <= n;

            per cases ;

              suppose n <> (k + 1);

              then n <= k by A18, NAT_1: 8;

              then (F2 . n) = (F . n) & (F . n) is QC-alphabet by A7, A10, A18, FINSEQ_1: 64;

              hence thesis;

            end;

              suppose n = (k + 1);

              hence thesis by A10, FINSEQ_1: 42;

            end;

          end;

          (F2 . 1) = Al by A7, A10, FINSEQ_1: 64;

          hence thesis by A15, A17;

        end;

      end;

      

       A19: A[ 0 ];

      for n be Nat holds A[n] from NAT_1:sch 2( A19, A1);

      hence thesis;

    end;

    definition

      let Al;

      let k be Nat;

      :: GOEDCPUC:def7

      mode FCEx-Sequence of Al,k -> (k + 1) -element FinSequence means

      : Def7: (for n be Nat st n <= (k + 1) & 1 <= n holds (it . n) is QC-alphabet) & (it . 1) = Al & (for n be Nat st n < (k + 1) & 1 <= n holds ex Al2 be QC-alphabet st (it . n) = Al2 & (it . (n + 1)) = ( FCEx Al2));

      existence by Th2;

    end

    theorem :: GOEDCPUC:3

    

     Th3: for k be Nat holds for S be FCEx-Sequence of Al, k holds (S . (k + 1)) is QC-alphabet

    proof

      let k be Nat;

      let S be FCEx-Sequence of Al, k;

       0 < ( 0 + (k + 1));

      then 1 <= (k + 1) & (k + 1) <= (k + 1) by NAT_1: 19;

      hence thesis by Def7;

    end;

    theorem :: GOEDCPUC:4

    

     Th4: for k be Nat holds for S be FCEx-Sequence of Al, k holds (S . (k + 1)) is Al -expanding QC-alphabet

    proof

      let k be Nat;

      let S be FCEx-Sequence of Al, k;

      set Al2 = (S . (k + 1));

      reconsider Al2 as QC-alphabet by Th3;

      Al c= Al2

      proof

        let x be object;

        assume

         A1: x in Al;

        defpred A[ Nat] means $1 < (k + 1) implies x in (S . ($1 + 1));

        

         A2: A[ 0 ] by A1, Def7;

        

         A3: for l be Nat st A[l] holds A[(l + 1)]

        proof

          let l be Nat;

          assume

           A4: A[l];

          assume

           A5: (l + 1) < (k + 1);

          

           A6: for n be Nat st (n + 1) < (k + 1) & 1 <= (n + 1) holds ex Al2 be QC-alphabet st (S . (n + 1)) = Al2 & (S . (n + 2)) = ( FCEx Al2)

          proof

            let n be Nat such that

             A7: (n + 1) < (k + 1) & 1 <= (n + 1);

            set m = (n + 1);

            ex Al2 be QC-alphabet st (S . m) = Al2 & (S . (m + 1)) = ( FCEx Al2) by Def7, A7;

            hence thesis;

          end;

           0 < ( 0 + (l + 1));

          then

          consider Al2 be QC-alphabet such that

           A8: (S . (l + 1)) = Al2 & (S . (l + 2)) = ( FCEx Al2) by A5, A6, NAT_1: 19;

          (S . (l + 1)) c= (S . (l + 2)) by A8, QC_TRANS:def 1;

          hence thesis by A4, A5, NAT_1: 16, XXREAL_0: 2;

        end;

        for n be Nat holds A[n] from NAT_1:sch 2( A2, A3);

        then k < (k + 1) implies x in (S . (k + 1));

        hence thesis by NAT_1: 13;

      end;

      hence thesis by QC_TRANS:def 1;

    end;

    definition

      let Al;

      let k be Nat;

      :: GOEDCPUC:def8

      func k -th_FCEx (Al) -> Al -expanding QC-alphabet equals ( the FCEx-Sequence of Al, k . (k + 1));

      coherence by Th4;

    end

    definition

      let Al, PHI;

      :: GOEDCPUC:def9

      mode EF-Sequence of Al,PHI -> Function means

      : Def9: ( dom it ) = NAT & (it . 0 ) = PHI & for n be Nat holds (it . (n + 1)) = ((it . n) \/ ( Example_Formulae_of (n -th_FCEx Al)));

      existence

      proof

        deffunc F1() = PHI;

        deffunc F2( Nat, set) = ($2 \/ ( Example_Formulae_of ($1 -th_FCEx Al)));

        ex f be Function st ( dom f) = NAT & (f . 0 ) = F1() & for n be Nat holds (f . (n + 1)) = F2(n,.) from NAT_1:sch 11;

        hence thesis;

      end;

    end

    theorem :: GOEDCPUC:5

    

     Th5: for k be Nat holds ( FCEx (k -th_FCEx Al)) = ((k + 1) -th_FCEx Al)

    proof

      let k be Nat;

      ((k + 1) + 1) <= ((k + 1) + 1) & 0 < ( 0 + (k + 1));

      then (k + 1) < (k + 2) & 1 <= (k + 1) by NAT_1: 19;

      then

      consider Al2 be QC-alphabet such that

       A1: ( the FCEx-Sequence of Al, (k + 1) . (k + 1)) = Al2 & ( the FCEx-Sequence of Al, (k + 1) . (k + 2)) = ( FCEx Al2) by Def7;

      set X = ( the FCEx-Sequence of Al, (k + 1) . (k + 1));

      X = (k -th_FCEx Al)

      proof

        defpred A[ Nat] means 0 < $1 & $1 <= (k + 1) implies ( the FCEx-Sequence of Al, k . $1) = ( the FCEx-Sequence of Al, (k + 1) . $1);

        

         A2: A[ 0 ];

        

         A3: for n be Nat st A[n] holds A[(n + 1)]

        proof

          let n be Nat;

          assume

           A4: A[n];

          per cases ;

            suppose

             A5: (n + 1) <= (k + 1);

            per cases ;

              suppose

               A6: n = 0 ;

              ( the FCEx-Sequence of Al, k . 1) = Al by Def7

              .= ( the FCEx-Sequence of Al, (k + 1) . 1) by Def7;

              hence A[(n + 1)] by A6;

            end;

              suppose

               A7: n <> 0 ;

              

               A8: 0 < ( 0 + n) & n <= (n + 1) by A7, NAT_1: 11;

               0 < ( 0 + n) by A7;

              then

               A9: 1 <= n by NAT_1: 19;

              

               A10: n < (k + 1) by A5, NAT_1: 13;

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

              then

              consider Al3 be QC-alphabet such that

               A11: ( the FCEx-Sequence of Al, (k + 1) . n) = Al3 & ( the FCEx-Sequence of Al, (k + 1) . (n + 1)) = ( FCEx Al3) by A9, Def7;

              consider Al4 be QC-alphabet such that

               A12: ( the FCEx-Sequence of Al, k . n) = Al4 & ( the FCEx-Sequence of Al, k . (n + 1)) = ( FCEx Al4) by A9, A10, Def7;

              thus A[(n + 1)] by A4, A8, A11, A12, XXREAL_0: 2;

            end;

          end;

            suppose not (n + 1) <= (k + 1);

            hence A[(n + 1)];

          end;

        end;

        for n be Nat holds A[n] from NAT_1:sch 2( A2, A3);

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: GOEDCPUC:6

    

     Th6: for k, n st n <= k holds (n -th_FCEx Al) c= (k -th_FCEx Al)

    proof

      let k;

      defpred P[ Nat] means $1 <= k implies ex j st j = (k - $1) & (j -th_FCEx Al) c= (k -th_FCEx Al);

      

       A1: P[ 0 ];

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A3: P[n];

        per cases ;

          suppose

           A4: (n + 1) <= k;

          then

          consider j such that

           A5: j = (k - n) & (j -th_FCEx Al) c= (k -th_FCEx Al) by A3, NAT_1: 13;

          set j2 = (k - (n + 1));

          reconsider j2 as Element of NAT by A4, NAT_1: 21;

          ( FCEx (j2 -th_FCEx Al)) = (j -th_FCEx Al) by A5, Th5;

          then (j2 -th_FCEx Al) c= (j -th_FCEx Al) by QC_TRANS:def 1;

          hence thesis by A5, XBOOLE_1: 1;

        end;

          suppose not (n + 1) <= k;

          hence thesis;

        end;

      end;

      

       A6: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      let n such that

       A7: n <= k;

      set n2 = (k - n);

      reconsider n2 as Element of NAT by A7, NAT_1: 21;

      k = (n + n2);

      then

      consider n3 be Element of NAT such that

       A8: n3 = (k - n2) & (n3 -th_FCEx Al) c= (k -th_FCEx Al) by A6, NAT_1: 11;

      thus thesis by A8;

    end;

    definition

      let Al, PHI;

      let k be Nat;

      :: GOEDCPUC:def10

      func k -th_EF (Al,PHI) -> Subset of ( CQC-WFF (k -th_FCEx Al)) equals ( the EF-Sequence of Al, PHI . k);

      coherence

      proof

        defpred P[ Nat] means ( the EF-Sequence of Al, PHI . $1) is Subset of ( CQC-WFF ($1 -th_FCEx Al));

        

         A1: P[ 0 ]

        proof

          ( 0 -th_FCEx Al) = Al by Def7;

          hence thesis by Def9;

        end;

        

         A2: for n be Nat holds P[n] implies P[(n + 1)]

        proof

          let n be Nat;

          assume

           A3: P[n];

          set E = ( the EF-Sequence of Al, PHI . (n + 1));

          set S = ( the EF-Sequence of Al, PHI . n);

          

           A4: ( Example_Formulae_of (n -th_FCEx Al)) is Subset of ( CQC-WFF ( FCEx (n -th_FCEx Al))) & ( FCEx (n -th_FCEx Al)) = ((n + 1) -th_FCEx Al) by Th5;

          S c= ( CQC-WFF ( FCEx (n -th_FCEx Al)))

          proof

            let p be object;

            assume

             A5: p in S;

            reconsider p as Element of ( CQC-WFF (n -th_FCEx Al)) by A3, A5;

            p is Element of ( CQC-WFF ( FCEx (n -th_FCEx Al))) by QC_TRANS: 7;

            hence thesis;

          end;

          then (S \/ ( Example_Formulae_of (n -th_FCEx Al))) c= ( CQC-WFF ((n + 1) -th_FCEx Al)) by A4, XBOOLE_1: 8;

          hence thesis by Def9;

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

        hence thesis;

      end;

    end

    theorem :: GOEDCPUC:7

    

     Th7: for r, s, x holds (Al2 -Cast (r 'or' s)) = ((Al2 -Cast r) 'or' (Al2 -Cast s)) & (Al2 -Cast ( Ex (x,r))) = ( Ex ((Al2 -Cast x),(Al2 -Cast r)))

    proof

      let r, s, x;

      

       A1: (Al2 -Cast ( 'not' r)) = ( 'not' (Al2 -Cast r)) & (Al2 -Cast ( 'not' s)) = ( 'not' (Al2 -Cast s)) by QC_TRANS: 8;

      

      thus (Al2 -Cast (r 'or' s)) = (Al2 -Cast ( 'not' (( 'not' r) '&' ( 'not' s)))) by QC_LANG2:def 3

      .= ( 'not' (Al2 -Cast (( 'not' r) '&' ( 'not' s)))) by QC_TRANS: 8

      .= ( 'not' (( 'not' (Al2 -Cast r)) '&' ( 'not' (Al2 -Cast s)))) by A1, QC_TRANS: 8

      .= ((Al2 -Cast r) 'or' (Al2 -Cast s)) by QC_LANG2:def 3;

      

      thus (Al2 -Cast ( Ex (x,r))) = (Al2 -Cast ( 'not' ( All (x,( 'not' r))))) by QC_LANG2:def 5

      .= ( 'not' (Al2 -Cast ( All (x,( 'not' r))))) by QC_TRANS: 8

      .= ( 'not' ( All ((Al2 -Cast x),(Al2 -Cast ( 'not' r))))) by QC_TRANS: 8

      .= ( 'not' ( All ((Al2 -Cast x),( 'not' (Al2 -Cast r))))) by QC_TRANS: 8

      .= ( Ex ((Al2 -Cast x),(Al2 -Cast r))) by QC_LANG2:def 5;

    end;

    theorem :: GOEDCPUC:8

    

     Th8: for p, q, A, J, v holds ((J,v) |= p or (J,v) |= q) iff (J,v) |= (p 'or' q)

    proof

      let p, q, A, J, v;

      thus ((J,v) |= p or (J,v) |= q) implies (J,v) |= (p 'or' q)

      proof

        assume (J,v) |= p or (J,v) |= q;

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

        then not (J,v) |= (( 'not' p) '&' ( 'not' q)) by VALUAT_1: 18;

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

        hence thesis by QC_LANG2:def 3;

      end;

      thus (J,v) |= (p 'or' q) implies ((J,v) |= p or (J,v) |= q)

      proof

        assume (J,v) |= (p 'or' q);

        then (J,v) |= ( 'not' (( 'not' p) '&' ( 'not' q))) by QC_LANG2:def 3;

        then not (J,v) |= ( 'not' p) or not (J,v) |= ( 'not' q) by VALUAT_1: 17, VALUAT_1: 18;

        hence (J,v) |= p or (J,v) |= q by VALUAT_1: 17;

      end;

    end;

    theorem :: GOEDCPUC:9

    

     Th9: (PHI \/ ( Example_Formulae_of Al)) is Consistent Subset of ( CQC-WFF ( FCEx Al))

    proof

      reconsider Al2 = ( FCEx Al) as Al -expanding QC-alphabet;

      for s be object st s in ( CQC-WFF Al) holds s in ( CQC-WFF Al2)

      proof

        let s be object;

        assume s in ( CQC-WFF Al);

        then

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

        s is Element of ( CQC-WFF Al2) by QC_TRANS: 7;

        hence thesis;

      end;

      then

       A1: ( CQC-WFF Al) c= ( CQC-WFF Al2);

      then PHI c= ( CQC-WFF Al2) & ( Example_Formulae_of Al) c= ( CQC-WFF Al2);

      then

      reconsider B = (PHI \/ ( Example_Formulae_of Al)) as Subset of ( CQC-WFF Al2) by XBOOLE_1: 8;

      B is Consistent

      proof

        assume B is Inconsistent;

        then

        consider CHI2 be Subset of ( CQC-WFF Al2) such that

         A2: CHI2 c= B & CHI2 is finite & CHI2 is Inconsistent by HENMODEL: 7;

        reconsider CHI2 as finite Subset of ( CQC-WFF Al2) by A2;

        consider Al1 be countable QC-alphabet such that

         A3: CHI2 is finite Subset of ( CQC-WFF Al1) & Al2 is Al1 -expanding by QC_TRANS: 20;

        reconsider Al2 as Al1 -expanding QC-alphabet by A3;

        consider CHI1 be Subset of ( CQC-WFF Al1) such that

         A4: CHI1 = CHI2 by A3;

        reconsider CHI1 as finite Subset of ( CQC-WFF Al1) by A4;

        set PHI1 = (CHI1 /\ PHI);

        PHI1 c= CHI1 & CHI1 c= ( CQC-WFF Al1) by XBOOLE_1: 18;

        then

        reconsider PHI1 as Subset of ( CQC-WFF Al1) by XBOOLE_1: 1;

        reconsider Al2 as Al -expanding QC-alphabet;

        PHI is Subset of ( CQC-WFF Al2) by A1, XBOOLE_1: 1;

        then

        consider PHIp be Subset of ( CQC-WFF Al2) such that

         A5: PHIp = PHI;

        set PHI2 = (CHI2 /\ PHIp);

        reconsider PHI2 as Subset of ( CQC-WFF Al2);

        PHI1 is Consistent

        proof

          reconsider Al2 as Al1 -expanding QC-alphabet;

          PHI is Al2 -Consistent by QC_TRANS: 23;

          then PHIp is Consistent & PHI2 c= PHIp by A5, QC_TRANS:def 2, XBOOLE_1: 18;

          then PHI2 is Consistent & PHI2 = PHI1 by A4, A5, QC_TRANS: 22;

          then PHI2 is Al1 -Consistent by QC_TRANS: 18;

          hence PHI1 is Consistent by A4, A5, QC_TRANS:def 2;

        end;

        then

        reconsider PHI1 as Consistent Subset of ( CQC-WFF Al1);

        ( still_not-bound_in PHI1) is finite;

        then

        consider CZ be Consistent Subset of ( CQC-WFF Al1), JH be Henkin_interpretation of CZ such that

         A6: (JH,( valH Al1)) |= PHI1 by GOEDELCP: 34;

        consider A2 be non empty set, J2 be interpretation of Al2, A2, v2 be Element of ( Valuations_in (Al2,A2)) such that

         A7: (J2,v2) |= PHI2 by A4, A5, A6, QC_TRANS: 21;

        set Ex2 = (CHI2 /\ ( Example_Formulae_of Al));

        reconsider Ex2 as Subset of ( CQC-WFF Al2);

        

         A8: CHI2 = (CHI2 /\ (PHIp \/ ( Example_Formulae_of Al))) by A2, A5, XBOOLE_1: 28

        .= (PHI2 \/ Ex2) by XBOOLE_1: 23;

        ex A be non empty set, J be interpretation of Al2, A, v be Element of ( Valuations_in (Al2,A)) st (J,v) |= (PHI2 \/ Ex2)

        proof

          defpred P[ set] means ex A be non empty set, J be interpretation of Al2, A, v be Element of ( Valuations_in (Al2,A)), Ex3 be Subset of ( CQC-WFF Al2) st Ex3 = $1 & (J,v) |= (PHI2 \/ Ex3);

          

           A9: Ex2 is finite;

          (J2,v2) |= (PHI2 \/ ( {} ( CQC-WFF Al2))) by A7;

          then

           A10: P[ {} ];

          

           A11: for b,B be set st b in Ex2 & B c= Ex2 & P[B] holds P[(B \/ {b})]

          proof

            let b,B be set such that

             A12: b in Ex2 & B c= Ex2 & P[B];

            reconsider B as Subset of ( CQC-WFF Al2) by A12;

            consider A be non empty set, J be interpretation of Al2, A, v be Element of ( Valuations_in (Al2,A)) such that

             A13: (J,v) |= (PHI2 \/ B) by A12;

            Ex2 c= ( Example_Formulae_of Al) by XBOOLE_1: 18;

            then b in ( Example_Formulae_of Al) by A12;

            then

            consider p, x such that

             A14: b = ( Example_Formula_of (p,x));

            set fc = ( Example_of (p,x));

            set x2 = (Al2 -Cast x);

            set p2 = (Al2 -Cast p);

            reconsider fc, x2 as bound_QC-variable of Al2;

            reconsider p2 as Element of ( CQC-WFF Al2);

            reconsider b as Element of ( CQC-WFF Al2) by A14;

            

             A15: (J,v) |= b implies thesis

            proof

              assume

               A16: (J,v) |= b;

              for q2 be Element of ( CQC-WFF Al2) st q2 in (PHI2 \/ (B \/ {b})) holds (J,v) |= q2

              proof

                let q2 be Element of ( CQC-WFF Al2);

                assume q2 in (PHI2 \/ (B \/ {b}));

                then q2 in ((PHI2 \/ B) \/ {b}) by XBOOLE_1: 4;

                then

                 A17: q2 in (PHI2 \/ B) or q2 in {b} by XBOOLE_0:def 3;

                per cases ;

                  suppose q2 in (PHI2 \/ B);

                  hence thesis by A13, CALCUL_1:def 11;

                end;

                  suppose not q2 in (PHI2 \/ B);

                  hence thesis by A16, A17, TARSKI:def 1;

                end;

              end;

              hence thesis by CALCUL_1:def 11;

            end;

            per cases ;

              suppose not (J,v) |= ( Ex (x2,p2));

              then (J,v) |= ( 'not' ( Ex (x2,p2))) by VALUAT_1: 17;

              hence thesis by A14, A15, Th8;

            end;

              suppose (J,v) |= ( Ex (x2,p2));

              then

              consider a be Element of A such that

               A18: (J,(v . (x2 | a))) |= p2 by GOEDELCP: 9;

              reconsider vp = (v . (fc | a)) as Element of ( Valuations_in (Al2,A));

              

               A19: for p2 be Element of ( CQC-WFF Al2) st p2 is Element of ( CQC-WFF Al) holds (v | ( still_not-bound_in p2)) = (vp | ( still_not-bound_in p2))

              proof

                let p2 be Element of ( CQC-WFF Al2);

                assume p2 is Element of ( CQC-WFF Al);

                then

                consider pp be Element of ( CQC-WFF Al) such that

                 A20: pp = p2;

                 not [ the free_symbol of Al, [x, p]] in ( QC-symbols Al) by Def2;

                then not [4, [ the free_symbol of Al, [x, p]]] in [: {4}, ( QC-symbols Al):] by ZFMISC_1: 87;

                then not fc in ( bound_QC-variables Al) by QC_LANG1:def 4;

                then not fc in ( still_not-bound_in pp);

                then not fc in ( still_not-bound_in (Al2 -Cast pp)) by QC_TRANS: 12;

                then not fc in ( still_not-bound_in p2) by A20, QC_TRANS:def 3;

                hence (v | ( still_not-bound_in p2)) = (vp | ( still_not-bound_in p2)) by CALCUL_1: 26;

              end;

              p2 = p by QC_TRANS:def 3;

              then (v | ( still_not-bound_in p2)) = (vp | ( still_not-bound_in p2)) by A19;

              then ((v . (x2 | a)) | ( still_not-bound_in p2)) = ((vp . (x2 | a)) | ( still_not-bound_in p2)) by SUBLEMMA: 64;

              then (J,(vp . (x2 | a))) |= p2 & (vp . fc) = a by A18, SUBLEMMA: 49, SUBLEMMA: 68;

              then

               A21: (J,vp) |= (p2 . (x2,fc)) by CALCUL_1: 24;

              for q2 be Element of ( CQC-WFF Al2) st q2 in (PHI2 \/ (B \/ {b})) holds (J,vp) |= q2

              proof

                let q2 be Element of ( CQC-WFF Al2);

                assume q2 in (PHI2 \/ (B \/ {b}));

                then q2 in ((PHI2 \/ B) \/ {b}) by XBOOLE_1: 4;

                then

                 A22: q2 in (PHI2 \/ B) or q2 in {b} by XBOOLE_0:def 3;

                per cases ;

                  suppose

                   A23: q2 in PHI2;

                  then

                   A24: q2 in (PHI2 \/ B) by XBOOLE_0:def 3;

                  PHI2 c= PHI & PHI c= ( CQC-WFF Al) by A5, XBOOLE_1: 18;

                  then PHI2 c= ( CQC-WFF Al);

                  then (v | ( still_not-bound_in q2)) = (vp | ( still_not-bound_in q2)) & (J,v) |= q2 by A13, A19, A23, A24, CALCUL_1:def 11;

                  hence (J,vp) |= q2 by SUBLEMMA: 68;

                end;

                  suppose

                   A25: q2 in B;

                  B c= ( Example_Formulae_of Al) by A12, XBOOLE_1: 18;

                  then q2 in ( Example_Formulae_of Al) by A25;

                  then

                  consider r, y such that

                   A26: q2 = ( Example_Formula_of (r,y));

                  set fcr = ( Example_of (r,y));

                  set y2 = (Al2 -Cast y);

                  set r2 = (Al2 -Cast r);

                  reconsider fcr, y2 as bound_QC-variable of Al2;

                  reconsider r2 as Element of ( CQC-WFF Al2);

                  per cases ;

                    suppose fcr = fc;

                    then [ the free_symbol of Al, [x, p]] = [ the free_symbol of Al, [y, r]] by XTUPLE_0: 1;

                    then [x, p] = [y, r] by XTUPLE_0: 1;

                    then r = p & x = y by XTUPLE_0: 1;

                    hence thesis by A21, A26, Th8;

                  end;

                    suppose

                     A27: not fcr = fc;

                    

                     A28: q2 in (PHI2 \/ B) by A25, XBOOLE_0:def 3;

                    per cases ;

                      suppose

                       A29: (J,v) |= ( 'not' ( Ex (y2,r2)));

                      set fml = ( 'not' ( Ex (y2,r2)));

                      ( 'not' ( Ex (y,r))) = (Al2 -Cast ( 'not' ( Ex (y,r)))) by QC_TRANS:def 3

                      .= ( 'not' (Al2 -Cast ( Ex (y,r)))) by QC_TRANS: 8

                      .= fml by Th7;

                      then (v | ( still_not-bound_in fml)) = (vp | ( still_not-bound_in fml)) & (J,v) |= fml by A19, A29;

                      then (J,vp) |= fml by SUBLEMMA: 68;

                      hence (J,vp) |= q2 by A26, Th8;

                    end;

                      suppose not (J,v) |= ( 'not' ( Ex (y2,r2)));

                      then (J,v) |= (r2 . (y2,fcr)) by A13, A26, A28, Th8, CALCUL_1:def 11;

                      then

                      consider a2 be Element of A such that

                       A30: (v . fcr) = a2 & (J,(v . (y2 | a2))) |= r2 by CALCUL_1: 24;

                      

                       A31: (vp . fcr) = a2 by A27, A30, SUBLEMMA: 48;

                       not [ the free_symbol of Al, [x, p]] in ( QC-symbols Al) by Def2;

                      then not [4, [ the free_symbol of Al, [x, p]]] in [: {4}, ( QC-symbols Al):] by ZFMISC_1: 87;

                      then not fc in ( bound_QC-variables Al) by QC_LANG1:def 4;

                      then not fc in ( still_not-bound_in r);

                      then not fc in ( still_not-bound_in r2) by QC_TRANS: 12;

                      then ((v . (fc | a)) | ( still_not-bound_in r2)) = (v | ( still_not-bound_in r2)) by CALCUL_1: 26;

                      then ((vp . (y2 | a2)) | ( still_not-bound_in r2)) = ((v . (y2 | a2)) | ( still_not-bound_in r2)) by SUBLEMMA: 64;

                      then (J,(vp . (y2 | a2))) |= r2 by A30, SUBLEMMA: 68;

                      then (J,vp) |= (r2 . (y2,fcr)) by A31, CALCUL_1: 24;

                      hence thesis by A26, Th8;

                    end;

                  end;

                end;

                  suppose not q2 in PHI2 & not q2 in B;

                  then q2 = b by A22, TARSKI:def 1, XBOOLE_0:def 3;

                  hence thesis by A14, A21, Th8;

                end;

              end;

              hence thesis by CALCUL_1:def 11;

            end;

          end;

           P[Ex2] from FINSET_1:sch 2( A9, A10, A11);

          hence thesis;

        end;

        hence contradiction by A2, A8, HENMODEL: 12;

      end;

      hence thesis;

    end;

    begin

    theorem :: GOEDCPUC:10

    

     Th10: ex Al2 be Al -expanding QC-alphabet, PSI be Consistent Subset of ( CQC-WFF Al2) st PHI c= PSI & PSI is with_examples

    proof

      deffunc S( Nat) = ($1 -th_FCEx Al);

      deffunc PSI( Nat) = ($1 -th_EF (Al,PHI));

      set Al2 = ( union the set of all S(n));

      set PSI = ( union the set of all PSI(n));

      

       A1: PHI c= PSI

      proof

        PHI = PSI(0) by Def9;

        then PHI in the set of all PSI(n);

        hence PHI c= PSI by ZFMISC_1: 74;

      end;

      

       A2: Al c= Al2 & for n holds S(n) c= Al2

      proof

        Al = S(0) by Def7;

        then Al in the set of all S(n);

        hence Al c= Al2 by ZFMISC_1: 74;

        let n;

         S(n) in the set of all S(k);

        hence S(n) c= Al2 by ZFMISC_1: 74;

      end;

      reconsider Al2 as non empty set by A2;

      set Al2sym = ( union the set of all ( QC-symbols S(n)));

       NAT c= Al2sym & Al2 = [: NAT , Al2sym:]

      proof

        for s be object st s in Al2 holds s in [: NAT , Al2sym:]

        proof

          let s be object such that

           A3: s in Al2;

          consider P be set such that

           A4: s in P & P in the set of all S(n) by A3, TARSKI:def 4;

          consider n be Element of NAT such that

           A5: P = S(n) by A4;

          

           A6: for y be set st y in ( QC-symbols S(n)) holds y in Al2sym

          proof

            let y be set such that

             A7: y in ( QC-symbols S(n));

            ( QC-symbols S(n)) in the set of all ( QC-symbols S(k));

            hence y in Al2sym by A7, TARSKI:def 4;

          end;

          s in [: NAT , ( QC-symbols S(n)):] by A5, A4, QC_LANG1: 5;

          then ex k,y be object st k in NAT & y in ( QC-symbols S(n)) & s = [k, y] by ZFMISC_1:def 2;

          then ex k be set, y be set st k in NAT & y in Al2sym & s = [k, y] by A6;

          hence thesis by ZFMISC_1: 87;

        end;

        then

         A8: Al2 c= [: NAT , Al2sym:];

        ( QC-symbols Al) = ( QC-symbols S(0)) by Def7;

        then ( QC-symbols Al) in the set of all ( QC-symbols S(n));

        then NAT c= ( QC-symbols Al) & ( QC-symbols Al) c= Al2sym by QC_LANG1: 3, ZFMISC_1: 74;

        hence NAT c= Al2sym;

        for x be object st x in [: NAT , Al2sym:] holds x in Al2

        proof

          let x be object such that

           A9: x in [: NAT , Al2sym:];

          consider m,y be object such that

           A10: m in NAT & y in Al2sym & x = [m, y] by A9, ZFMISC_1:def 2;

          consider P be set such that

           A11: y in P & P in the set of all ( QC-symbols S(n)) by A10, TARSKI:def 4;

          consider n be Element of NAT such that

           A12: P = ( QC-symbols S(n)) by A11;

           [m, y] in [: NAT , ( QC-symbols S(n)):] by A10, A11, A12, ZFMISC_1: 87;

          then

           A13: [m, y] in S(n) by QC_LANG1: 5;

           S(n) c= Al2 by A2;

          hence thesis by A10, A13;

        end;

        then [: NAT , Al2sym:] c= Al2;

        hence Al2 = [: NAT , Al2sym:] by A8, XBOOLE_0:def 10;

      end;

      then

      reconsider Al2 as QC-alphabet by QC_LANG1:def 1;

      reconsider Al2 as Al -expanding QC-alphabet by A2, QC_TRANS:def 1;

      for p be object st p in PSI holds p in ( CQC-WFF Al2)

      proof

        let p be object such that

         A14: p in PSI;

        consider P be set such that

         A15: p in P & P in the set of all PSI(n) by A14, TARSKI:def 4;

        consider n be Element of NAT such that

         A16: P = PSI(n) by A15;

        Al2 is S(n) -expanding QC-alphabet by A2, QC_TRANS:def 1;

        then p is Element of ( CQC-WFF Al2) by QC_TRANS: 7, A15, A16;

        hence thesis;

      end;

      then

      reconsider PSI as Subset of ( CQC-WFF Al2) by TARSKI:def 3;

      PSI is Consistent

      proof

        defpred C[ Nat] means PSI($1) is Consistent & PSI($1) is Al2 -Consistent;

        

         A17: C[ 0 ]

        proof

          

           A18: PSI(0) = PHI by Def9;

          PHI is Al2 -Consistent by QC_TRANS: 23;

          then S(0) = Al & for S be Subset of ( CQC-WFF Al2) st PSI(0) = S holds S is Consistent by A18, Def7, QC_TRANS:def 2;

          hence thesis by A18, QC_TRANS:def 2;

        end;

        

         A19: for n be Nat holds C[n] implies C[(n + 1)]

        proof

          let n be Nat;

          

           A20: ( FCEx S(n)) = S(+) by Th5;

          reconsider Al2 as S(+) -expanding QC-alphabet by A2, QC_TRANS:def 1;

          assume C[n];

          then

          reconsider PSIn = PSI(n) as Consistent Subset of ( CQC-WFF S(n));

           PSI(+) = (PSIn \/ ( Example_Formulae_of S(n))) by Def9;

          then

          reconsider PSIn1 = PSI(+) as Consistent Subset of ( CQC-WFF S(+)) by A20, Th9;

          PSIn1 is Al2 -Consistent by QC_TRANS: 23;

          hence thesis;

        end;

        

         A21: for n be Nat holds C[n] from NAT_1:sch 2( A17, A19);

        

         A22: for n holds PSI(n) c= PSI

        proof

          let n;

          let p be object such that

           A23: p in PSI(n);

           PSI(n) in the set of all PSI(k);

          hence p in PSI by A23, TARSKI:def 4;

        end;

        

         A24: for n holds PSI(n) in ( bool ( CQC-WFF Al2))

        proof

          let n;

           PSI(n) c= PSI & PSI c= ( CQC-WFF Al2) by A22;

          then PSI(n) c= ( CQC-WFF Al2);

          hence thesis;

        end;

        consider f be Function such that

         A25: ( dom f) = NAT & for n holds (f . n) = PSI(n) from FUNCT_1:sch 4;

        for y be object st y in ( rng f) holds y in ( bool ( CQC-WFF Al2))

        proof

          let y be object such that

           A26: y in ( rng f);

          consider x be object such that

           A27: x in ( dom f) & y = (f . x) by A26, FUNCT_1:def 3;

          reconsider x as Element of NAT by A25, A27;

          (f . x) = PSI(x) by A25;

          hence thesis by A24, A27;

        end;

        then

        reconsider f as sequence of ( bool ( CQC-WFF Al2)) by A25, FUNCT_2: 2, TARSKI:def 3;

        set PSIp = ( union ( rng f));

        f in ( Funcs ( NAT ,( bool ( CQC-WFF Al2)))) by FUNCT_2: 8;

        then ( union ( rng f)) c= ( union ( bool ( CQC-WFF Al2))) by ZFMISC_1: 77, FUNCT_2: 92;

        then

        reconsider PSIp as Subset of ( CQC-WFF Al2) by ZFMISC_1: 81;

        for n,m be Nat st m in ( dom f) & n in ( dom f) & n < m holds (f . n) is Consistent & (f . n) c= (f . m)

        proof

          let nn,mm be Nat such that

           A28: mm in ( dom f) & nn in ( dom f) & nn < mm;

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

          (f . n) is Subset of ( CQC-WFF Al2) & (f . n) = PSI(n) & PSI(n) is Al2 -Consistent by A21, A25;

          hence (f . nn) is Consistent by QC_TRANS:def 2;

          defpred S[ Nat] means $1 <= m implies ex k st k = (m - $1) & PSI(k) c= PSI(m);

          

           A29: S[ 0 ];

          

           A30: for k be Nat holds S[k] implies S[(k + 1)]

          proof

            let k be Nat;

            assume

             A31: S[k];

            set j1 = (m - k);

            set j2 = (m - (k + 1));

            per cases ;

              suppose

               A32: (k + 1) <= m;

              then k <= m by NAT_1: 13;

              then

              reconsider j1, j2 as Element of NAT by A32, NAT_1: 21;

               PSI(+) = (( the EF-Sequence of Al, PHI . j2) \/ ( Example_Formulae_of (j2 -th_FCEx Al))) by Def9;

              then PSI(j2) c= PSI(j1) & PSI(j1) c= PSI(m) by A31, A32, NAT_1: 13, XBOOLE_1: 7;

              hence thesis by XBOOLE_1: 1;

            end;

              suppose not (k + 1) <= m;

              hence thesis;

            end;

          end;

          

           A33: for k be Nat holds S[k] from NAT_1:sch 2( A29, A30);

          set k = (m - n);

          reconsider k as Element of NAT by A28, NAT_1: 21;

           S[k] & k <= (k + n) by A33, NAT_1: 11;

          then PSI(n) c= PSI(m) & (f . n) = PSI(n) & (f . m) = PSI(m) by A25;

          hence (f . nn) c= (f . mm);

        end;

        then

        reconsider PSIp as Consistent Subset of ( CQC-WFF Al2) by HENMODEL: 11;

        for y be object st y in the set of all PSI(n) holds ex x be object st x in ( dom f) & y = (f . x)

        proof

          let P be object such that

           A34: P in the set of all PSI(n);

          consider n such that

           A35: P = PSI(n) by A34;

          n in ( dom f) & (f . n) = P by A25, A35;

          hence thesis;

        end;

        then

         A36: the set of all PSI(n) c= ( rng f) by FUNCT_1: 9;

        for y be object st y in ( rng f) holds y in the set of all PSI(n)

        proof

          let y be object such that

           A37: y in ( rng f);

          consider x be object such that

           A38: x in ( dom f) & y = (f . x) by A37, FUNCT_1:def 3;

          reconsider x as Element of NAT by A25, A38;

          (f . x) = PSI(x) by A25;

          hence thesis by A38;

        end;

        then ( rng f) c= the set of all PSI(n);

        then PSIp = PSI by A36, XBOOLE_0:def 10;

        hence thesis;

      end;

      then

      reconsider PSI as Consistent Subset of ( CQC-WFF Al2);

      set S = the set of all S(n);

       S(0) in S;

      then

      reconsider S as non empty set;

      

       A39: for a,b be set st a in S & b in S holds ex c be set st (a \/ b) c= c & c in S

      proof

        let a,b be set such that

         A40: a in S & b in S;

        consider i such that

         A41: a = S(i) by A40;

        consider j such that

         A42: b = S(j) by A40;

        per cases ;

          suppose j <= i;

          then S(j) c= S(i) by Th6;

          hence thesis by A40, A41, A42, XBOOLE_1: 8;

        end;

          suppose not j <= i;

          then S(i) c= S(j) by Th6;

          hence thesis by A40, A41, A42, XBOOLE_1: 8;

        end;

      end;

      

       A43: for p be Element of ( CQC-WFF Al2) holds ex n st p is Element of ( CQC-WFF S(n))

      proof

        defpred P[ Element of ( CQC-WFF Al2)] means ex n st $1 is Element of ( CQC-WFF S(n));

        

         A44: P[( VERUM Al2)]

        proof

          reconsider Al2 as S(0) -expanding QC-alphabet by A2, QC_TRANS:def 1;

          ( VERUM S(0)) in ( CQC-WFF S(0));

          then (Al2 -Cast ( VERUM S(0))) in ( CQC-WFF S(0)) by QC_TRANS:def 3;

          then ( VERUM Al2) in ( CQC-WFF S(0)) by QC_TRANS: 8;

          hence thesis;

        end;

        

         A45: for k be Nat holds for P be QC-pred_symbol of k, Al2, l be CQC-variable_list of k, Al2 holds P[(P ! l)]

        proof

          let k be Nat;

          let P be QC-pred_symbol of k, Al2, l be CQC-variable_list of k, Al2;

          ex n st ( rng l) c= ( bound_QC-variables S(n)) & P is QC-pred_symbol of k, S(n)

          proof

            

             A46: ( rng l) c= ( bound_QC-variables Al2) & {P} c= ( QC-pred_symbols Al2) by ZFMISC_1: 31;

            ( bound_QC-variables Al2) c= ( QC-variables Al2) & ( QC-variables Al2) c= [: NAT , ( QC-symbols Al2):] by QC_LANG1: 4;

            then

             A47: ( bound_QC-variables Al2) c= [: NAT , ( QC-symbols Al2):] & ( QC-pred_symbols Al2) c= [: NAT , ( QC-symbols Al2):] by QC_LANG1: 6;

            then ( rng l) c= [: NAT , ( QC-symbols Al2):] & {P} c= [: NAT , ( QC-symbols Al2):] by A46;

            then ( rng l) c= Al2 & {P} c= Al2 by QC_LANG1: 5;

            then (( rng l) \/ {P}) c= ( union S) & (( rng l) \/ {P}) is finite by XBOOLE_1: 8;

            then

            consider a be set such that

             A48: a in S & (( rng l) \/ {P}) c= a by A39, COHSP_1: 6, COHSP_1: 13;

            consider n such that

             A49: a = S(n) by A48;

            take n;

            

             A50: ( rng l) c= (( rng l) \/ {P}) & {P} c= (( rng l) \/ {P}) by XBOOLE_1: 7;

            for s be object st s in ( rng l) holds s in ( bound_QC-variables S(n))

            proof

              let s be object such that

               A51: s in ( rng l);

              s in ( bound_QC-variables Al2) by A51;

              then s in [: {4}, ( QC-symbols Al2):] by QC_LANG1:def 4;

              then

              consider s1,s2 be object such that

               A52: s1 in {4} & s2 in ( QC-symbols Al2) & s = [s1, s2] by ZFMISC_1:def 2;

              ( rng l) c= S(n) & {P} c= S(n) by A48, A49, A50;

              then s in S(n) by A51;

              then s in [: NAT , ( QC-symbols S(n)):] by QC_LANG1: 5;

              then

              consider s3,s4 be object such that

               A53: s3 in NAT & s4 in ( QC-symbols S(n)) & s = [s3, s4] by ZFMISC_1:def 2;

              s = [s1, s4] by A52, A53, XTUPLE_0: 1;

              then s in [: {4}, ( QC-symbols S(n)):] by A52, A53, ZFMISC_1:def 2;

              hence thesis by QC_LANG1:def 4;

            end;

            hence ( rng l) c= ( bound_QC-variables S(n));

            thus P is QC-pred_symbol of k, S(n)

            proof

              P in [: NAT , ( QC-symbols Al2):] by A47;

              then

              consider p1,p2 be object such that

               A54: p1 in NAT & p2 in ( QC-symbols Al2) & P = [p1, p2] by ZFMISC_1:def 2;

              ( rng l) c= S(n) & P in S(n) by A48, A49, A50, ZFMISC_1: 31;

              then P in [: NAT , ( QC-symbols S(n)):] by QC_LANG1: 5;

              then

              reconsider p2 as QC-symbol of S(n) by A54, ZFMISC_1: 87;

              

               A55: (P `1 ) = (( the_arity_of P) + 7) by QC_LANG1:def 8

              .= (k + 7) by QC_LANG1: 11;

              reconsider p1 as Element of NAT by A54;

              (P `1 ) = (7 + ( the_arity_of P)) & (P `1 ) = p1 by A54, QC_LANG1:def 8;

              then 7 <= p1 by NAT_1: 11;

              then [p1, p2] in { [m, x] where m be Nat, x be QC-symbol of S(n) : 7 <= m };

              then

              reconsider P as QC-pred_symbol of S(n) by A54, QC_LANG1:def 7;

              ( the_arity_of P) = k by A55, QC_LANG1:def 8;

              then P in { Q where Q be QC-pred_symbol of S(n) : ( the_arity_of Q) = k };

              hence thesis by QC_LANG1:def 9;

            end;

          end;

          then

          consider n such that

           A56: ( rng l) c= ( bound_QC-variables S(n)) & P is QC-pred_symbol of k, S(n);

          l is CQC-variable_list of k, S(n) by A56, FINSEQ_1:def 4, XBOOLE_1: 1;

          then

          consider l2 be CQC-variable_list of k, S(n), P2 be QC-pred_symbol of k, S(n) such that

           A57: l2 = l & P = P2 by A56;

          reconsider Al2 as S(n) -expanding QC-alphabet by A2, QC_TRANS:def 1;

          

           A58: (Al2 -Cast P2) = P & (Al2 -Cast l2) = l by A57, QC_TRANS:def 5, QC_TRANS:def 6;

          (P2 ! l2) = (Al2 -Cast (P2 ! l2)) by QC_TRANS:def 3

          .= (P ! l) by A58, QC_TRANS: 8;

          hence thesis;

        end;

        

         A59: for r be Element of ( CQC-WFF Al2) st P[r] holds P[( 'not' r)]

        proof

          let r be Element of ( CQC-WFF Al2);

          assume P[r];

          then

          consider n such that

           A60: r is Element of ( CQC-WFF S(n));

          consider r2 be Element of ( CQC-WFF S(n)) such that

           A61: r = r2 by A60;

          reconsider Al2 as S(n) -expanding QC-alphabet by A2, QC_TRANS:def 1;

          ( 'not' r2) = (Al2 -Cast ( 'not' r2)) by QC_TRANS:def 3

          .= ( 'not' (Al2 -Cast r2)) by QC_TRANS: 8

          .= ( 'not' r) by A61, QC_TRANS:def 3;

          hence thesis;

        end;

        

         A62: for r,s be Element of ( CQC-WFF Al2) st P[r] & P[s] holds P[(r '&' s)]

        proof

          let r,s be Element of ( CQC-WFF Al2);

          assume P[r] & P[s];

          then

          consider n, m such that

           A63: r is Element of ( CQC-WFF S(n)) & s is Element of ( CQC-WFF S(m));

          per cases ;

            suppose n <= m;

            then

            reconsider Sm = S(m) as S(n) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

            r is Element of ( CQC-WFF Sm) by A63, QC_TRANS: 7;

            then

            consider r2,s2 be Element of ( CQC-WFF Sm) such that

             A64: r2 = r & s2 = s by A63;

            reconsider Al2 as Sm -expanding QC-alphabet by A2, QC_TRANS:def 1;

            

             A65: r = (Al2 -Cast r2) & s = (Al2 -Cast s2) by A64, QC_TRANS:def 3;

            (r2 '&' s2) = (Al2 -Cast (r2 '&' s2)) by QC_TRANS:def 3

            .= (r '&' s) by A65, QC_TRANS: 8;

            hence thesis;

          end;

            suppose not n <= m;

            then

            reconsider Sn = S(n) as S(m) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

            s is Element of ( CQC-WFF Sn) by A63, QC_TRANS: 7;

            then

            consider r2,s2 be Element of ( CQC-WFF Sn) such that

             A66: r2 = r & s2 = s by A63;

            reconsider Al2 as Sn -expanding QC-alphabet by A2, QC_TRANS:def 1;

            

             A67: r = (Al2 -Cast r2) & s = (Al2 -Cast s2) by A66, QC_TRANS:def 3;

            (r2 '&' s2) = (Al2 -Cast (r2 '&' s2)) by QC_TRANS:def 3

            .= (r '&' s) by A67, QC_TRANS: 8;

            hence thesis;

          end;

        end;

        for x be bound_QC-variable of Al2, r be Element of ( CQC-WFF Al2) st P[r] holds P[( All (x,r))]

        proof

          let x be bound_QC-variable of Al2, r be Element of ( CQC-WFF Al2);

          x in ( QC-variables Al2) & ( QC-variables Al2) c= [: NAT , ( QC-symbols Al2):] by QC_LANG1: 4;

          then x in [: NAT , ( QC-symbols Al2):] & Al2 = [: NAT , ( QC-symbols Al2):] by QC_LANG1: 5;

          then {x} c= ( union S) & {x} is finite by ZFMISC_1: 31;

          then

          consider a be set such that

           A68: a in S & {x} c= a by A39, COHSP_1: 6, COHSP_1: 13;

          consider n such that

           A69: a = S(n) by A68;

          assume P[r];

          then

          consider m such that

           A70: r is Element of ( CQC-WFF S(m));

          x in ( bound_QC-variables Al2);

          then x in [: {4}, ( QC-symbols Al2):] by QC_LANG1:def 4;

          then

          consider x1,x2 be object such that

           A71: x1 in {4} & x2 in ( QC-symbols Al2) & x = [x1, x2] by ZFMISC_1:def 2;

          

           A72: x in S(n) by A68, A69, ZFMISC_1: 31;

          per cases ;

            suppose

             A73: n <= m;

            then

            reconsider Sm = S(m) as S(n) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

             S(n) c= S(m) by A73, Th6;

            then x in S(m) by A72;

            then x in [: NAT , ( QC-symbols S(m)):] by QC_LANG1: 5;

            then

            consider x3,x4 be object such that

             A74: x3 in NAT & x4 in ( QC-symbols S(m)) & x = [x3, x4] by ZFMISC_1:def 2;

            x = [x1, x4] by A71, A74, XTUPLE_0: 1;

            then x in [: {4}, ( QC-symbols Sm):] by A71, A74, ZFMISC_1:def 2;

            then x is bound_QC-variable of Sm by QC_LANG1:def 4;

            then

            consider x2 be bound_QC-variable of Sm, r2 be Element of ( CQC-WFF Sm) such that

             A75: x2 = x & r2 = r by A70;

            reconsider Al2 as Sm -expanding QC-alphabet by A2, QC_TRANS:def 1;

            

             A76: r = (Al2 -Cast r2) & x = (Al2 -Cast x2) by A75, QC_TRANS:def 3, QC_TRANS:def 4;

            ( All (x2,r2)) = (Al2 -Cast ( All (x2,r2))) by QC_TRANS:def 3

            .= ( All (x,r)) by A76, QC_TRANS: 8;

            hence thesis;

          end;

            suppose not n <= m;

            then

            reconsider Sn = S(n) as S(m) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

            x in [: NAT , ( QC-symbols Sn):] by A72, QC_LANG1: 5;

            then

            consider x3,x4 be object such that

             A77: x3 in NAT & x4 in ( QC-symbols Sn) & x = [x3, x4] by ZFMISC_1:def 2;

            x = [x1, x4] by A71, A77, XTUPLE_0: 1;

            then x in [: {4}, ( QC-symbols Sn):] by A71, A77, ZFMISC_1:def 2;

            then x is bound_QC-variable of Sn & r is Element of ( CQC-WFF Sn) by A70, QC_TRANS: 7, QC_LANG1:def 4;

            then

            consider x2 be bound_QC-variable of Sn, r2 be Element of ( CQC-WFF Sn) such that

             A78: x2 = x & r2 = r;

            reconsider Al2 as Sn -expanding QC-alphabet by A2, QC_TRANS:def 1;

            

             A79: r = (Al2 -Cast r2) & x = (Al2 -Cast x2) by A78, QC_TRANS:def 3, QC_TRANS:def 4;

            ( All (x2,r2)) = (Al2 -Cast ( All (x2,r2))) by QC_TRANS:def 3

            .= ( All (x,r)) by A79, QC_TRANS: 8;

            hence thesis;

          end;

        end;

        then

         A80: for r,s be Element of ( CQC-WFF Al2), x be bound_QC-variable of Al2, k be Nat, l be CQC-variable_list of k, Al2, P be QC-pred_symbol of k, Al2 holds P[( VERUM Al2)] & P[(P ! l)] & ( P[r] implies P[( 'not' r)]) & ( P[r] & P[s] implies P[(r '&' s)]) & ( P[r] implies P[( All (x,r))]) by A44, A45, A59, A62;

        for p be Element of ( CQC-WFF Al2) holds P[p] from CQC_LANG:sch 1( A80);

        hence thesis;

      end;

      PSI is with_examples

      proof

        for x be bound_QC-variable of Al2, p be Element of ( CQC-WFF Al2) holds ex y be bound_QC-variable of Al2 st PSI |- (( 'not' ( Ex (x,p))) 'or' (p . (x,y)))

        proof

          let x be bound_QC-variable of Al2, p be Element of ( CQC-WFF Al2);

          ex n st (x is bound_QC-variable of S(n) & p is Element of ( CQC-WFF S(n)))

          proof

            consider m such that

             A81: p is Element of ( CQC-WFF S(m)) by A43;

            x in ( QC-variables Al2) & ( QC-variables Al2) c= [: NAT , ( QC-symbols Al2):] by QC_LANG1: 4;

            then x in [: NAT , ( QC-symbols Al2):] & Al2 = [: NAT , ( QC-symbols Al2):] by QC_LANG1: 5;

            then {x} c= ( union S) & {x} is finite by ZFMISC_1: 31;

            then

            consider a be set such that

             A82: a in S & {x} c= a by A39, COHSP_1: 6, COHSP_1: 13;

            consider n such that

             A83: a = S(n) by A82;

            x in ( bound_QC-variables Al2);

            then x in [: {4}, ( QC-symbols Al2):] by QC_LANG1:def 4;

            then

            consider x1,x2 be object such that

             A84: x1 in {4} & x2 in ( QC-symbols Al2) & x = [x1, x2] by ZFMISC_1:def 2;

            

             A85: x in S(n) by A82, A83, ZFMISC_1: 31;

            per cases ;

              suppose

               A86: n <= m;

              then

              reconsider Sm = S(m) as S(n) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

               S(n) c= S(m) by A86, Th6;

              then x in S(m) by A85;

              then x in [: NAT , ( QC-symbols S(m)):] by QC_LANG1: 5;

              then

              consider x3,x4 be object such that

               A87: x3 in NAT & x4 in ( QC-symbols S(m)) & x = [x3, x4] by ZFMISC_1:def 2;

              x = [x1, x4] by A84, A87, XTUPLE_0: 1;

              then x in [: {4}, ( QC-symbols Sm):] by A84, A87, ZFMISC_1:def 2;

              then x is bound_QC-variable of Sm by QC_LANG1:def 4;

              hence thesis by A81;

            end;

              suppose not n <= m;

              then

              reconsider Sn = S(n) as S(m) -expanding QC-alphabet by Th6, QC_TRANS:def 1;

              x in [: NAT , ( QC-symbols S(n)):] by A85, QC_LANG1: 5;

              then

              consider x3,x4 be object such that

               A88: x3 in NAT & x4 in ( QC-symbols S(n)) & x = [x3, x4] by ZFMISC_1:def 2;

              x = [x1, x4] by A84, A88, XTUPLE_0: 1;

              then x in [: {4}, ( QC-symbols Sn):] by A84, A88, ZFMISC_1:def 2;

              then x is bound_QC-variable of Sn & p is Element of ( CQC-WFF Sn) by A81, QC_TRANS: 7, QC_LANG1:def 4;

              hence thesis;

            end;

          end;

          then

          consider n such that

           A89: x is bound_QC-variable of S(n) & p is Element of ( CQC-WFF S(n));

          

           A90: ( FCEx S(n)) = S(+) by Th5;

          

           A91: PSI(+) = ( PSI(n) \/ ( Example_Formulae_of S(n))) by Def9;

          consider x2 be bound_QC-variable of S(n), p2 be Element of ( CQC-WFF S(n)) such that

           A92: x2 = x & p2 = p by A89;

          ( Example_Formula_of (p2,x2)) in ( Example_Formulae_of S(n));

          then

           A93: ( Example_Formula_of (p2,x2)) in PSI(+) by A91, XBOOLE_0:def 3;

           S(n) c= S(+) by Th6, NAT_1: 11;

          then

          reconsider Sn1 = S(+) as S(n) -expanding QC-alphabet by QC_TRANS:def 1;

          set y2 = ( Example_of (p2,x2));

          reconsider y2 as bound_QC-variable of Sn1 by Th5;

          reconsider Al2 as Sn1 -expanding QC-alphabet by A2, QC_TRANS:def 1;

          y2 is bound_QC-variable of Al2 by TARSKI:def 3, QC_TRANS: 4;

          then

          consider y be bound_QC-variable of Al2 such that

           A94: y = y2;

          

           A95: (Sn1 -Cast p2) = p & (Sn1 -Cast x2) = x by A92, QC_TRANS:def 3, QC_TRANS:def 4;

          then

           A96: (Al2 -Cast (Sn1 -Cast p2)) = p & (Al2 -Cast (Sn1 -Cast x2)) = x by QC_TRANS:def 3, QC_TRANS:def 4;

          

           A97: (Al2 -Cast ( Ex ((Sn1 -Cast x2),(Sn1 -Cast p2)))) = ( Ex (x,p)) by A96, Th7;

          reconsider p as Element of ( CQC-WFF Al2);

          reconsider x as bound_QC-variable of Al2;

          

           A98: ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2)) = (p . (x,y)) by A94, A95, QC_TRANS: 17;

          

           A99: ( Example_Formula_of (p2,x2)) = (Al2 -Cast (( 'not' ( Ex ((Sn1 -Cast x2),(Sn1 -Cast p2)))) 'or' ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2)))) by A90, QC_TRANS:def 3

          .= ((Al2 -Cast ( 'not' ( Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))))) 'or' (Al2 -Cast ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2)))) by Th7

          .= (( 'not' (Al2 -Cast ( Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))))) 'or' (Al2 -Cast ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2)))) by QC_TRANS: 8

          .= (( 'not' ( Ex (x,p))) 'or' (p . (x,y))) by A97, A98, QC_TRANS:def 3;

          set example = (( 'not' ( Ex (x,p))) 'or' (p . (x,y)));

          reconsider example as Element of ( CQC-WFF Al2);

          reconsider PSI as Consistent Subset of ( CQC-WFF Al2);

           PSI(+) in the set of all PSI(m);

          then PSI(+) c= PSI by ZFMISC_1: 74;

          hence thesis by A93, A99, GOEDELCP: 21;

        end;

        hence thesis by GOEDELCP:def 2;

      end;

      hence thesis by A1;

    end;

    theorem :: GOEDCPUC:11

    

     Th11: (PHI \/ {p}) is Consistent or (PHI \/ {( 'not' p)}) is Consistent

    proof

      assume not (PHI \/ {p}) is Consistent & not (PHI \/ {( 'not' p)}) is Consistent;

      then PHI |- ( 'not' p) & PHI |- p by HENMODEL: 9, HENMODEL: 10;

      hence contradiction by HENMODEL:def 2;

    end;

    theorem :: GOEDCPUC:12

    

     Th12: for PSI be Consistent Subset of ( CQC-WFF Al) holds ex THETA be Consistent Subset of ( CQC-WFF Al) st THETA is negation_faithful & PSI c= THETA

    proof

      let PSI be Consistent Subset of ( CQC-WFF Al);

      set U = { PHI : PSI c= PHI };

      

       A1: PSI in U;

      (for Z be set st Z c= U & Z is c=-linear holds ex Y be set st (Y in U & (for X be set st X in Z holds X c= Y)))

      proof

        let Z be set such that

         A2: Z c= U & Z is c=-linear;

        per cases ;

          suppose

           A3: Z is empty;

          PSI in U & for X be set st X in Z holds X c= PSI by A3;

          hence thesis;

        end;

          suppose

           A4: Z is non empty;

          set Y = ( union Z);

          

           A5: PSI c= Y

          proof

            let z be object such that

             A6: z in PSI;

            consider X be object such that

             A7: X in Z by A4, XBOOLE_0: 7;

            X in U by A2, A7;

            then ex R be Consistent Subset of ( CQC-WFF Al) st X = R & PSI c= R;

            hence z in Y by A6, A7, TARSKI:def 4;

          end;

          

           A8: Y is Consistent Subset of ( CQC-WFF Al)

          proof

            for X be set st X in Z holds X c= ( CQC-WFF Al)

            proof

              let X be set such that

               A9: X in Z;

              X in U by A2, A9;

              then ex R be Consistent Subset of ( CQC-WFF Al) st X = R & PSI c= R;

              hence X c= ( CQC-WFF Al);

            end;

            then

            reconsider Y as Subset of ( CQC-WFF Al) by ZFMISC_1: 76;

            Y is Consistent

            proof

              assume Y is Inconsistent;

              then

              consider X be Subset of ( CQC-WFF Al) such that

               A10: X c= Y & X is finite & X is Inconsistent by HENMODEL: 7;

              ex Rs be finite Subset of Z st for x be set st x in X holds ex R be set st R in Rs & x in R

              proof

                defpred R[ set] means ex Rs be finite Subset of Z st for x be set st x in $1 holds ex R be set st R in Rs & x in R;

                

                 A11: R[ {} ]

                proof

                  consider Rs be object such that

                   A12: Rs in Z by A4, XBOOLE_0: 7;

                  set Rss = {Rs};

                  reconsider Rss as finite Subset of Z by A12, ZFMISC_1: 31;

                  for x be set st x in {} holds ex R be set st R in Rss & x in R;

                  hence thesis;

                end;

                

                 A13: for x,B be set st x in X & B c= X & R[B] holds R[(B \/ {x})]

                proof

                  let x,B be set such that

                   A14: x in X & B c= X & R[B];

                  consider Rs be finite Subset of Z such that

                   A15: for b be set st b in B holds ex R be set st R in Rs & b in R by A14;

                  consider S be set such that

                   A16: (x in S & S in Z) by A10, A14, TARSKI:def 4;

                  set Rss = (Rs \/ {S});

                  Rs c= Z & {S} c= Z by A16, ZFMISC_1: 31;

                  then

                   A17: Rss c= Z by XBOOLE_1: 8;

                  for y be set st y in (B \/ {x}) holds ex R be set st R in Rss & y in R

                  proof

                    let y be set such that

                     A18: y in (B \/ {x});

                    per cases by A18, XBOOLE_0:def 3;

                      suppose y in {x};

                      then

                       A19: y = x by TARSKI:def 1;

                      S in {S} by TARSKI:def 1;

                      then S in Rss by XBOOLE_0:def 3;

                      hence thesis by A16, A19;

                    end;

                      suppose y in B;

                      then

                      consider R be set such that

                       A20: R in Rs & y in R by A15;

                      R in Rss by A20, XBOOLE_0:def 3;

                      hence thesis by A20;

                    end;

                  end;

                  hence thesis by A17;

                end;

                

                 A21: X is finite by A10;

                 R[X] from FINSET_1:sch 2( A21, A11, A13);

                hence thesis;

              end;

              then

              consider Rs be finite Subset of Z such that

               A22: for x be set st x in X holds ex R be set st R in Rs & x in R;

              defpred F[ set] means $1 is non empty implies ( union $1) in $1;

              

               A23: Rs is finite;

              

               A24: F[ {} ];

              

               A25: for x,B be set st x in Rs & B c= Rs & F[B] holds F[(B \/ {x})]

              proof

                let x,B be set such that

                 A26: x in Rs & B c= Rs & F[B];

                per cases ;

                  suppose

                   A27: B is empty;

                  

                   A28: ( union (B \/ {x})) = x by A27, ZFMISC_1: 25;

                  thus thesis by A27, A28, TARSKI:def 1;

                end;

                  suppose

                   A29: B is non empty;

                  per cases by A2, A26, A29, ORDINAL1:def 8, XBOOLE_0:def 9;

                    suppose

                     A30: x c= ( union B);

                    ( union (B \/ {x})) = (( union B) \/ ( union {x})) by ZFMISC_1: 78

                    .= (( union B) \/ x) by ZFMISC_1: 25

                    .= ( union B) by A30, XBOOLE_1: 12;

                    hence thesis by A26, A29, XBOOLE_0:def 3;

                  end;

                    suppose

                     A31: ( union B) c= x;

                    

                     A32: x in {x} by TARSKI:def 1;

                    ( union (B \/ {x})) = (( union B) \/ ( union {x})) by ZFMISC_1: 78

                    .= (( union B) \/ x) by ZFMISC_1: 25

                    .= x by A31, XBOOLE_1: 12;

                    hence thesis by A32, XBOOLE_0:def 3;

                  end;

                end;

              end;

              

               A33: F[Rs] from FINSET_1:sch 2( A23, A24, A25);

              X is non empty

              proof

                assume

                 A34: X is empty;

                X |- ( 'not' ( VERUM Al)) by A10, HENMODEL: 6;

                then (X \/ {( VERUM Al)}) is Inconsistent & (X \/ {( VERUM Al)}) = {( VERUM Al)} by A34, HENMODEL: 10;

                hence contradiction by HENMODEL: 13;

              end;

              then

              consider x be object such that

               A35: x in X by XBOOLE_0:def 1;

              ex R be set st R in Rs & x in R by A22, A35;

              then ( union Rs) in Z by A33;

              then ( union Rs) in U by A2;

              then

              consider uRs be Consistent Subset of ( CQC-WFF Al) such that

               A36: ( union Rs) = uRs & PSI c= uRs;

              for x be object st x in X holds x in uRs

              proof

                let x be object such that

                 A37: x in X;

                ex R be set st R in Rs & x in R by A22, A37;

                hence thesis by A36, TARSKI:def 4;

              end;

              then

               A38: X c= uRs;

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

               A39: ( rng f) c= X & |- (f ^ <*( 'not' ( VERUM Al))*>) by A10, HENMODEL:def 1, GOEDELCP: 24;

              ( rng f) c= uRs by A38, A39;

              hence contradiction by A39, HENMODEL:def 1, GOEDELCP: 24;

            end;

            hence thesis;

          end;

          Y in U & for X be set st X in Z holds X c= Y by A5, A8, ZFMISC_1: 74;

          hence thesis;

        end;

      end;

      then

      consider THETA be set such that

       A40: (THETA in U & (for Z be set st Z in U & Z <> THETA holds not THETA c= Z)) by A1, ORDERS_1: 65;

      

       A41: ex PHI st PHI = THETA & PSI c= PHI by A40;

      then

      reconsider THETA as Consistent Subset of ( CQC-WFF Al);

      

       A42: for p holds (p in THETA or ( 'not' p) in THETA)

      proof

        let p;

        per cases by Th11;

          suppose

           A43: (THETA \/ {p}) is Consistent;

          assume

           A44: not p in THETA;

          p in {p} by TARSKI:def 1;

          then

           A45: p in (THETA \/ {p}) & not p in THETA by XBOOLE_0:def 3, A44;

          PSI c= (THETA \/ {p}) by A41, XBOOLE_1: 10;

          then (THETA \/ {p}) in U by A43;

          hence thesis by A40, A45, XBOOLE_1: 10;

        end;

          suppose

           A46: (THETA \/ {( 'not' p)}) is Consistent;

          ( 'not' p) in THETA

          proof

            assume

             A47: not (( 'not' p) in THETA);

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

            then

             A48: ( 'not' p) in (THETA \/ {( 'not' p)}) & not ( 'not' p) in THETA by XBOOLE_0:def 3, A47;

            PSI c= (THETA \/ {( 'not' p)}) by A41, XBOOLE_1: 10;

            then (THETA \/ {( 'not' p)}) in U by A46;

            hence thesis by A40, A48, XBOOLE_1: 10;

          end;

          hence thesis;

        end;

      end;

      for p holds THETA |- p or THETA |- ( 'not' p)

      proof

        let p;

        p in THETA or ( 'not' p) in THETA by A42;

        hence thesis by GOEDELCP: 21;

      end;

      then THETA is negation_faithful by GOEDELCP:def 1;

      hence thesis by A41;

    end;

    theorem :: GOEDCPUC:13

    

     Th13: for THETA be Consistent Subset of ( CQC-WFF Al) st PHI c= THETA & PHI is with_examples holds THETA is with_examples

    proof

      let THETA be Consistent Subset of ( CQC-WFF Al) such that

       A1: PHI c= THETA & PHI is with_examples;

      now

        let x be bound_QC-variable of Al, p be Element of ( CQC-WFF Al);

        consider y be bound_QC-variable of Al such that

         A2: PHI |- (( 'not' ( Ex (x,p))) 'or' (p . (x,y))) by A1, GOEDELCP:def 2;

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

         A3: ( rng f) c= PHI & |- (f ^ <*(( 'not' ( Ex (x,p))) 'or' (p . (x,y)))*>) by A2, HENMODEL:def 1;

        take y;

        thus THETA |- (( 'not' ( Ex (x,p))) 'or' (p . (x,y))) by A1, A3, HENMODEL:def 1, XBOOLE_1: 1;

      end;

      hence thesis by GOEDELCP:def 2;

    end;

    registration

      let Al;

      cluster Consistent -> satisfiable for Subset of ( CQC-WFF Al);

      coherence

      proof

        let PHI be Subset of ( CQC-WFF Al);

        assume

         A1: PHI is Consistent;

        then

        consider Al2 be Al -expanding QC-alphabet, PSI be Consistent Subset of ( CQC-WFF Al2) such that

         A2: PHI c= PSI & PSI is with_examples by Th10;

        consider THETA be Consistent Subset of ( CQC-WFF Al2) such that

         A3: THETA is negation_faithful & PSI c= THETA by Th12;

        set JH = the Henkin_interpretation of THETA;

        now

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

          

           A4: THETA is with_examples by Th13, A3, A2;

          assume p in THETA;

          then THETA |- p by GOEDELCP: 21;

          hence (JH,( valH Al2)) |= p by GOEDELCP: 17, A3, A4;

        end;

        then (JH,( valH Al2)) |= THETA by CALCUL_1:def 11;

        then ex A, J, v st (J,v) |= PHI by A1, A2, A3, QC_TRANS: 10, XBOOLE_1: 1;

        hence thesis;

      end;

    end

    theorem :: GOEDCPUC:14

    PSI |= p implies PSI |- p

    proof

      set CHI = (PSI \/ {( 'not' p)});

      assume

       A1: PSI |= p;

      assume not PSI |- p;

      then CHI is Consistent by HENMODEL: 9;

      then ex A, J, v st (J,v) |= CHI by Def1;

      hence contradiction by GOEDELCP: 37, A1;

    end;