pl_axiom.miz



    begin

    theorem :: PL_AXIOM:1

    

     rnginc: for f,g be Function holds (( dom f) c= ( dom g) & for x be set st x in ( dom f) holds (f . x) = (g . x)) implies ( rng f) c= ( rng g)

    proof

      let f,g be Function;

      assume that

       A2: ( dom f) c= ( dom g) and

       A2a: for x be set st x in ( dom f) holds (f . x) = (g . x);

      let x be object;

      assume x in ( rng f);

      then

      consider y be object such that

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

      x = (g . y) by A2a, A1;

      hence x in ( rng g) by FUNCT_1: 3, A1, A2;

    end;

    theorem :: PL_AXIOM:2

    

     th1: for p,q be boolean object holds ((p '&' q) => p) = TRUE

    proof

      let p,q be boolean object;

      p = TRUE or p = FALSE by XBOOLEAN:def 3;

      hence ((p '&' q) => p) = TRUE ;

    end;

    theorem :: PL_AXIOM:3

    

     th2: for p be boolean object holds (( 'not' ( 'not' p)) <=> p) = TRUE

    proof

      let p be boolean object;

      p = TRUE or p = FALSE by XBOOLEAN:def 3;

      hence (( 'not' ( 'not' p)) <=> p) = TRUE ;

    end;

    theorem :: PL_AXIOM:4

    

     th3: for p,q be boolean object holds (( 'not' (p '&' q)) <=> (( 'not' p) 'or' ( 'not' q))) = TRUE

    proof

      let p,q be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      q = TRUE or q = FALSE by XBOOLEAN:def 3;

      hence (( 'not' (p '&' q)) <=> (( 'not' p) 'or' ( 'not' q))) = TRUE by A1;

    end;

    theorem :: PL_AXIOM:5

    

     th3a: for p,q be boolean object holds (( 'not' (p 'or' q)) <=> (( 'not' p) '&' ( 'not' q))) = TRUE

    proof

      let p,q be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      q = TRUE or q = FALSE by XBOOLEAN:def 3;

      hence (( 'not' (p 'or' q)) <=> (( 'not' p) '&' ( 'not' q))) = TRUE by A1;

    end;

    theorem :: PL_AXIOM:6

    

     th4: for p,q be boolean object holds ((p => q) => (( 'not' q) => ( 'not' p))) = TRUE

    proof

      let p,q be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      q = TRUE or q = FALSE by XBOOLEAN:def 3;

      hence ((p => q) => (( 'not' q) => ( 'not' p))) = TRUE by A1;

    end;

    theorem :: PL_AXIOM:7

    

     th5: for p,q,r be boolean object holds ((p => q) => ((p => r) => (p => (q '&' r)))) = TRUE

    proof

      let p,q,r be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      

       A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;

      r = TRUE or r = FALSE by XBOOLEAN:def 3;

      hence thesis by A1, A2;

    end;

    theorem :: PL_AXIOM:8

    

     th5a: for p,q,r be boolean object holds ((p => r) => ((q => r) => ((p 'or' q) => r))) = TRUE

    proof

      let p,q,r be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      

       A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;

      r = TRUE or r = FALSE by XBOOLEAN:def 3;

      hence thesis by A1, A2;

    end;

    theorem :: PL_AXIOM:9

    

     th6: for p,q be boolean object holds ((p '&' q) <=> (q '&' p)) = TRUE

    proof

      let p,q be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      q = TRUE or q = FALSE by XBOOLEAN:def 3;

      hence ((p '&' q) <=> (q '&' p)) = TRUE by A1;

    end;

    theorem :: PL_AXIOM:10

    

     th6a: for p,q be boolean object holds ((p 'or' q) <=> (q 'or' p)) = TRUE

    proof

      let p,q be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      q = TRUE or q = FALSE by XBOOLEAN:def 3;

      hence ((p 'or' q) <=> (q 'or' p)) = TRUE by A1;

    end;

    theorem :: PL_AXIOM:11

    

     th7: for p,q,r be boolean object holds (((p '&' q) '&' r) <=> (p '&' (q '&' r))) = TRUE

    proof

      let p,q,r be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      

       A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;

      r = TRUE or r = FALSE by XBOOLEAN:def 3;

      hence thesis by A1, A2;

    end;

    theorem :: PL_AXIOM:12

    

     th7a: for p,q,r be boolean object holds (((p 'or' q) 'or' r) <=> (p 'or' (q 'or' r))) = TRUE

    proof

      let p,q,r be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      

       A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;

      r = TRUE or r = FALSE by XBOOLEAN:def 3;

      hence thesis by A1, A2;

    end;

    theorem :: PL_AXIOM:13

    

     Th17a: for p,q be boolean object holds ((( 'not' q) => ( 'not' p)) => ((( 'not' q) => p) => q)) = TRUE

    proof

      let p,q be boolean object;

      

       A1: p = FALSE or p = TRUE by XBOOLEAN:def 3;

      q = FALSE or q = TRUE by XBOOLEAN:def 3;

      hence thesis by A1;

    end;

    theorem :: PL_AXIOM:14

    

     th8: for p,q,r be boolean object holds ((p '&' (q 'or' r)) <=> ((p '&' q) 'or' (p '&' r))) = TRUE

    proof

      let p,q,r be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      

       A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;

      r = TRUE or r = FALSE by XBOOLEAN:def 3;

      hence thesis by A1, A2;

    end;

    theorem :: PL_AXIOM:15

    

     th8a: for p,q,r be boolean object holds ((p 'or' (q '&' r)) <=> ((p 'or' q) '&' (p 'or' r))) = TRUE

    proof

      let p,q,r be boolean object;

      

       A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;

      

       A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;

      r = TRUE or r = FALSE by XBOOLEAN:def 3;

      hence thesis by A1, A2;

    end;

    theorem :: PL_AXIOM:16

    

     uniolinf: for X be finite set, Y be set holds Y is c=-linear & X c= ( union Y) & Y <> {} implies ex Z be set st X c= Z & Z in Y

    proof

      let X be finite set, Y be set;

      assume

       A0: Y is c=-linear & X c= ( union Y) & Y <> {} ;

      deffunc G( object) = { y where y be Element of Y : $1 in y };

      deffunc F( object) = the Element of G($1);

      

       A18: for x be object holds x in X implies G(x) is non empty

      proof

        let x be object;

        assume x in X;

        then

        consider y be set such that

         A11: x in y & y in Y by TARSKI:def 4, A0;

        reconsider y as Element of Y by A11;

        y in G(x) by A11;

        hence G(x) is non empty;

      end;

      per cases ;

        suppose

         S1: X is empty;

        consider Z be object such that

         A15: Z in Y by A0, XBOOLE_0:def 1;

        consider Z1 be set such that

         A16: Z1 in Y & not ex x be object st x in Y & x in Z1 by TARSKI: 3, A15;

        X c= Z1 by S1;

        hence thesis by A16;

      end;

        suppose

         S2: not X is empty;

        set Y1 = { F(x) where x be Element of X : x in X };

        

         A20: X is finite;

        

         A2: Y1 is finite from FRAENKEL:sch 21( A20);

        

         A19: Y1 c= Y

        proof

          let x be object;

          assume x in Y1;

          then

          consider x1 be Element of X such that

           A13: x = the Element of G(x1) & x1 in X;

           G(x1) is non empty by A18, A13;

          then x in G(x1) by A13;

          then

          consider x2 be Element of Y such that

           A14: x2 = x & x1 in x2;

          thus x in Y by A0, A14;

        end;

        Y1 <> {}

        proof

          consider x be object such that

           A15: x in X by XBOOLE_0:def 1, S2;

          consider x1 be set such that

           A16: x1 in X & not ex x be object st x in X & x in x1 by TARSKI: 3, A15;

          reconsider x1 as Element of X by A16;

           the Element of G(x1) in Y1 by A16;

          hence thesis;

        end;

        then

        consider Z be set such that

         A1: Z in Y1 & for y be set st y in Y1 holds y c= Z by FINSET_1: 12, A0, A2, A19;

        

         A4: X c= Z

        proof

          let x be object;

          assume

           A8: x in X;

          then the Element of G(x) in Y1;

          then

           A9: the Element of G(x) c= Z by A1;

           G(x) is non empty by A8, A18;

          then the Element of G(x) in G(x);

          then

          consider y3 be Element of Y such that

           A10: y3 = the Element of G(x) & x in y3;

          thus x in Z by A10, A9;

        end;

        consider x be Element of X such that

         A6: Z = the Element of G(x) & x in X by A1;

         G(x) is non empty by A6, A18;

        then Z in G(x) by A6;

        then

        consider y be Element of Y such that

         U1: y = Z & x in y;

        thus ex Z be set st X c= Z & Z in Y by A4, A0, U1;

      end;

    end;

    begin

    definition

      let D be set;

      :: PL_AXIOM:def1

      attr D is with_propositional_variables means

      : Def4: for n be Element of NAT holds <*(3 + n)*> in D;

    end

    definition

      let D be set;

      :: PL_AXIOM:def2

      attr D is PL-closed means

      : Def5: D c= ( NAT * ) & D is with_FALSUM with_implication with_propositional_variables;

    end

    

     Lm1: for D be set st D is PL-closed holds D is non empty

    proof

      let D be set;

      assume D is PL-closed;

      then D is with_FALSUM;

      hence thesis;

    end;

    registration

      cluster PL-closed -> with_FALSUM with_implication with_propositional_variables non empty for set;

      coherence by Lm1;

      cluster with_FALSUM with_implication with_propositional_variables -> PL-closed for Subset of ( NAT * );

      coherence ;

    end

    definition

      :: PL_AXIOM:def3

      func PL-WFF -> set means

      : Def6: it is PL-closed & for D be set st D is PL-closed holds it c= D;

      existence

      proof

        

         A1: <* 0 qua Element of NAT *> in ( NAT * ) by FINSEQ_1:def 11;

        defpred P[ set] means for D be set st D is PL-closed holds $1 in D;

        consider D0 be set such that

         A2: for x be set holds x in D0 iff x in ( NAT * ) & P[x] from XFAMILY:sch 1;

        

         A3: for D be set st D is PL-closed holds <* 0 *> in D by INTPRO_1:def 1;

        then

        reconsider D0 as non empty set by A2, A1;

        take D0;

        

         A4: D0 c= ( NAT * ) by A2;

        for p,q be FinSequence st p in D0 & q in D0 holds (( <*1*> ^ p) ^ q) in D0

        proof

          let p,q be FinSequence such that

           A5: p in D0 and

           A6: q in D0;

          

           A7: q in ( NAT * ) by A2, A6;

          

           A8: for D be set st D is PL-closed holds (( <*1*> ^ p) ^ q) in D

          proof

            let D be set;

            assume

             A9: D is PL-closed;

            then

             A10: q in D by A2, A6;

            p in D by A2, A5, A9;

            hence thesis by A9, A10, HILBERT1:def 2;

          end;

          p in ( NAT * ) by A2, A5;

          then

          reconsider p9 = p, q9 = q as FinSequence of NAT by A7, FINSEQ_1:def 11;

          (( <*1*> ^ p9) ^ q9) in ( NAT * ) by FINSEQ_1:def 11;

          hence thesis by A2, A8;

        end;

        then

         A11: D0 is with_implication by HILBERT1:def 2;

        for n be Element of NAT holds <*(3 + n)*> in D0

        proof

          let n be Element of NAT ;

          set p = (3 + n);

          reconsider h = <*p*> as FinSequence of NAT ;

          

           A19: h in ( NAT * ) by FINSEQ_1:def 11;

          for D be set st D is PL-closed holds <*p*> in D by Def4;

          hence thesis by A2, A19;

        end;

        then

         A20: D0 is with_propositional_variables;

        D0 is with_FALSUM by A2, A1, A3;

        hence D0 is PL-closed by A4, A20, A11;

        let D be set such that

         A21: D is PL-closed;

        let x be object;

        assume x in D0;

        hence thesis by A2, A21;

      end;

      uniqueness

      proof

        let D1,D2 be set such that

         A22: D1 is PL-closed and

         A23: for D be set st D is PL-closed holds D1 c= D and

         A24: D2 is PL-closed and

         A25: for D be set st D is PL-closed holds D2 c= D;

        

         A26: D2 c= D1 by A22, A25;

        D1 c= D2 by A23, A24;

        hence thesis by A26, XBOOLE_0:def 10;

      end;

    end

    registration

      cluster PL-WFF -> PL-closed;

      coherence by Def6;

    end

    registration

      cluster PL-closed non empty for set;

      existence

      proof

        take PL-WFF ;

        thus thesis;

      end;

    end

    registration

      cluster PL-WFF -> functional;

      coherence

      proof

         PL-WFF c= ( NAT * ) by Def5;

        hence thesis;

      end;

    end

    registration

      cluster -> FinSequence-like for Element of PL-WFF ;

      coherence

      proof

        let p be Element of PL-WFF ;

         PL-WFF c= ( NAT * ) by Def5;

        hence thesis;

      end;

    end

    definition

      :: PL_AXIOM:def4

      func FaLSUM -> Element of PL-WFF equals <* 0 *>;

      correctness by INTPRO_1:def 1;

      let p,q be Element of PL-WFF ;

      :: PL_AXIOM:def5

      func p => q -> Element of PL-WFF equals (( <*1*> ^ p) ^ q);

      coherence by HILBERT1:def 2;

    end

    definition

      let n be Element of NAT ;

      :: PL_AXIOM:def6

      func Prop n -> Element of PL-WFF equals <*(3 + n)*>;

      coherence by Def4;

    end

    definition

      :: PL_AXIOM:def7

      func props -> Subset of PL-WFF means

      : defprops: for x be set holds x in it iff ex n be Element of NAT st x = ( Prop n);

      existence

      proof

        defpred P1[ object] means ex n be Element of NAT st $1 = ( Prop n);

        consider X be set such that

         A1: for x be object holds (x in X iff x in PL-WFF & P1[x]) from XBOOLE_0:sch 1;

        X c= PL-WFF by A1;

        then

        reconsider X as Subset of PL-WFF ;

        take X;

        thus for x be set holds (x in X iff ex n be Element of NAT st x = ( Prop n)) by A1;

      end;

      uniqueness

      proof

        let A,B be Subset of PL-WFF such that

         A2: for x be set holds x in A iff ex n be Element of NAT st x = ( Prop n) and

         A3: for x be set holds x in B iff ex n be Element of NAT st x = ( Prop n);

        

         A4: B c= A

        proof

          let x be object;

          assume x in B;

          then

          consider n be Element of NAT such that

           A5: x = ( Prop n) by A3;

          thus x in A by A2, A5;

        end;

        A c= B

        proof

          let x be object;

          assume x in A;

          then

          consider n be Element of NAT such that

           A6: x = ( Prop n) by A2;

          thus x in B by A3, A6;

        end;

        hence A = B by A4, XBOOLE_0:def 10;

      end;

    end

    reserve p,q,r,s,A,B for Element of PL-WFF ,

F,G,H for Subset of PL-WFF ,

k,n for Element of NAT ,

f,f1,f2 for FinSequence of PL-WFF ;

    definition

      let D be Subset of PL-WFF ;

      :: original: with_implication

      redefine

      :: PL_AXIOM:def8

      attr D is with_implication means for p, q st p in D & q in D holds (p => q) in D;

      compatibility

      proof

        thus D is with_implication implies for p, q st p in D & q in D holds (p => q) in D by HILBERT1:def 2;

        assume

         A1: for p, q st p in D & q in D holds (p => q) in D;

        let p,q be FinSequence;

        assume

         A2: p in D & q in D;

        then

        reconsider p9 = p, q9 = q as Element of PL-WFF ;

        (p9 => q9) in D by A1, A2;

        hence thesis;

      end;

    end

    scheme :: PL_AXIOM:sch1

    PLInd { P[ set] } :

for r holds P[r]

      provided

       A1: P[ FaLSUM ]

       and

       A2: for n holds P[( Prop n)]

       and

       A3: for r, s st P[r] & P[s] holds P[(r => s)];

      set X = { p where p be Element of PL-WFF : P[p] };

      X c= PL-WFF

      proof

        let x be object;

        assume x in X;

        then ex p be Element of PL-WFF st x = p & P[p];

        hence thesis;

      end;

      then

      reconsider X as Subset of PL-WFF ;

      let r;

      

       A4: X is with_propositional_variables

      proof

        let n;

        P[( Prop n)] by A2;

        hence thesis;

      end;

      

       A5: X is with_implication

      proof

        let p, q;

        assume p in X;

        then

         A6: ex x be Element of PL-WFF st p = x & P[x];

        assume q in X;

        then ex x be Element of PL-WFF st q = x & P[x];

        then P[(p => q)] by A3, A6;

        hence thesis;

      end;

       PL-WFF c= ( NAT * ) by Def5;

      then

       A8: X c= ( NAT * );

      X is with_FALSUM by A1;

      then PL-WFF c= X by A8, A5, A4, Def6;

      then r in X;

      then ex p be Element of PL-WFF st r = p & P[p];

      hence thesis;

    end;

    theorem :: PL_AXIOM:17

    

     plhp: PL-WFF c= HP-WFF

    proof

      let x be object;

      assume

       A0: x in PL-WFF ;

      defpred P[ Element of PL-WFF ] means $1 in HP-WFF ;

       VERUM = FaLSUM ;

      then

       A1: P[ FaLSUM ];

      

       A2: for n holds P[( Prop n)]

      proof

        let n;

        ( Prop n) = ( prop n);

        hence thesis;

      end;

      

       A3: for r, s st P[r] & P[s] holds P[(r => s)]

      proof

        let r, s;

        assume P[r] & P[s];

        then

        reconsider r1 = r, s1 = s as Element of HP-WFF ;

        (r1 => s1) in HP-WFF ;

        hence P[(r => s)];

      end;

      

       A4: for A holds P[A] from PLInd( A1, A2, A3);

      reconsider x1 = x as Element of PL-WFF by A0;

      x1 in HP-WFF by A4;

      hence x in HP-WFF ;

    end;

    definition

      let p;

      :: PL_AXIOM:def9

      func 'not' p -> Element of PL-WFF equals (p => FaLSUM );

      correctness ;

    end

    definition

      :: PL_AXIOM:def10

      func VeRUM -> Element of PL-WFF equals ( 'not' FaLSUM );

      correctness ;

    end

    definition

      let p, q;

      :: PL_AXIOM:def11

      func p '&' q -> Element of PL-WFF equals ( 'not' (p => ( 'not' q)));

      coherence ;

      :: PL_AXIOM:def12

      func p 'or' q -> Element of PL-WFF equals (( 'not' p) => q);

      coherence ;

    end

    definition

      let p, q;

      :: PL_AXIOM:def13

      func p <=> q -> Element of PL-WFF equals ((p => q) '&' (q => p));

      correctness ;

    end

    begin

    definition

      mode PLModel is Subset of props ;

    end

    reserve M for PLModel;

    definition

      let M be PLModel;

      :: PL_AXIOM:def14

      func SAT M -> Function of PL-WFF , BOOLEAN means

      : Def11: (it . FaLSUM ) = 0 & (for k holds (it . ( Prop k)) = 1 iff ( Prop k) in M) & for p, q holds (it . (p => q)) = ((it . p) => (it . q));

      existence

      proof

        defpred P1[ Element of NAT , Element of BOOLEAN ] means $2 = 1 iff ( Prop $1) in M;

        

         A16: for x be Element of NAT holds ex y be Element of BOOLEAN st P1[x, y]

        proof

          let x be Element of NAT ;

          defpred P2[ Element of BOOLEAN ] means $1 = 1 iff ( Prop x) in M;

          per cases ;

            suppose ( prop x) in M;

            then P2[ TRUE ];

            hence ex y be Element of BOOLEAN st P1[x, y];

          end;

            suppose not ( prop x) in M;

            then P2[ FALSE ];

            hence ex y be Element of BOOLEAN st P1[x, y];

          end;

        end;

        consider f1 be sequence of BOOLEAN such that

         A19: for k holds P1[k, (f1 . k)] from FUNCT_2:sch 3( A16);

        deffunc P( Element of NAT ) = (f1 . $1);

        defpred C[ Element of HP-WFF , Element of HP-WFF , set, set, set] means ex s5 be Element of BOOLEAN st $5 = FALSE ;

        defpred I[ Element of HP-WFF , Element of HP-WFF , set, set, set] means ($3 is Element of BOOLEAN & $4 is Element of BOOLEAN implies ex s3,s4,s5 be Element of BOOLEAN st s3 = $3 & s4 = $4 & s5 = $5 & s5 = (s3 => s4)) & ( not ($3 is Element of BOOLEAN & $4 is Element of BOOLEAN ) implies $5 = FALSE );

        

         A1: for p,q be Element of HP-WFF holds for a,b be set holds ex c be set st C[p, q, a, b, c];

        

         A2: for p,q be Element of HP-WFF holds for a,b be set holds ex d be set st I[p, q, a, b, d]

        proof

          let p,q be Element of HP-WFF , a,b be set;

          per cases ;

            suppose a is Element of BOOLEAN & b is Element of BOOLEAN ;

            then

            reconsider a1 = a, b1 = b as Element of BOOLEAN ;

            reconsider ab = (a1 => b1) as Element of BOOLEAN by MARGREL1:def 12;

            ab = (a1 => b1);

            hence thesis;

          end;

            suppose not (a is Element of BOOLEAN & b is Element of BOOLEAN );

            hence thesis;

          end;

        end;

        

         A3: for p,q be Element of HP-WFF holds for a,b,c,d be set st C[p, q, a, b, c] & C[p, q, a, b, d] holds c = d;

        

         A4: for p,q be Element of HP-WFF holds for a,b,c,d be set st I[p, q, a, b, c] & I[p, q, a, b, d] holds c = d;

        consider sat be ManySortedSet of HP-WFF such that

         A34: (sat . VERUM ) = 0 & (for n holds (sat . ( prop n)) = P(n)) & for p,q be Element of HP-WFF holds C[p, q, (sat . p), (sat . q), (sat . (p '&' q))] & I[p, q, (sat . p), (sat . q), (sat . (p => q))] from HILBERT2:sch 3( A1, A2, A3, A4);

        

         A35: for x be object st x in HP-WFF holds (sat . x) in BOOLEAN

        proof

          let x be object;

          assume x in HP-WFF ;

          then

          reconsider x1 = x as Element of HP-WFF ;

           A42:

          now

            let n;

            (sat . ( prop n)) = (f1 . n) by A34;

            hence (sat . ( prop n)) in BOOLEAN ;

          end;

          per cases by HILBERT2: 9;

            suppose x1 = VERUM ;

            hence (sat . x) in BOOLEAN by A34;

          end;

            suppose x1 is simple;

            then ex n be Element of NAT st x1 = ( prop n) by HILBERT2:def 8;

            hence (sat . x) in BOOLEAN by A42;

          end;

            suppose x1 is conjunctive;

            then

            consider A,B be Element of HP-WFF such that

             E2: x1 = (A '&' B) by HILBERT2:def 6;

            consider s5 be Element of BOOLEAN such that

             E3: (sat . (A '&' B)) = FALSE by A34;

            thus (sat . x) in BOOLEAN by E3, E2;

          end;

            suppose x1 is conditional;

            then

            consider A,B be Element of HP-WFF such that

             E1: x1 = (A => B) by HILBERT2:def 7;

            

             A37: I[A, B, (sat . A), (sat . B), (sat . (A => B))] by A34;

            thus (sat . x) in BOOLEAN by A37, E1;

          end;

        end;

        ( dom sat) = HP-WFF by PARTFUN1:def 2;

        then

        reconsider sat as Function of HP-WFF , BOOLEAN by A35, FUNCT_2: 3;

        set satc = (sat | PL-WFF );

        reconsider satc as Function of PL-WFF , BOOLEAN by FUNCT_2: 32, plhp;

        

         B1: (satc . FaLSUM ) = 0 by A34, FUNCT_1: 49;

        

         B2: for k holds (satc . ( Prop k)) = 1 iff ( Prop k) in M

        proof

          let k;

          hereby

            assume (satc . ( Prop k)) = 1;

            then

             D2: (sat . ( Prop k)) = 1 by FUNCT_1: 49;

            (sat . ( prop k)) = (f1 . k) by A34;

            hence ( Prop k) in M by A19, D2;

          end;

          assume ( Prop k) in M;

          then

           D1: (f1 . k) = 1 by A19;

          (sat . ( prop k)) = (f1 . k) by A34;

          hence (satc . ( Prop k)) = 1 by D1, FUNCT_1: 49;

        end;

        for p, q holds (satc . (p => q)) = ((satc . p) => (satc . q))

        proof

          let p, q;

          reconsider p1 = p, q1 = q as Element of HP-WFF by plhp;

          consider s3,s4,s5 be Element of BOOLEAN such that

           D4: s3 = (sat . p1) & s4 = (sat . q1) & s5 = (sat . (p1 => q1)) & s5 = (s3 => s4) by A34;

          

          thus (satc . (p => q)) = (sat . (p => q)) by FUNCT_1: 49

          .= ((satc . p) => (sat . q)) by FUNCT_1: 49, D4

          .= ((satc . p) => (satc . q)) by FUNCT_1: 49;

        end;

        hence thesis by B1, B2;

      end;

      uniqueness

      proof

        let v1,v2 be Function of PL-WFF , BOOLEAN ;

        assume

         A65: (v1 . FaLSUM ) = 0 & (for k holds (v1 . ( Prop k)) = 1 iff ( Prop k) in M) & for p, q holds (v1 . (p => q)) = ((v1 . p) => (v1 . q));

        assume

         A66: (v2 . FaLSUM ) = 0 & (for k holds (v2 . ( Prop k)) = 1 iff ( Prop k) in M) & for p, q holds (v2 . (p => q)) = ((v2 . p) => (v2 . q));

        defpred P1[ Element of PL-WFF ] means (v1 . $1) = (v2 . $1);

        

         A67: P1[( Prop n)]

        proof

          per cases ;

            suppose

             A68: ( Prop n) in M;

            

            hence (v1 . ( Prop n)) = 1 by A65

            .= (v2 . ( Prop n)) by A66, A68;

          end;

            suppose

             A69: not ( Prop n) in M;

            then (v1 . ( Prop n)) = 0 by XBOOLEAN:def 3, A65;

            hence (v1 . ( Prop n)) = (v2 . ( Prop n)) by XBOOLEAN:def 3, A66, A69;

          end;

        end;

        

         A70: for p, q st P1[p] & P1[q] holds P1[(p => q)]

        proof

          let p, q;

          assume that

           A71: P1[p] and

           A72: P1[q];

          

          thus (v1 . (p => q)) = ((v1 . p) => (v1 . q)) by A65

          .= (v2 . (p => q)) by A66, A72, A71;

        end;

        

         A83: P1[ FaLSUM ] by A66, A65;

        for A holds P1[A] from PLInd( A83, A67, A70);

        then

         A85: for x be Element of PL-WFF st x in ( dom v1) holds (v1 . x) = (v2 . x);

        ( dom v1) = PL-WFF by FUNCT_2:def 1

        .= ( dom v2) by FUNCT_2:def 1;

        hence thesis by A85, PARTFUN1: 5;

      end;

    end

    theorem :: PL_AXIOM:18

    (( SAT M) . (A => B)) = 1 iff (( SAT M) . A) = 0 or (( SAT M) . B) = 1

    proof

      

       A3: (( SAT M) . B) = TRUE or (( SAT M) . B) = FALSE by XBOOLEAN:def 3;

      hereby

        assume (( SAT M) . (A => B)) = 1;

        then ((( SAT M) . A) => (( SAT M) . B)) = 1 by Def11;

        hence (( SAT M) . A) = 0 or (( SAT M) . B) = 1 by A3;

      end;

      assume

       A4: (( SAT M) . A) = 0 or (( SAT M) . B) = 1;

      

      thus (( SAT M) . (A => B)) = ((( SAT M) . A) => (( SAT M) . B)) by Def11

      .= 1 by A4;

    end;

    theorem :: PL_AXIOM:19

    

     semnot2: (( SAT M) . ( 'not' p)) = ( 'not' (( SAT M) . p))

    proof

      

      thus (( SAT M) . ( 'not' p)) = ((( SAT M) . p) => (( SAT M) . FaLSUM )) by Def11

      .= ((( SAT M) . p) => FALSE ) by Def11

      .= ( 'not' (( SAT M) . p));

    end;

    theorem :: PL_AXIOM:20

    

     semnot: (( SAT M) . ( 'not' A)) = 1 iff (( SAT M) . A) = 0

    proof

      hereby

        assume (( SAT M) . ( 'not' A)) = 1;

        then ( 'not' (( SAT M) . A)) = 1 by semnot2;

        hence (( SAT M) . A) = 0 ;

      end;

      assume

       A2: (( SAT M) . A) = 0 ;

      

      thus (( SAT M) . ( 'not' A)) = ( 'not' (( SAT M) . A)) by semnot2

      .= 1 by A2;

    end;

    theorem :: PL_AXIOM:21

    

     semcon2: (( SAT M) . (A '&' B)) = ((( SAT M) . A) '&' (( SAT M) . B))

    proof

      

      thus (( SAT M) . (A '&' B)) = ( 'not' (( SAT M) . (A => ( 'not' B)))) by semnot2

      .= ( 'not' ((( SAT M) . A) => (( SAT M) . ( 'not' B)))) by Def11

      .= ( 'not' ((( SAT M) . A) => ( 'not' (( SAT M) . B)))) by semnot2

      .= ((( SAT M) . A) '&' (( SAT M) . B));

    end;

    theorem :: PL_AXIOM:22

    (( SAT M) . (A '&' B)) = 1 iff (( SAT M) . A) = 1 & (( SAT M) . B) = 1

    proof

      hereby

        assume (( SAT M) . (A '&' B)) = 1;

        then ((( SAT M) . A) '&' (( SAT M) . B)) = 1 by semcon2;

        hence (( SAT M) . A) = 1 & (( SAT M) . B) = 1 by XBOOLEAN: 101;

      end;

      assume

       A3: (( SAT M) . A) = 1 & (( SAT M) . B) = 1;

      

      thus (( SAT M) . (A '&' B)) = ((( SAT M) . A) '&' (( SAT M) . B)) by semcon2

      .= 1 by A3;

    end;

    theorem :: PL_AXIOM:23

    

     semdis2: (( SAT M) . (A 'or' B)) = ((( SAT M) . A) 'or' (( SAT M) . B))

    proof

      

      thus (( SAT M) . (A 'or' B)) = ((( SAT M) . ( 'not' A)) => (( SAT M) . B)) by Def11

      .= ((( SAT M) . A) 'or' (( SAT M) . B)) by semnot2;

    end;

    theorem :: PL_AXIOM:24

    (( SAT M) . (A 'or' B)) = 1 iff (( SAT M) . A) = 1 or (( SAT M) . B) = 1

    proof

      

       A2: (( SAT M) . B) = TRUE or (( SAT M) . B) = FALSE by XBOOLEAN:def 3;

      hereby

        assume (( SAT M) . (A 'or' B)) = 1;

        then ((( SAT M) . A) 'or' (( SAT M) . B)) = 1 by semdis2;

        hence (( SAT M) . A) = 1 or (( SAT M) . B) = 1 by A2;

      end;

      assume

       A3: (( SAT M) . A) = 1 or (( SAT M) . B) = 1;

      

      thus (( SAT M) . (A 'or' B)) = ((( SAT M) . A) 'or' (( SAT M) . B)) by semdis2

      .= 1 by A3;

    end;

    theorem :: PL_AXIOM:25

    

     semequ2: (( SAT M) . (A <=> B)) = ((( SAT M) . A) <=> (( SAT M) . B))

    proof

      

      thus (( SAT M) . (A <=> B)) = ((( SAT M) . (A => B)) '&' (( SAT M) . (B => A))) by semcon2

      .= (((( SAT M) . A) => (( SAT M) . B)) '&' (( SAT M) . (B => A))) by Def11

      .= ((( SAT M) . A) <=> (( SAT M) . B)) by Def11;

    end;

    theorem :: PL_AXIOM:26

    (( SAT M) . (A <=> B)) = 1 iff (( SAT M) . A) = (( SAT M) . B)

    proof

      

       A2: (( SAT M) . B) = TRUE or (( SAT M) . B) = FALSE by XBOOLEAN:def 3;

      hereby

        assume (( SAT M) . (A <=> B)) = 1;

        then ((( SAT M) . A) <=> (( SAT M) . B)) = 1 by semequ2;

        hence (( SAT M) . A) = (( SAT M) . B) by A2;

      end;

      assume

       A3: (( SAT M) . A) = (( SAT M) . B);

      

      thus (( SAT M) . (A <=> B)) = ((( SAT M) . A) <=> (( SAT M) . B)) by semequ2

      .= 1 by A3, A2;

    end;

    definition

      let M, p;

      :: PL_AXIOM:def15

      pred M |= p means (( SAT M) . p) = 1;

    end

    definition

      let M, F;

      :: PL_AXIOM:def16

      pred M |= F means for p st p in F holds M |= p;

    end

    definition

      let F, p;

      :: PL_AXIOM:def17

      pred F |= p means for M st M |= F holds M |= p;

    end

    definition

      let A;

      :: PL_AXIOM:def18

      attr A is tautology means for M holds (( SAT M) . A) = 1;

    end

    theorem :: PL_AXIOM:27

    

     tautsat: A is tautology iff ( {} PL-WFF ) |= A

    proof

      hereby

        assume

         A1: A is tautology;

        assume not ( {} PL-WFF ) |= A;

        then

        consider M such that

         A3: M |= ( {} PL-WFF ) & not M |= A;

        thus contradiction by A3, A1;

      end;

      assume

       A4: ( {} PL-WFF ) |= A;

      assume not A is tautology;

      then

      consider M such that

       A5: not (( SAT M) . A) = 1;

      M |= ( {} PL-WFF );

      then M |= A by A4;

      hence contradiction by A5;

    end;

    theorem :: PL_AXIOM:28

    

     Th15: (p => (q => p)) is tautology

    proof

      let M;

      

      thus (( SAT M) . (p => (q => p))) = ((( SAT M) . p) => (( SAT M) . (q => p))) by Def11

      .= ((( SAT M) . p) => ((( SAT M) . q) => (( SAT M) . p))) by Def11

      .= 1 by XBOOLEAN: 104;

    end;

    theorem :: PL_AXIOM:29

    

     Th16: ((p => (q => r)) => ((p => q) => (p => r))) is tautology

    proof

      let M;

      

      thus (( SAT M) . ((p => (q => r)) => ((p => q) => (p => r)))) = ((( SAT M) . (p => (q => r))) => (( SAT M) . ((p => q) => (p => r)))) by Def11

      .= (((( SAT M) . p) => (( SAT M) . (q => r))) => (( SAT M) . ((p => q) => (p => r)))) by Def11

      .= (((( SAT M) . p) => ((( SAT M) . q) => (( SAT M) . r))) => (( SAT M) . ((p => q) => (p => r)))) by Def11

      .= (((( SAT M) . p) => ((( SAT M) . q) => (( SAT M) . r))) => ((( SAT M) . (p => q)) => (( SAT M) . (p => r)))) by Def11

      .= (((( SAT M) . p) => ((( SAT M) . q) => (( SAT M) . r))) => (((( SAT M) . p) => (( SAT M) . q)) => (( SAT M) . (p => r)))) by Def11

      .= (((( SAT M) . p) => ((( SAT M) . q) => (( SAT M) . r))) => (((( SAT M) . p) => (( SAT M) . q)) => ((( SAT M) . p) => (( SAT M) . r)))) by Def11

      .= 1 by XBOOLEAN: 109;

    end;

    theorem :: PL_AXIOM:30

    

     Th17: ((( 'not' q) => ( 'not' p)) => ((( 'not' q) => p) => q)) is tautology

    proof

      let M;

      

      thus (( SAT M) . ((( 'not' q) => ( 'not' p)) => ((( 'not' q) => p) => q))) = ((( SAT M) . (( 'not' q) => ( 'not' p))) => (( SAT M) . ((( 'not' q) => p) => q))) by Def11

      .= (((( SAT M) . ( 'not' q)) => (( SAT M) . ( 'not' p))) => (( SAT M) . ((( 'not' q) => p) => q))) by Def11

      .= ((( 'not' (( SAT M) . q)) => (( SAT M) . ( 'not' p))) => (( SAT M) . ((( 'not' q) => p) => q))) by semnot2

      .= ((( 'not' (( SAT M) . q)) => ( 'not' (( SAT M) . p))) => (( SAT M) . ((( 'not' q) => p) => q))) by semnot2

      .= ((( 'not' (( SAT M) . q)) => ( 'not' (( SAT M) . p))) => ((( SAT M) . (( 'not' q) => p)) => (( SAT M) . q))) by Def11

      .= ((( 'not' (( SAT M) . q)) => ( 'not' (( SAT M) . p))) => (((( SAT M) . ( 'not' q)) => (( SAT M) . p)) => (( SAT M) . q))) by Def11

      .= ((( 'not' (( SAT M) . q)) => ( 'not' (( SAT M) . p))) => ((( 'not' (( SAT M) . q)) => (( SAT M) . p)) => (( SAT M) . q))) by semnot2

      .= 1 by Th17a;

    end;

    theorem :: PL_AXIOM:31

    ((p => q) => (( 'not' q) => ( 'not' p))) is tautology

    proof

      let M;

      

      thus (( SAT M) . ((p => q) => (( 'not' q) => ( 'not' p)))) = ((( SAT M) . (p => q)) => (( SAT M) . (( 'not' q) => ( 'not' p)))) by Def11

      .= (((( SAT M) . p) => (( SAT M) . q)) => (( SAT M) . (( 'not' q) => ( 'not' p)))) by Def11

      .= (((( SAT M) . p) => (( SAT M) . q)) => ((( SAT M) . ( 'not' q)) => (( SAT M) . ( 'not' p)))) by Def11

      .= (((( SAT M) . p) => (( SAT M) . q)) => (( 'not' (( SAT M) . q)) => (( SAT M) . ( 'not' p)))) by semnot2

      .= (((( SAT M) . p) => (( SAT M) . q)) => (( 'not' (( SAT M) . q)) => ( 'not' (( SAT M) . p)))) by semnot2

      .= 1 by th4;

    end;

    theorem :: PL_AXIOM:32

    ((p '&' q) => p) is tautology

    proof

      let M;

      

      thus (( SAT M) . ((p '&' q) => p)) = ((( SAT M) . (p '&' q)) => (( SAT M) . p)) by Def11

      .= (((( SAT M) . p) '&' (( SAT M) . q)) => (( SAT M) . p)) by semcon2

      .= 1 by th1;

    end;

    theorem :: PL_AXIOM:33

    ((p '&' q) => q) is tautology

    proof

      let M;

      

      thus (( SAT M) . ((p '&' q) => q)) = ((( SAT M) . (p '&' q)) => (( SAT M) . q)) by Def11

      .= (((( SAT M) . p) '&' (( SAT M) . q)) => (( SAT M) . q)) by semcon2

      .= 1 by th1;

    end;

    theorem :: PL_AXIOM:34

    (p => (p 'or' q)) is tautology

    proof

      let M;

      

      thus (( SAT M) . (p => (p 'or' q))) = ((( SAT M) . p) => (( SAT M) . (p 'or' q))) by Def11

      .= ((( SAT M) . p) => ((( SAT M) . p) 'or' (( SAT M) . q))) by semdis2

      .= 1 by XBOOLEAN: 123;

    end;

    theorem :: PL_AXIOM:35

    (q => (p 'or' q)) is tautology

    proof

      let M;

      

      thus (( SAT M) . (q => (p 'or' q))) = ((( SAT M) . q) => (( SAT M) . (p 'or' q))) by Def11

      .= ((( SAT M) . q) => ((( SAT M) . p) 'or' (( SAT M) . q))) by semdis2

      .= 1 by XBOOLEAN: 123;

    end;

    theorem :: PL_AXIOM:36

    ((p '&' q) <=> (q '&' p)) is tautology

    proof

      let M;

      

      thus (( SAT M) . ((p '&' q) <=> (q '&' p))) = ((( SAT M) . (p '&' q)) <=> (( SAT M) . (q '&' p))) by semequ2

      .= (((( SAT M) . p) '&' (( SAT M) . q)) <=> (( SAT M) . (q '&' p))) by semcon2

      .= (((( SAT M) . p) '&' (( SAT M) . q)) <=> ((( SAT M) . q) '&' (( SAT M) . p))) by semcon2

      .= 1 by th6;

    end;

    theorem :: PL_AXIOM:37

    ((p 'or' q) <=> (q 'or' p)) is tautology

    proof

      let M;

      

      thus (( SAT M) . ((p 'or' q) <=> (q 'or' p))) = ((( SAT M) . (p 'or' q)) <=> (( SAT M) . (q 'or' p))) by semequ2

      .= (((( SAT M) . p) 'or' (( SAT M) . q)) <=> (( SAT M) . (q 'or' p))) by semdis2

      .= (((( SAT M) . p) 'or' (( SAT M) . q)) <=> ((( SAT M) . q) 'or' (( SAT M) . p))) by semdis2

      .= 1 by th6a;

    end;

    theorem :: PL_AXIOM:38

    (((p '&' q) '&' r) <=> (p '&' (q '&' r))) is tautology

    proof

      let M;

      

      thus (( SAT M) . (((p '&' q) '&' r) <=> (p '&' (q '&' r)))) = ((( SAT M) . ((p '&' q) '&' r)) <=> (( SAT M) . (p '&' (q '&' r)))) by semequ2

      .= (((( SAT M) . (p '&' q)) '&' (( SAT M) . r)) <=> (( SAT M) . (p '&' (q '&' r)))) by semcon2

      .= (((( SAT M) . (p '&' q)) '&' (( SAT M) . r)) <=> ((( SAT M) . p) '&' (( SAT M) . (q '&' r)))) by semcon2

      .= (((( SAT M) . (p '&' q)) '&' (( SAT M) . r)) <=> ((( SAT M) . p) '&' ((( SAT M) . q) '&' (( SAT M) . r)))) by semcon2

      .= ((((( SAT M) . p) '&' (( SAT M) . q)) '&' (( SAT M) . r)) <=> ((( SAT M) . p) '&' ((( SAT M) . q) '&' (( SAT M) . r)))) by semcon2

      .= 1 by th7;

    end;

    theorem :: PL_AXIOM:39

    (((p 'or' q) 'or' r) <=> (p 'or' (q 'or' r))) is tautology

    proof

      let M;

      

      thus (( SAT M) . (((p 'or' q) 'or' r) <=> (p 'or' (q 'or' r)))) = ((( SAT M) . ((p 'or' q) 'or' r)) <=> (( SAT M) . (p 'or' (q 'or' r)))) by semequ2

      .= (((( SAT M) . (p 'or' q)) 'or' (( SAT M) . r)) <=> (( SAT M) . (p 'or' (q 'or' r)))) by semdis2

      .= (((( SAT M) . (p 'or' q)) 'or' (( SAT M) . r)) <=> ((( SAT M) . p) 'or' (( SAT M) . (q 'or' r)))) by semdis2

      .= (((( SAT M) . (p 'or' q)) 'or' (( SAT M) . r)) <=> ((( SAT M) . p) 'or' ((( SAT M) . q) 'or' (( SAT M) . r)))) by semdis2

      .= ((((( SAT M) . p) 'or' (( SAT M) . q)) 'or' (( SAT M) . r)) <=> ((( SAT M) . p) 'or' ((( SAT M) . q) 'or' (( SAT M) . r)))) by semdis2

      .= 1 by th7a;

    end;

    theorem :: PL_AXIOM:40

    ((p '&' (q 'or' r)) <=> ((p '&' q) 'or' (p '&' r))) is tautology

    proof

      let M;

      

      thus (( SAT M) . ((p '&' (q 'or' r)) <=> ((p '&' q) 'or' (p '&' r)))) = ((( SAT M) . (p '&' (q 'or' r))) <=> (( SAT M) . ((p '&' q) 'or' (p '&' r)))) by semequ2

      .= (((( SAT M) . p) '&' (( SAT M) . (q 'or' r))) <=> (( SAT M) . ((p '&' q) 'or' (p '&' r)))) by semcon2

      .= (((( SAT M) . p) '&' ((( SAT M) . q) 'or' (( SAT M) . r))) <=> (( SAT M) . ((p '&' q) 'or' (p '&' r)))) by semdis2

      .= (((( SAT M) . p) '&' ((( SAT M) . q) 'or' (( SAT M) . r))) <=> ((( SAT M) . (p '&' q)) 'or' (( SAT M) . (p '&' r)))) by semdis2

      .= (((( SAT M) . p) '&' ((( SAT M) . q) 'or' (( SAT M) . r))) <=> (((( SAT M) . p) '&' (( SAT M) . q)) 'or' (( SAT M) . (p '&' r)))) by semcon2

      .= (((( SAT M) . p) '&' ((( SAT M) . q) 'or' (( SAT M) . r))) <=> (((( SAT M) . p) '&' (( SAT M) . q)) 'or' ((( SAT M) . p) '&' (( SAT M) . r)))) by semcon2

      .= 1 by th8;

    end;

    theorem :: PL_AXIOM:41

    ((p 'or' (q '&' r)) <=> ((p 'or' q) '&' (p 'or' r))) is tautology

    proof

      let M;

      

      thus (( SAT M) . ((p 'or' (q '&' r)) <=> ((p 'or' q) '&' (p 'or' r)))) = ((( SAT M) . (p 'or' (q '&' r))) <=> (( SAT M) . ((p 'or' q) '&' (p 'or' r)))) by semequ2

      .= (((( SAT M) . p) 'or' (( SAT M) . (q '&' r))) <=> (( SAT M) . ((p 'or' q) '&' (p 'or' r)))) by semdis2

      .= (((( SAT M) . p) 'or' ((( SAT M) . q) '&' (( SAT M) . r))) <=> (( SAT M) . ((p 'or' q) '&' (p 'or' r)))) by semcon2

      .= (((( SAT M) . p) 'or' ((( SAT M) . q) '&' (( SAT M) . r))) <=> ((( SAT M) . (p 'or' q)) '&' (( SAT M) . (p 'or' r)))) by semcon2

      .= (((( SAT M) . p) 'or' ((( SAT M) . q) '&' (( SAT M) . r))) <=> (((( SAT M) . p) 'or' (( SAT M) . q)) '&' (( SAT M) . (p 'or' r)))) by semdis2

      .= (((( SAT M) . p) 'or' ((( SAT M) . q) '&' (( SAT M) . r))) <=> (((( SAT M) . p) 'or' (( SAT M) . q)) '&' ((( SAT M) . p) 'or' (( SAT M) . r)))) by semdis2

      .= 1 by th8a;

    end;

    theorem :: PL_AXIOM:42

    (( 'not' ( 'not' p)) <=> p) is tautology

    proof

      let M;

      

      thus (( SAT M) . (( 'not' ( 'not' p)) <=> p)) = ((( SAT M) . ( 'not' ( 'not' p))) <=> (( SAT M) . p)) by semequ2

      .= (( 'not' (( SAT M) . ( 'not' p))) <=> (( SAT M) . p)) by semnot2

      .= (( 'not' ( 'not' (( SAT M) . p))) <=> (( SAT M) . p)) by semnot2

      .= 1 by th2;

    end;

    theorem :: PL_AXIOM:43

    (( 'not' (p '&' q)) <=> (( 'not' p) 'or' ( 'not' q))) is tautology

    proof

      let M;

      

      thus (( SAT M) . (( 'not' (p '&' q)) <=> (( 'not' p) 'or' ( 'not' q)))) = ((( SAT M) . ( 'not' (p '&' q))) <=> (( SAT M) . (( 'not' p) 'or' ( 'not' q)))) by semequ2

      .= (( 'not' (( SAT M) . (p '&' q))) <=> (( SAT M) . (( 'not' p) 'or' ( 'not' q)))) by semnot2

      .= (( 'not' ((( SAT M) . p) '&' (( SAT M) . q))) <=> (( SAT M) . (( 'not' p) 'or' ( 'not' q)))) by semcon2

      .= (( 'not' ((( SAT M) . p) '&' (( SAT M) . q))) <=> ((( SAT M) . ( 'not' p)) 'or' (( SAT M) . ( 'not' q)))) by semdis2

      .= (( 'not' ((( SAT M) . p) '&' (( SAT M) . q))) <=> (( 'not' (( SAT M) . p)) 'or' (( SAT M) . ( 'not' q)))) by semnot2

      .= (( 'not' ((( SAT M) . p) '&' (( SAT M) . q))) <=> (( 'not' (( SAT M) . p)) 'or' ( 'not' (( SAT M) . q)))) by semnot2

      .= 1 by th3;

    end;

    theorem :: PL_AXIOM:44

    (( 'not' (p 'or' q)) <=> (( 'not' p) '&' ( 'not' q))) is tautology

    proof

      let M;

      

      thus (( SAT M) . (( 'not' (p 'or' q)) <=> (( 'not' p) '&' ( 'not' q)))) = ((( SAT M) . ( 'not' (p 'or' q))) <=> (( SAT M) . (( 'not' p) '&' ( 'not' q)))) by semequ2

      .= (( 'not' (( SAT M) . (p 'or' q))) <=> (( SAT M) . (( 'not' p) '&' ( 'not' q)))) by semnot2

      .= (( 'not' ((( SAT M) . p) 'or' (( SAT M) . q))) <=> (( SAT M) . (( 'not' p) '&' ( 'not' q)))) by semdis2

      .= (( 'not' ((( SAT M) . p) 'or' (( SAT M) . q))) <=> ((( SAT M) . ( 'not' p)) '&' (( SAT M) . ( 'not' q)))) by semcon2

      .= (( 'not' ((( SAT M) . p) 'or' (( SAT M) . q))) <=> (( 'not' (( SAT M) . p)) '&' (( SAT M) . ( 'not' q)))) by semnot2

      .= (( 'not' ((( SAT M) . p) 'or' (( SAT M) . q))) <=> (( 'not' (( SAT M) . p)) '&' ( 'not' (( SAT M) . q)))) by semnot2

      .= 1 by th3a;

    end;

    theorem :: PL_AXIOM:45

    ((p => q) => ((p => r) => (p => (q '&' r)))) is tautology

    proof

      let M;

      

      thus (( SAT M) . ((p => q) => ((p => r) => (p => (q '&' r))))) = ((( SAT M) . (p => q)) => (( SAT M) . ((p => r) => (p => (q '&' r))))) by Def11

      .= (((( SAT M) . p) => (( SAT M) . q)) => (( SAT M) . ((p => r) => (p => (q '&' r))))) by Def11

      .= (((( SAT M) . p) => (( SAT M) . q)) => ((( SAT M) . (p => r)) => (( SAT M) . (p => (q '&' r))))) by Def11

      .= (((( SAT M) . p) => (( SAT M) . q)) => (((( SAT M) . p) => (( SAT M) . r)) => (( SAT M) . (p => (q '&' r))))) by Def11

      .= (((( SAT M) . p) => (( SAT M) . q)) => (((( SAT M) . p) => (( SAT M) . r)) => ((( SAT M) . p) => (( SAT M) . (q '&' r))))) by Def11

      .= (((( SAT M) . p) => (( SAT M) . q)) => (((( SAT M) . p) => (( SAT M) . r)) => ((( SAT M) . p) => ((( SAT M) . q) '&' (( SAT M) . r))))) by semcon2

      .= 1 by th5;

    end;

    theorem :: PL_AXIOM:46

    ((p => r) => ((q => r) => ((p 'or' q) => r))) is tautology

    proof

      let M;

      

       A3: (( SAT M) . ((q => r) => ((p 'or' q) => r))) = ((( SAT M) . (q => r)) => (( SAT M) . ((p 'or' q) => r))) by Def11

      .= (((( SAT M) . q) => (( SAT M) . r)) => (( SAT M) . ((p 'or' q) => r))) by Def11

      .= (((( SAT M) . q) => (( SAT M) . r)) => ((( SAT M) . (p 'or' q)) => (( SAT M) . r))) by Def11

      .= (((( SAT M) . q) => (( SAT M) . r)) => (((( SAT M) . p) 'or' (( SAT M) . q)) => (( SAT M) . r))) by semdis2;

      

      thus (( SAT M) . ((p => r) => ((q => r) => ((p 'or' q) => r)))) = ((( SAT M) . (p => r)) => (( SAT M) . ((q => r) => ((p 'or' q) => r)))) by Def11

      .= (((( SAT M) . p) => (( SAT M) . r)) => (((( SAT M) . q) => (( SAT M) . r)) => (((( SAT M) . p) 'or' (( SAT M) . q)) => (( SAT M) . r)))) by Def11, A3

      .= 1 by th5a;

    end;

    theorem :: PL_AXIOM:47

    

     th24: F |= A & F |= (A => B) implies F |= B

    proof

      assume that

       A1: F |= A and

       A2: F |= (A => B);

      let M;

      assume

       A3: M |= F;

      then M |= (A => B) by A2;

      then

       A4: ((( SAT M) . A) => (( SAT M) . B)) = 1 by Def11;

      M |= A by A1, A3;

      hence (( SAT M) . B) = 1 by A4;

    end;

    begin

    definition

      let D be set;

      :: PL_AXIOM:def19

      attr D is with_PL_axioms means

      : withplax: for p, q, r holds ((p => (q => p)) in D & ((p => (q => r)) => ((p => q) => (p => r))) in D & ((( 'not' q) => ( 'not' p)) => ((( 'not' q) => p) => q)) in D);

    end

    definition

      :: PL_AXIOM:def20

      func PL_axioms -> Subset of PL-WFF means

      : defplax: it is with_PL_axioms & for D be Subset of PL-WFF st D is with_PL_axioms holds it c= D;

      existence

      proof

        defpred S1[ object] means for D be set st D is with_PL_axioms holds $1 in D;

        consider D0 be set such that

         A1: for x be object holds (x in D0 iff x in PL-WFF & S1[x]) from XBOOLE_0:sch 1;

        D0 c= PL-WFF by A1;

        then

        reconsider D0 as Subset of PL-WFF ;

        take D0;

        thus D0 is with_PL_axioms

        proof

          let p,q,r be Element of PL-WFF ;

          for D be set st D is with_PL_axioms holds (p => (q => p)) in D;

          hence (p => (q => p)) in D0 by A1;

          for D be set st D is with_PL_axioms holds ((p => (q => r)) => ((p => q) => (p => r))) in D;

          hence ((p => (q => r)) => ((p => q) => (p => r))) in D0 by A1;

          for D be set st D is with_PL_axioms holds ((( 'not' q) => ( 'not' p)) => ((( 'not' q) => p) => q)) in D;

          hence ((( 'not' q) => ( 'not' p)) => ((( 'not' q) => p) => q)) in D0 by A1;

        end;

        let D be Subset of PL-WFF ;

        assume

         A2: D is with_PL_axioms;

        let x be object;

        assume x in D0;

        hence x in D by A1, A2;

      end;

      uniqueness

      proof

        let D1,D2 be Subset of PL-WFF ;

        assume (D1 is with_PL_axioms) & (for D be Subset of PL-WFF st D is with_PL_axioms holds D1 c= D) & D2 is with_PL_axioms & for D be Subset of PL-WFF st D is with_PL_axioms holds D2 c= D;

        then D1 c= D2 & D2 c= D1;

        hence D1 = D2 by XBOOLE_0:def 10;

      end;

    end

    registration

      cluster PL_axioms -> with_PL_axioms;

      coherence by defplax;

    end

    definition

      let p, q, r;

      :: PL_AXIOM:def21

      pred p,q MP_rule r means q = (p => r);

    end

    registration

      cluster PL_axioms -> non empty;

      coherence by withplax;

    end

    definition

      let A;

      :: PL_AXIOM:def22

      attr A is axpl1 means

      : defaxpl1: ex p, q st A = (p => (q => p));

      :: PL_AXIOM:def23

      attr A is axpl2 means

      : defaxpl2: ex p, q, r st A = ((p => (q => r)) => ((p => q) => (p => r)));

      :: PL_AXIOM:def24

      attr A is axpl3 means

      : defaxpl3: ex p, q st A = ((( 'not' q) => ( 'not' p)) => ((( 'not' q) => p) => q));

    end

    theorem :: PL_AXIOM:48

    

     Th36: for A be Element of PL_axioms holds (A is axpl1 or A is axpl2 or A is axpl3)

    proof

      defpred P1[ Element of PL_axioms ] means $1 is axpl1 or $1 is axpl2 or $1 is axpl3;

      set X = { p where p be Element of PL_axioms : P1[p] };

      X c= PL-WFF

      proof

        let x be object;

        assume x in X;

        then ex p be Element of PL_axioms st x = p & P1[p];

        hence x in PL-WFF ;

      end;

      then

      reconsider X as Subset of PL-WFF ;

      let A be Element of PL_axioms ;

      X is with_PL_axioms

      proof

        let p, q, r;

        thus (p => (q => p)) in X

        proof

          reconsider pp = (p => (q => p)) as Element of PL_axioms by withplax;

           P1[pp] by defaxpl1;

          hence thesis;

        end;

        thus ((p => (q => r)) => ((p => q) => (p => r))) in X

        proof

          reconsider pp = ((p => (q => r)) => ((p => q) => (p => r))) as Element of PL_axioms by withplax;

           P1[pp] by defaxpl2;

          hence thesis;

        end;

        thus ((( 'not' q) => ( 'not' p)) => ((( 'not' q) => p) => q)) in X

        proof

          reconsider pp = ((( 'not' q) => ( 'not' p)) => ((( 'not' q) => p) => q)) as Element of PL_axioms by withplax;

           P1[pp] by defaxpl3;

          hence thesis;

        end;

      end;

      then A in PL_axioms & PL_axioms c= X by defplax;

      then A in X;

      then ex p be Element of PL_axioms st A = p & P1[p];

      hence P1[A];

    end;

    theorem :: PL_AXIOM:49

    

     Th37: A is axpl1 or A is axpl2 or A is axpl3 implies F |= A

    proof

      assume

       A1: A is axpl1 or A is axpl2 or A is axpl3;

      let M;

      assume M |= F;

      per cases by A1;

        suppose A is axpl1;

        then

        consider p,q be Element of PL-WFF such that

         A2: A = (p => (q => p));

        A is tautology by Th15, A2;

        hence thesis;

      end;

        suppose A is axpl2;

        then

        consider p,q,r be Element of PL-WFF such that

         A3: A = ((p => (q => r)) => ((p => q) => (p => r)));

        A is tautology by Th16, A3;

        hence thesis;

      end;

        suppose A is axpl3;

        then

        consider p,q be Element of PL-WFF such that

         A4: A = ((( 'not' q) => ( 'not' p)) => ((( 'not' q) => p) => q));

        A is tautology by Th17, A4;

        hence thesis;

      end;

    end;

    definition

      let i be Nat, f, F;

      :: PL_AXIOM:def25

      pred prc f,F,i means

      : defprc: (f . i) in PL_axioms or (f . i) in F or (ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & (((f /. j),(f /. k)) MP_rule (f /. i)));

    end

    definition

      let F, p;

      :: PL_AXIOM:def26

      pred F |- p means ex f st (f . ( len f)) = p & 1 <= ( len f) & for i be Nat st 1 <= i & i <= ( len f) holds prc (f,F,i);

    end

    theorem :: PL_AXIOM:50

    

     Th38: for i,n be Nat st (n + ( len f)) <= ( len f2) & (for k be Nat st 1 <= k & k <= ( len f) holds (f . k) = (f2 . (k + n))) & 1 <= i <= ( len f) holds prc (f,F,i) implies prc (f2,F,(i + n))

    proof

      let i,n be Nat;

      assume that

       A1: (n + ( len f)) <= ( len f2) and

       A2: for k be Nat st 1 <= k & k <= ( len f) holds (f . k) = (f2 . (k + n)) and

       A3: 1 <= i and

       A4: i <= ( len f);

      (i + n) <= (( len f) + n) by A4, XREAL_1: 6;

      then

       A5: (i + n) <= ( len f2) by A1, XXREAL_0: 2;

      

       A6: (f /. i) = (f . i) by A3, A4, LTLAXIO5: 1

      .= (f2 . (i + n)) by A2, A3, A4

      .= (f2 /. (i + n)) by A3, A5, LTLAXIO5: 1, NAT_1: 12;

      assume

       A7: prc (f,F,i);

      per cases by A7;

        suppose (f . i) in PL_axioms ;

        hence prc (f2,F,(i + n)) by A2, A3, A4;

      end;

        suppose (f . i) in F;

        hence prc (f2,F,(i + n)) by A2, A3, A4;

      end;

        suppose ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & ((f /. j),(f /. k)) MP_rule (f /. i);

        then

        consider j,k be Nat such that

         A8: 1 <= j and

         A9: j < i and

         A10: 1 <= k and

         A11: k < i and

         A12: ((f /. j),(f /. k)) MP_rule (f /. i);

        

         A13: 1 <= (j + n) & (j + n) < (i + n) by A8, A9, NAT_1: 12, XREAL_1: 8;

        

         A14: k <= ( len f) by A4, A11, XXREAL_0: 2;

        then (k + n) <= (( len f) + n) by XREAL_1: 6;

        then

         A15: (k + n) <= ( len f2) by A1, XXREAL_0: 2;

        

         A16: j <= ( len f) by A4, A9, XXREAL_0: 2;

        then (j + n) <= (( len f) + n) by XREAL_1: 6;

        then

         A17: (j + n) <= ( len f2) by A1, XXREAL_0: 2;

        

         A18: (f /. k) = (f . k) by A10, A14, LTLAXIO5: 1

        .= (f2 . (k + n)) by A2, A10, A14

        .= (f2 /. (k + n)) by A10, A15, LTLAXIO5: 1, NAT_1: 12;

        

         A19: 1 <= (k + n) & (k + n) < (i + n) by A10, A11, NAT_1: 12, XREAL_1: 8;

        (f /. j) = (f . j) by A8, A16, LTLAXIO5: 1

        .= (f2 . (j + n)) by A2, A8, A16

        .= (f2 /. (j + n)) by A8, A17, LTLAXIO5: 1, NAT_1: 12;

        hence prc (f2,F,(i + n)) by A6, A12, A13, A19, A18;

      end;

    end;

    theorem :: PL_AXIOM:51

    

     Th39: f2 = (f ^ f1) & 1 <= ( len f) & 1 <= ( len f1) & (for i be Nat st 1 <= i & i <= ( len f) holds prc (f,F,i)) & (for i be Nat st 1 <= i & i <= ( len f1) holds prc (f1,F,i)) implies for i be Nat st 1 <= i & i <= ( len f2) holds prc (f2,F,i)

    proof

      assume that

       A1: f2 = (f ^ f1) and 1 <= ( len f) and 1 <= ( len f1) and

       A2: for i be Nat st 1 <= i & i <= ( len f) holds prc (f,F,i) and

       A3: for i be Nat st 1 <= i & i <= ( len f1) holds prc (f1,F,i);

      

       A4: ( len f2) = (( len f) + ( len f1)) by A1, FINSEQ_1: 22;

      

       A5: for k be Nat st 1 <= k & k <= ( len f1) holds (f1 . k) = (f2 . (k + ( len f))) by A1, FINSEQ_1: 65;

      let i be Nat;

      assume that

       A6: 1 <= i and

       A7: i <= ( len f2);

      per cases by NAT_1: 13;

        suppose

         A8: i <= ( len f);

        

        then

         A9: (f /. i) = (f . i) by A6, LTLAXIO5: 1

        .= (f2 . i) by A1, A6, A8, FINSEQ_1: 64

        .= (f2 /. i) by A6, A7, LTLAXIO5: 1;

        per cases by A2, A6, A8, defprc;

          suppose (f . i) in PL_axioms ;

          hence prc (f2,F,i) by A1, A6, A8, FINSEQ_1: 64;

        end;

          suppose (f . i) in F;

          hence prc (f2,F,i) by A1, A6, A8, FINSEQ_1: 64;

        end;

          suppose ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & ((f /. j),(f /. k)) MP_rule (f /. i);

          then

          consider j,k be Nat such that

           A10: 1 <= j and

           A11: j < i and

           A12: 1 <= k and

           A13: k < i and

           A14: ((f /. j),(f /. k)) MP_rule (f /. i);

          

           A15: k <= ( len f) by A8, A13, XXREAL_0: 2;

          then

           A16: k <= ( len f2) by A4, NAT_1: 12;

          

           A17: (f /. k) = (f . k) by A12, A15, LTLAXIO5: 1

          .= (f2 . k) by A1, A12, A15, FINSEQ_1: 64

          .= (f2 /. k) by A12, A16, LTLAXIO5: 1;

          

           A18: j <= ( len f) by A8, A11, XXREAL_0: 2;

          then

           A19: j <= ( len f2) by A4, NAT_1: 12;

          (f /. j) = (f . j) by A10, A18, LTLAXIO5: 1

          .= (f2 . j) by A1, A10, A18, FINSEQ_1: 64

          .= (f2 /. j) by A10, A19, LTLAXIO5: 1;

          hence prc (f2,F,i) by A9, A10, A11, A12, A13, A14, A17;

        end;

      end;

        suppose

         A25: (( len f) + 1) <= i;

        set i1 = (i -' ( len f));

        i <= (( len f) + ( len f1)) by A1, A7, FINSEQ_1: 22;

        then (i -' ( len f)) <= ((( len f) + ( len f1)) -' ( len f)) by NAT_D: 42;

        then

         A26: i1 <= ( len f1) by NAT_D: 34;

        1 <= i1 by A25, NAT_D: 55;

        then prc (f2,F,(i1 + ( len f))) by A3, A4, A5, A26, Th38;

        hence prc (f2,F,i) by A25, NAT_D: 43, NAT_D: 55;

      end;

    end;

    theorem :: PL_AXIOM:52

    

     Th40: (f = (f1 ^ <*p*>) & 1 <= ( len f1) & for i be Nat st 1 <= i & i <= ( len f1) holds prc (f1,F,i)) & prc (f,F,( len f)) implies (for i be Nat st 1 <= i & i <= ( len f) holds prc (f,F,i)) & F |- p

    proof

      assume that

       A1: f = (f1 ^ <*p*>) and 1 <= ( len f1) and

       A2: for i be Nat st 1 <= i & i <= ( len f1) holds prc (f1,F,i);

      

       A3: ( len f) = (( len f1) + ( len <*p*>)) by A1, FINSEQ_1: 22

      .= (( len f1) + 1) by FINSEQ_1: 39;

      assume

       A4: prc (f,F,( len f));

      

       A5: ( 0 + ( len f1)) <= ( len f) by A3, NAT_1: 12;

       A6:

      now

        let i be Nat;

        assume that

         A7: 1 <= i and

         A8: i <= ( len f);

        

         A9: i < (( len f1) + 1) or i = (( len f1) + 1) by A3, A8, XXREAL_0: 1;

        

         A10: for k be Nat st 1 <= k & k <= ( len f1) holds (f1 . k) = (f . (k + 0 )) by A1, FINSEQ_1: 64;

        per cases by A3, A9, NAT_1: 13;

          suppose i <= ( len f1);

          then prc (f,F,(i + 0 )) by A2, A5, A7, A10, Th38;

          hence prc (f,F,i);

        end;

          suppose i = ( len f);

          hence prc (f,F,i) by A4;

        end;

      end;

      hence for i be Nat st 1 <= i & i <= ( len f) holds prc (f,F,i);

      (f . ( len f)) = (f . (( len f1) + ( len <*p*>))) by A1, FINSEQ_1: 22

      .= (f . (( len f1) + 1)) by FINSEQ_1: 39

      .= p by A1, FINSEQ_1: 42;

      hence F |- p by A3, XREAL_1: 31, A6;

    end;

    theorem :: PL_AXIOM:53

    

     th42: p in PL_axioms or p in F implies F |- p

    proof

      defpred P1[ set, set] means $2 = p;

      

       A1: for k be Nat st k in ( Seg 1) holds ex x be Element of PL-WFF st P1[k, x];

      consider f such that

       A2: ( dom f) = ( Seg 1) & for k be Nat st k in ( Seg 1) holds P1[k, (f . k)] from FINSEQ_1:sch 5( A1);

      

       A3: ( len f) = 1 by A2, FINSEQ_1:def 3;

      1 in ( Seg 1);

      then

       A4: (f . 1) = p by A2;

      assume

       A5: p in PL_axioms or p in F;

      for j be Nat st 1 <= j & j <= ( len f) holds prc (f,F,j)

      proof

        let j be Nat;

        assume

         A6: 1 <= j & j <= ( len f);

        per cases by A5;

          suppose p in PL_axioms ;

          hence thesis by A3, A4, A6, XXREAL_0: 1;

        end;

          suppose p in F;

          hence thesis by A3, A4, A6, XXREAL_0: 1;

        end;

      end;

      hence F |- p by A3, A4;

    end;

    theorem :: PL_AXIOM:54

    

     th43: F |- p & F |- (p => q) implies F |- q

    proof

      assume F |- p;

      then

      consider f such that

       A1: (f . ( len f)) = p and

       A2: 1 <= ( len f) and

       A3: for i be Nat st 1 <= i & i <= ( len f) holds prc (f,F,i);

      set j = ( len f);

      assume F |- (p => q);

      then

      consider f1 such that

       A4: (f1 . ( len f1)) = (p => q) and

       A5: 1 <= ( len f1) and

       A6: for i be Nat st 1 <= i & i <= ( len f1) holds prc (f1,F,i);

      

       A7: 1 <= (( len f) + ( len f1)) by A2, NAT_1: 12;

      set g = ((f ^ f1) ^ <*q*>);

      

       A8: g = (f ^ (f1 ^ <*q*>)) by FINSEQ_1: 32;

      

       A9: for i be Nat st 1 <= i & i <= ( len f1) holds (g . (( len f) + i)) = (f1 . i)

      proof

        let i be Nat;

        assume that

         A10: 1 <= i and

         A11: i <= ( len f1);

        ( len (f1 ^ <*q*>)) = (( len f1) + ( len <*q*>)) by FINSEQ_1: 22

        .= (( len f1) + 1) by FINSEQ_1: 39;

        then i <= ( len (f1 ^ <*q*>)) by A11, NAT_1: 12;

        

        hence (g . (( len f) + i)) = ((f1 ^ <*q*>) . i) by A8, A10, FINSEQ_1: 65

        .= (f1 . i) by A10, A11, FINSEQ_1: 64;

      end;

      

       A12: ( len g) = (( len (f ^ f1)) + ( len <*q*>)) by FINSEQ_1: 22

      .= (( len (f ^ f1)) + 1) by FINSEQ_1: 39;

      then

       A13: ( len g) = ((( len f) + ( len f1)) + 1) by FINSEQ_1: 22;

      then ( len g) = (( len f) + (( len f1) + 1));

      then

       A14: j < ( len g) by NAT_1: 16;

      

      then

       A15: (g /. j) = (g . j) by A2, LTLAXIO5: 1

      .= p by A1, A2, A8, FINSEQ_1: 64;

      set k = (( len f) + ( len f1));

      

       A16: 1 <= k by A2, NAT_1: 12;

      

       U1: (g . ( len g)) = q & 1 <= ( len g) by A12, FINSEQ_1: 42, NAT_1: 11;

      

       A18: k < ( len g) by A13, NAT_1: 16;

      

      then (g /. k) = (g . k) by A2, LTLAXIO5: 1, NAT_1: 12

      .= (p => q) by A4, A5, A9;

      then ((g /. j),(g /. k)) MP_rule (g /. ( len g)) by A15, LTLAXIO5: 1, U1;

      then

       A19: ( len (f ^ f1)) = (( len f) + ( len f1)) & prc (g,F,( len g)) by A2, A14, A16, A18, FINSEQ_1: 22;

      for i be Nat st 1 <= i & i <= ( len (f ^ f1)) holds prc ((f ^ f1),F,i) by A2, A3, A5, A6, Th39;

      hence F |- q by A7, A19, Th40;

    end;

    theorem :: PL_AXIOM:55

    

     monmp: F c= G implies (F |- p implies G |- p)

    proof

      assume

       Z0: F c= G;

      assume F |- p;

      then

      consider f such that

       C1: (f . ( len f)) = p & 1 <= ( len f) & for k be Nat st 1 <= k <= ( len f) holds prc (f,F,k);

      

       C17: ( len f) in ( dom f) by C1, FINSEQ_3: 25;

      defpred P3[ Nat] means 1 <= $1 <= ( len f) implies G |- (f /. $1);

       C2:

      now

        let s be Nat;

        assume

         C5: for n be Nat st n < s holds P3[n];

        per cases by NAT_1: 14;

          suppose s = 0 ;

          hence P3[s];

        end;

          suppose not s < 1;

          assume

           C7: 1 <= s <= ( len f);

          then

           C3: prc (f,F,s) by C1;

          

           C16: s in ( dom f) by C7, FINSEQ_3: 25;

          thus G |- (f /. s)

          proof

            per cases by C3;

              suppose (f . s) in PL_axioms ;

              then (f /. s) in PL_axioms by C16, PARTFUN1:def 6;

              hence G |- (f /. s) by th42;

            end;

              suppose (f . s) in F;

              then (f /. s) in F by C16, PARTFUN1:def 6;

              hence G |- (f /. s) by th42, Z0;

            end;

              suppose ex j,k be Nat st 1 <= j & j < s & 1 <= k & k < s & (((f /. j),(f /. k)) MP_rule (f /. s));

              then

              consider j,k be Nat such that

               C4: 1 <= j & j < s & 1 <= k & k < s & (((f /. j),(f /. k)) MP_rule (f /. s));

              

               C6: P3[j] by C5, C4;

               P3[k] by C4, C5;

              hence G |- (f /. s) by th43, C7, XXREAL_0: 2, C4, C6;

            end;

          end;

        end;

      end;

      for k be Nat holds P3[k] from NAT_1:sch 4( C2);

      then G |- (f /. ( len f)) by C1;

      hence G |- p by C1, C17, PARTFUN1:def 6;

    end;

    begin

    theorem :: PL_AXIOM:56

    

     sth: F |- A implies F |= A

    proof

      assume F |- A;

      then

      consider f such that

       A1: (f . ( len f)) = A and

       A2: 1 <= ( len f) and

       A3: for i be Nat st 1 <= i & i <= ( len f) holds prc (f,F,i);

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies F |= (f /. $1);

      

       A4: for i be Nat st for j be Nat st j < i holds P[j] holds P[i]

      proof

        let i be Nat;

        assume

         A5: for j be Nat st j < i holds P[j];

        per cases by NAT_1: 14;

          suppose i = 0 ;

          hence P[i];

        end;

          suppose not i < 1;

          assume that

           A6: 1 <= i and

           A7: i <= ( len f);

          per cases by A3, A6, A7, defprc;

            suppose (f . i) in PL_axioms ;

            then (f /. i) in PL_axioms by A6, A7, LTLAXIO5: 1;

            then (f /. i) is axpl1 or (f /. i) is axpl2 or (f /. i) is axpl3 by Th36;

            hence F |= (f /. i) by Th37;

          end;

            suppose (f . i) in F;

            then

             A9: (f /. i) in F by A6, A7, LTLAXIO5: 1;

            thus F |= (f /. i)

            proof

              let M;

              assume M |= F;

              hence M |= (f /. i) by A9;

            end;

          end;

            suppose ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & ((f /. j),(f /. k)) MP_rule (f /. i);

            then

            consider j,k be Nat such that

             A10: 1 <= j and

             A11: j < i and

             A12: 1 <= k and

             A13: k < i and

             A14: ((f /. j),(f /. k)) MP_rule (f /. i);

            

             U1: k <= ( len f) by A7, A13, XXREAL_0: 2;

            

             A16: j <= ( len f) by A7, A11, XXREAL_0: 2;

            F |= ((f /. j) => (f /. i)) by A5, A12, A13, A14, U1;

            hence F |= (f /. i) by A5, A10, A11, A16, th24;

          end;

        end;

      end;

      

       A22: for i be Nat holds P[i] from NAT_1:sch 4( A4);

      (f /. ( len f)) = A by A1, A2, LTLAXIO5: 1;

      hence F |= A by A2, A22;

    end;

    theorem :: PL_AXIOM:57

    

     thaa: F |- (A => A)

    proof

      (A => ((A => A) => A)) in PL_axioms by withplax;

      then

       A1: F |- (A => ((A => A) => A)) by th42;

      (A => (A => A)) in PL_axioms by withplax;

      then

       A2: F |- (A => (A => A)) by th42;

      ((A => ((A => A) => A)) => ((A => (A => A)) => (A => A))) in PL_axioms by withplax;

      then F |- ((A => ((A => A) => A)) => ((A => (A => A)) => (A => A))) by th42;

      then F |- ((A => (A => A)) => (A => A)) by th43, A1;

      hence F |- (A => A) by th43, A2;

    end;

    ::$Notion-Name

    theorem :: PL_AXIOM:58

    

     ded: (F \/ {A}) |- B implies F |- (A => B)

    proof

      assume (F \/ {A}) |- B;

      then

      consider f such that

       A1: (f . ( len f)) = B and

       A2: 1 <= ( len f) and

       A3: for i be Nat st 1 <= i & i <= ( len f) holds prc (f,(F \/ {A}),i);

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies F |- (A => (f /. $1));

      

       A4: for i be Nat st for j be Nat st j < i holds P[j] holds P[i]

      proof

        let i be Nat;

        assume

         A5: for j be Nat st j < i holds P[j];

        per cases by NAT_1: 14;

          suppose i = 0 ;

          hence P[i];

        end;

          suppose not i < 1;

          assume that

           A6: 1 <= i and

           A7: i <= ( len f);

          per cases by A3, A6, A7, defprc;

            suppose

             A8: (f . i) in PL_axioms ;

            ((f /. i) => (A => (f /. i))) in PL_axioms by withplax;

            then

             A9: F |- ((f /. i) => (A => (f /. i))) by th42;

            (f /. i) in PL_axioms by A6, A7, A8, LTLAXIO5: 1;

            then F |- (f /. i) by th42;

            hence thesis by th43, A9;

          end;

            suppose

             A10: (f . i) in (F \/ {A});

            per cases by A10, XBOOLE_0:def 3;

              suppose

               A11: (f . i) in F;

              ((f /. i) => (A => (f /. i))) in PL_axioms by withplax;

              then

               A12: F |- ((f /. i) => (A => (f /. i))) by th42;

              (f /. i) in F by A6, A7, A11, LTLAXIO5: 1;

              then F |- (f /. i) by th42;

              hence thesis by th43, A12;

            end;

              suppose (f . i) in {A};

              then (f . i) = A by TARSKI:def 1;

              then (f /. i) = A by A6, A7, LTLAXIO5: 1;

              hence thesis by thaa;

            end;

          end;

            suppose ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & ((f /. j),(f /. k)) MP_rule (f /. i);

            then

            consider j,k be Nat such that

             A15: 1 <= j and

             A16: j < i and

             A17: 1 <= k and

             A18: k < i and

             A19: ((f /. j),(f /. k)) MP_rule (f /. i);

            j <= ( len f) by A7, A16, XXREAL_0: 2;

            then

             A20: F |- (A => (f /. j)) by A5, A15, A16;

            k <= ( len f) by A7, A18, XXREAL_0: 2;

            then

             A21: F |- (A => (f /. k)) by A5, A17, A18;

            ((A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i)))) in PL_axioms by withplax;

            then

             A23: F |- ((A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i)))) by th42;

            F |- ((A => (f /. j)) => (A => (f /. i))) by A23, th43, A21, A19;

            hence F |- (A => (f /. i)) by A20, th43;

          end;

        end;

      end;

      

       A37: for i be Nat holds P[i] from NAT_1:sch 4( A4);

      B = (f /. ( len f)) by A1, A2, LTLAXIO5: 1;

      hence F |- (A => B) by A2, A37;

    end;

    theorem :: PL_AXIOM:59

    F |- (A => B) implies (F \/ {A}) |- B

    proof

      A in {A} by TARSKI:def 1;

      then A in (F \/ {A}) by XBOOLE_0:def 3;

      then

       A1: (F \/ {A}) |- A by th42;

      assume F |- (A => B);

      then (F \/ {A}) |- (A => B) by monmp, XBOOLE_1: 7;

      hence (F \/ {A}) |- B by A1, th43;

    end;

    theorem :: PL_AXIOM:60

    

     naab: F |- (( 'not' A) => (A => B))

    proof

      set f = ((F \/ {( 'not' A)}) \/ {A});

      A in f by ZFMISC_1: 31, XBOOLE_1: 11;

      then

       A1: f |- A by th42;

      f = ((F \/ {A}) \/ {( 'not' A)}) by XBOOLE_1: 4;

      then ( 'not' A) in f by ZFMISC_1: 31, XBOOLE_1: 11;

      then

       A2: f |- ( 'not' A) by th42;

      (A => (( 'not' B) => A)) in PL_axioms by withplax;

      then f |- (A => (( 'not' B) => A)) by th42;

      then

       A4: f |- (( 'not' B) => A) by th43, A1;

      (( 'not' A) => (( 'not' B) => ( 'not' A))) in PL_axioms by withplax;

      then f |- (( 'not' A) => (( 'not' B) => ( 'not' A))) by th42;

      then

       A3: f |- (( 'not' B) => ( 'not' A)) by th43, A2;

      ((( 'not' B) => ( 'not' A)) => ((( 'not' B) => A) => B)) in PL_axioms by withplax;

      then f |- ((( 'not' B) => ( 'not' A)) => ((( 'not' B) => A) => B)) by th42;

      then f |- ((( 'not' B) => A) => B) by th43, A3;

      then f |- B by th43, A4;

      then (F \/ {( 'not' A)}) |- (A => B) by ded;

      hence thesis by ded;

    end;

    theorem :: PL_AXIOM:61

    

     naa: F |- ((( 'not' A) => A) => A)

    proof

      ((( 'not' A) => ( 'not' A)) => ((( 'not' A) => A) => A)) in PL_axioms by withplax;

      then

       A1: F |- ((( 'not' A) => ( 'not' A)) => ((( 'not' A) => A) => A)) by th42;

      F |- (( 'not' A) => ( 'not' A)) by thaa;

      hence thesis by A1, th43;

    end;

    begin

    definition

      let F;

      :: PL_AXIOM:def27

      attr F is consistent means not ex p st (F |- p & F |- ( 'not' p));

    end

    theorem :: PL_AXIOM:62

    

     conco: F is consistent iff ex A st not F |- A

    proof

      hereby

        assume

         A0: F is consistent;

        assume

         A1: for A holds F |- A;

        then

         A2: F |- ( Prop 0 );

        F |- ( 'not' ( Prop 0 )) by A1;

        hence contradiction by A2, A0;

      end;

      assume

       A4: ex A st not F |- A;

      assume not F is consistent;

      then

      consider A such that

       A3: F |- A & F |- ( 'not' A);

      now

        let B;

        F |- (( 'not' A) => (A => B)) by naab;

        then F |- (A => B) by A3, th43;

        hence F |- B by A3, th43;

      end;

      hence contradiction by A4;

    end;

    theorem :: PL_AXIOM:63

    

     th34: not F |- A implies (F \/ {( 'not' A)}) is consistent

    proof

      assume

       Z1: not F |- A;

      assume not (F \/ {( 'not' A)}) is consistent;

      then

       A2: F |- (( 'not' A) => A) by ded, conco;

      F |- ((( 'not' A) => A) => A) by naa;

      hence contradiction by Z1, A2, th43;

    end;

    theorem :: PL_AXIOM:64

    

     exfin: for F, A holds F |- A iff ex G st G c= F & G is finite & G |- A

    proof

      let F, A;

      hereby

        assume F |- A;

        then

        consider f such that

         A1: (f . ( len f)) = A & 1 <= ( len f) & for i be Nat st 1 <= i & i <= ( len f) holds prc (f,F,i);

        deffunc h( Nat) = (f . $1);

        set w2 = { i where i be Element of NAT : 1 <= i & i <= ( len f) };

        set G = { h(i) where i be Element of NAT : i in w2 };

        

         F1: w2 c= ( Seg ( len f))

        proof

          let x be object;

          assume x in w2;

          then

          consider i be Element of NAT such that

           F2: i = x & 1 <= i <= ( len f);

          reconsider i1 = i as Nat;

          thus x in ( Seg ( len f)) by F2;

        end;

        

         A8: w2 is finite by F1;

        

         A4: G c= PL-WFF

        proof

          let x be object;

          assume x in G;

          then

          consider i be Element of NAT such that

           A6: x = h(i) & i in w2;

          consider j be Element of NAT such that

           A9: j = i & 1 <= j & j <= ( len f) by A6;

          i in ( dom f) by FINSEQ_3: 25, A9;

          then

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

          ( rng f) c= PL-WFF by FINSEQ_1:def 4;

          hence x in PL-WFF by A7;

        end;

        G is finite from FRAENKEL:sch 21( A8);

        then

        reconsider G as finite Subset of PL-WFF by A4;

        now

          let i be Nat;

          assume

           A6: 1 <= i <= ( len f);

          then prc (f,F,i) by A1;

          per cases ;

            suppose (f . i) in PL_axioms ;

            hence prc (f,(F /\ G),i);

          end;

            suppose

             A5: (f . i) in F;

            reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

            i1 in w2 by A6;

            then (f . i) in G;

            hence prc (f,(F /\ G),i) by A5, XBOOLE_0:def 4;

          end;

            suppose ex j,k be Nat st 1 <= j & j < i & 1 <= k & k < i & (((f /. j),(f /. k)) MP_rule (f /. i));

            hence prc (f,(F /\ G),i);

          end;

        end;

        then (F /\ G) |- A by A1;

        hence ex G st G c= F & G is finite & G |- A by XBOOLE_1: 17;

      end;

      given G such that

       A1: G c= F & G is finite & G |- A;

      thus F |- A by A1, monmp;

    end;

    theorem :: PL_AXIOM:65

    

     finin: for F st not F is consistent holds ex G st G is finite & not G is consistent & G c= F

    proof

      let F;

      assume not F is consistent;

      then

      consider A such that

       A1: F |- A & F |- ( 'not' A);

      consider G such that

       A2: G c= F & G is finite & G |- A by exfin, A1;

      consider H such that

       A2a: H c= F & H is finite & H |- ( 'not' A) by exfin, A1;

      

       A5: (G \/ H) |- A by A2, monmp, XBOOLE_1: 11;

      (G \/ H) |- ( 'not' A) by A2a, XBOOLE_1: 11, monmp;

      then not (G \/ H) is consistent by A5;

      hence thesis by XBOOLE_1: 8, A2, A2a;

    end;

    definition

      let F;

      :: PL_AXIOM:def28

      attr F is maximal means for p holds (p in F or ( 'not' p) in F);

    end

    theorem :: PL_AXIOM:66

    

     incsub: F c= G & not F is consistent implies not G is consistent

    proof

      assume

       A2: F c= G & not F is consistent;

      then

      consider p such that

       A1: F |- p & F |- ( 'not' p);

      G |- p & G |- ( 'not' p) by monmp, A1, A2;

      hence not G is consistent;

    end;

    theorem :: PL_AXIOM:67

    

     onecon: F is consistent & not (F \/ {A}) is consistent implies (F \/ {( 'not' A)}) is consistent

    proof

      assume

       A1: F is consistent & not (F \/ {A}) is consistent;

      assume not (F \/ {( 'not' A)}) is consistent;

      then

       A2: F |- (( 'not' A) => A) by ded, conco;

      F |- ((( 'not' A) => A) => A) by naa;

      then

       A6: F |- A by A2, th43;

      F |- ( 'not' A) by A1, conco, ded;

      hence contradiction by A6, A1;

    end;

    reserve x,y for set;

    ::$Notion-Name

    theorem :: PL_AXIOM:68

    

     th37: for F st F is consistent holds ex G st F c= G & G is consistent & G is maximal

    proof

      let F;

      assume

       Z0: F is consistent;

      set L = PL-WFF ;

      consider R be Relation such that

       A3: R well_orders L by WELLORD2: 17;

      (R /\ [:L, L:]) c= [:L, L:] by XBOOLE_1: 17;

      then

      reconsider R2 = (R |_2 L) as Relation of L by WELLORD1:def 6;

      R2 well_orders L by A3, PCOMPS_2: 1;

      then

       A76: R2 is_connected_in L by WELLORD1:def 5;

      reconsider RS = RelStr (# L, R2 #) as non empty RelStr;

      set cRS = the carrier of RS;

      defpred H[ object, object, object] means for p holds for f be PartFunc of cRS, ( bool L) st $1 = p & $2 = f holds ((((( union ( rng f qua ( bool L) -valued Relation)) \/ F) \/ {p}) is consistent implies $3 = ((( union ( rng f)) \/ F) \/ {p})) & ( not ((( union ( rng f qua ( bool L) -valued Relation)) \/ F) \/ {p}) is consistent implies $3 = (( union ( rng f)) \/ F)));

      

       A4: for x,y be object st x in cRS & y in ( PFuncs (cRS,( bool L))) holds ex z be object st z in ( bool L) & H[x, y, z]

      proof

        let x,y be object;

        assume

         A6: x in cRS & y in ( PFuncs (cRS,( bool L)));

        reconsider x1 = x as Element of L by A6;

        reconsider y1 = y as PartFunc of cRS, ( bool L) by A6, PARTFUN1: 46;

        per cases ;

          suppose

           A7: ((( union ( rng y1 qua ( bool L) -valued Relation)) \/ F) \/ {x1}) is consistent;

          take ((( union ( rng y1)) \/ F) \/ {x1});

          thus thesis by A7;

        end;

          suppose

           A7a: not ((( union ( rng y1 qua ( bool L) -valued Relation)) \/ F) \/ {x1}) is consistent;

          take (( union ( rng y1)) \/ F);

          thus thesis by A7a;

        end;

      end;

      consider h be Function of [:cRS, ( PFuncs (cRS,( bool L))):], ( bool L) such that

       A9: for x,y be object st x in cRS & y in ( PFuncs (cRS,( bool L))) holds H[x, y, (h . (x,y))] from BINOP_1:sch 1( A4);

      R2 well_orders L by A3, PCOMPS_2: 1;

      then R2 is_well_founded_in L by WELLORD1:def 5;

      then

       A11: RS is well_founded by WELLFND1:def 2;

      then

      consider f be Function of cRS, ( bool L) such that

       A12: f is_recursively_expressed_by h by WELLFND1: 11;

      

       A73: ( dom f) = cRS by FUNCT_2:def 1;

      reconsider G = ( union ( rng f qua ( bool L) -valued Relation)) as Subset of PL-WFF ;

      set iRS = the InternalRel of RS;

      

       F6: ( field R2) = L by A3, PCOMPS_2: 1;

      

       A17: for A, B holds [A, B] in R2 implies (f . A) c= (f . B)

      proof

        let A, B;

        assume

         F3: [A, B] in R2;

        per cases ;

          suppose A = B;

          hence thesis;

        end;

          suppose

           S2: A <> B;

          set frA = (f | (iRS -Seg A));

          set frB = (f | (iRS -Seg B));

          iRS is well-ordering by A3, PCOMPS_2: 1, WELLORD1: 4, F6;

          then

           F12: (iRS -Seg A) c= (iRS -Seg B) by F3, WELLORD1: 29, F6;

          (iRS -Seg B) c= ( field iRS) by WELLORD1: 9;

          then

           F21: frB is Function of (iRS -Seg B), ( bool L) by FUNCT_2: 32, F6;

          (iRS -Seg A) c= ( field iRS) by WELLORD1: 9;

          then frA is Function of (iRS -Seg A), ( bool L) by FUNCT_2: 32, F6;

          then

           F11: ( dom frA) = (iRS -Seg A) by FUNCT_2:def 1;

          

           F13: ( dom frB) = (iRS -Seg B) by FUNCT_2:def 1, F21;

           F18:

          now

            let x;

            assume

             F19: x in ( dom frA);

            

            thus (frA . x) = (f . x) by F19, FUNCT_1: 47

            .= (frB . x) by F13, FUNCT_1: 47, F12, F11, F19;

          end;

          

           E1: ( union ( rng frA)) c= ( union ( rng frB)) by ZFMISC_1: 77, rnginc, F18, F11, F12, F13;

          then

           F7: (( union ( rng frA)) \/ F) c= (( union ( rng frB)) \/ F) by XBOOLE_1: 9;

          

           F15: A in ( dom frB) by F13, S2, F3, WELLORD1: 1;

          (frB . A) = (f . A) by FUNCT_1: 47, F13, S2, F3, WELLORD1: 1;

          then

           F14: (f . A) c= ( union ( rng frB)) by ZFMISC_1: 74, FUNCT_1: 3, F15;

          

           F18: ( dom frA) c= cRS;

          ( rng frA qua ( bool L) -valued Relation) c= ( bool L);

          then

           E4: frA in ( PFuncs (cRS,( bool L))) by PARTFUN1:def 3, F18;

          

           F18a: ( dom frB) c= cRS;

          ( rng frB qua ( bool L) -valued Relation) c= ( bool L);

          then

           E2: frB in ( PFuncs (cRS,( bool L))) by PARTFUN1:def 3, F18a;

          per cases ;

            suppose ((( union ( rng frA qua ( bool L) -valued Relation)) \/ F) \/ {A}) is consistent;

            per cases ;

              suppose

               F2a: ((( union ( rng frB qua ( bool L) -valued Relation)) \/ F) \/ {B}) is consistent;

              

               F16: (f . B) = (h . (B,frB)) by WELLFND1:def 5, A12

              .= ((( union ( rng frB)) \/ F) \/ {B}) by A9, E2, F2a;

              thus (f . A) c= (f . B)

              proof

                let x be object;

                assume x in (f . A);

                then x in (( union ( rng frB)) \/ (F \/ {B})) by XBOOLE_0:def 3, F14;

                hence thesis by F16, XBOOLE_1: 4;

              end;

            end;

              suppose

               F2b: not ((( union ( rng frB qua ( bool L) -valued Relation)) \/ F) \/ {B}) is consistent;

              

               F16b: (f . B) = (h . (B,frB)) by WELLFND1:def 5, A12

              .= (( union ( rng frB)) \/ F) by A9, E2, F2b;

              thus (f . A) c= (f . B) by F16b, XBOOLE_0:def 3, F14;

            end;

          end;

            suppose

             F2: not ((( union ( rng frA qua ( bool L) -valued Relation)) \/ F) \/ {A}) is consistent;

            

             F8: (f . A) = (h . (A,frA)) by WELLFND1:def 5, A12

            .= (( union ( rng frA)) \/ F) by A9, E4, F2;

            per cases ;

              suppose

               F2a: ((( union ( rng frB qua ( bool L) -valued Relation)) \/ F) \/ {B}) is consistent;

              

               F9: (f . B) = (h . (B,frB)) by WELLFND1:def 5, A12

              .= ((( union ( rng frB)) \/ F) \/ {B}) by A9, E2, F2a;

              thus (f . A) c= (f . B) by F8, F9, XBOOLE_1: 10, F7;

            end;

              suppose

               F2b: not ((( union ( rng frB qua ( bool L) -valued Relation)) \/ F) \/ {B}) is consistent;

              (f . B) = (h . (B,frB)) by WELLFND1:def 5, A12

              .= (( union ( rng frB)) \/ F) by A9, E2, F2b;

              hence (f . A) c= (f . B) by F8, XBOOLE_1: 9, E1;

            end;

          end;

        end;

      end;

      

       A54: ( rng f) is c=-linear

      proof

        let x, y;

        assume

         B2: x in ( rng f) & y in ( rng f);

        then

        consider x1 be object such that

         B3: x1 in ( dom f) & (f . x1) = x by FUNCT_1:def 3;

        consider y1 be object such that

         B4: y1 in ( dom f) & (f . y1) = y by FUNCT_1:def 3, B2;

        reconsider x1, y1 as Element of L by B3, B4;

        per cases ;

          suppose x1 = y1;

          hence thesis by B3, B4;

        end;

          suppose

           B1: x1 <> y1;

          per cases by A76, RELAT_2:def 6, B1;

            suppose [x1, y1] in R2;

            then (f . x1) c= (f . y1) by A17;

            hence (x,y) are_c=-comparable by XBOOLE_0:def 9, B3, B4;

          end;

            suppose [y1, x1] in R2;

            then (f . y1) c= (f . x1) by A17;

            hence (x,y) are_c=-comparable by XBOOLE_0:def 9, B3, B4;

          end;

        end;

      end;

      defpred S[ Element of RS] means (f . $1) is consistent;

       A26:

      now

        let x be Element of RS;

        

         A20: (f . x) = (h . (x,(f | (iRS -Seg x)))) by WELLFND1:def 5, A12;

        (f | (iRS -Seg x)) in ( PFuncs (cRS,( bool L))) by PARTFUN1: 45;

        hence H[x, (f | (iRS -Seg x)), (f . x)] by A20, A9;

      end;

       A27:

      now

        let x be Element of RS;

        reconsider x1 = {x} as Subset of L;

        set fr = (f | (iRS -Seg x));

        per cases ;

          suppose ((( union ( rng fr qua ( bool L) -valued Relation)) \/ F) \/ x1) is consistent;

          

          then (f . x) = ((( union ( rng fr)) \/ F) \/ x1) by A26

          .= (F \/ (( union ( rng fr)) \/ x1)) by XBOOLE_1: 4;

          hence F c= (f . x) by XBOOLE_1: 7;

        end;

          suppose not ((( union ( rng fr qua ( bool L) -valued Relation)) \/ F) \/ x1) is consistent;

          then (f . x) = (F \/ ( union ( rng fr))) by A26;

          hence F c= (f . x) by XBOOLE_1: 7;

        end;

      end;

      

       A21: for x be Element of RS st for y be Element of RS st y <> x & [y, x] in iRS holds S[y] holds S[x]

      proof

        let x be Element of RS;

        assume

         A41: for y be Element of RS st y <> x & [y, x] in iRS holds S[y];

        set fr = (f | (iRS -Seg x));

        (iRS -Seg x) c= ( field iRS) by WELLORD1: 9;

        then

         C2: fr is Function of (iRS -Seg x), ( bool L) by FUNCT_2: 32, F6;

        then

         A39a: ( dom fr) = (iRS -Seg x) by FUNCT_2:def 1;

        reconsider x1 = {x} as Subset of L;

        per cases ;

          suppose ((( union ( rng fr qua ( bool L) -valued Relation)) \/ F) \/ x1) is consistent;

          hence S[x] by A26;

        end;

          suppose

           C1: not ((( union ( rng fr qua ( bool L) -valued Relation)) \/ F) \/ x1) is consistent;

          then

           A22: (f . x) = (( union ( rng fr)) \/ F) by A26;

          per cases ;

            suppose

             S4: for y be object holds ( not [y, x] in iRS or y = x);

            (iRS -Seg x) = {}

            proof

              assume (iRS -Seg x) <> {} ;

              then

              consider y be object such that

               F19: y in (iRS -Seg x) by XBOOLE_0: 7;

              y <> x & [y, x] in iRS by WELLORD1: 1, F19;

              hence contradiction by S4;

            end;

            then ( dom fr) = {} by FUNCT_2:def 1, C2;

            then ( rng fr) = {} by RELAT_1: 42;

            hence S[x] by Z0, ZFMISC_1: 2, A26, C1;

          end;

            suppose

             A39: ex y be object st [y, x] in iRS & y <> x;

            assume

             A30: not S[x];

            consider y be object such that

             A29: [y, x] in iRS & y <> x by A39;

            y in ( dom iRS) by A29, XTUPLE_0:def 12;

            then

            reconsider y as Element of RS;

            (fr . y) in ( rng fr) by FUNCT_1: 3, A39a, WELLORD1: 1, A29;

            then

             A37: (f . y) in ( rng fr) by WELLORD1: 1, A29, A39a, FUNCT_1: 47;

            

             A37b: ( rng fr) <> {} by WELLORD1: 1, A29, A39a, FUNCT_1: 3;

            

             A37a: F c= (f . y) by A27;

            F c= ( union ( rng fr)) by TARSKI:def 4, A37, A37a;

            then

             A23: (f . x) = ( union ( rng fr)) by A22, XBOOLE_1: 12;

            consider F such that

             A31: F is finite & not F is consistent & F c= (f . x) by A30, finin;

            ( rng fr) c= ( rng f) by RELAT_1: 70;

            then

            consider z be set such that

             A34: F c= z & z in ( rng fr) by uniolinf, A23, A31, A54, A37b;

            consider y be object such that

             A36: y in ( dom fr) & (fr . y) = z by A34, FUNCT_1:def 3;

            

             A42: [y, x] in iRS by WELLORD1: 1, A39a, A36;

            

             A44: y <> x by WELLORD1: 1, A39a, A36;

            y in ( dom iRS) by A42, XTUPLE_0:def 12;

            then

            reconsider y as Element of RS;

            (f . y) = (fr . y) by A36, FUNCT_1: 47;

            hence contradiction by A36, A34, A31, incsub, A44, A42, A41;

          end;

        end;

      end;

      

       A13a: for A be Element of RS holds S[A] from WELLFND1:sch 3( A21, A11);

      take G;

      thus F c= G

      proof

        let y be object;

        assume

         A46: y in F;

        set z = the Element of RS;

        

         A47: F c= (f . z) by A27;

        (f . z) in ( rng f) by FUNCT_1: 3, A73;

        hence y in G by A46, A47, TARSKI:def 4;

      end;

      thus G is consistent

      proof

        assume not G is consistent;

        then

        consider F such that

         A14: F is finite & not F is consistent & F c= G by finin;

        consider z be set such that

         A90: F c= z & z in ( rng f) by uniolinf, A14, A54, RELAT_1: 42, A73;

        ( rng f qua ( bool L) -valued Relation) c= ( bool L);

        then

        reconsider z as Subset of PL-WFF by A90;

        consider x be object such that

         A92: x in ( dom f) & (f . x) = z by A90, FUNCT_1:def 3;

        thus contradiction by A92, A13a, A90, A14, incsub;

      end;

      thus G is maximal

      proof

        given A such that

         A71: not A in G & not ( 'not' A) in G;

        reconsider ARS = A as Element of RS;

        reconsider nA = ( 'not' A) as Element of RS;

        set fA = (f | (iRS -Seg A));

        set fnA = (f | (iRS -Seg ( 'not' A)));

        reconsider A1 = {A} as Subset of L;

        reconsider A1n = {( 'not' A)} as Subset of L;

        

         A74: not ((( union ( rng fA qua ( bool L) -valued Relation)) \/ F) \/ A1) is consistent

        proof

          assume ((( union ( rng fA qua ( bool L) -valued Relation)) \/ F) \/ A1) is consistent;

          then

           A70: (f . ARS) = ((( union ( rng fA)) \/ F) \/ A1) by A26;

          ARS in A1 by TARSKI:def 1;

          then

           C1: ARS in ((( union ( rng fA)) \/ F) \/ A1) by XBOOLE_0:def 3;

          (f . ARS) in ( rng f) by FUNCT_1: 3, A73;

          hence contradiction by TARSKI:def 4, A71, A70, C1;

        end;

        

         A78: not ((( union ( rng fnA qua ( bool L) -valued Relation)) \/ F) \/ A1n) is consistent

        proof

          assume ((( union ( rng fnA qua ( bool L) -valued Relation)) \/ F) \/ A1n) is consistent;

          then

           A70a: (f . nA) = ((( union ( rng fnA)) \/ F) \/ A1n) by A26;

          nA in A1n by TARSKI:def 1;

          then

           A72a: nA in (f . nA) by A70a, XBOOLE_0:def 3;

          (f . nA) in ( rng f) by FUNCT_1: 3, A73;

          hence contradiction by TARSKI:def 4, A71, A72a;

        end;

        then

         A80: (f . nA) = (( union ( rng fnA)) \/ F) by A26;

        

         A79: (f . A) = (( union ( rng fA)) \/ F) by A26, A74;

        reconsider AAA = A as Element of HP-WFF by plhp;

        reconsider fal = FaLSUM as Element of HP-WFF by plhp;

        (AAA => fal) = (A => FaLSUM );

        then ( len A) <> ( len ( 'not' A)) by HILBERT2: 16;

        per cases by A76, RELAT_2:def 6;

          suppose [A, ( 'not' A)] in R2;

          then (f . A) c= (f . nA) by A17;

          then not ((f . nA) \/ A1) is consistent by A74, incsub, A79, XBOOLE_1: 9;

          hence contradiction by A13a, onecon, A78, A80;

        end;

          suppose [( 'not' A), A] in R2;

          then (f . nA) c= (f . A) by A17;

          then not ((f . ARS) \/ A1n) is consistent by A78, incsub, A80, XBOOLE_1: 9;

          hence contradiction by onecon, A74, A79, A13a;

        end;

      end;

    end;

    theorem :: PL_AXIOM:69

    

     inder: F is maximal & F is consistent implies for p holds F |- p iff p in F

    proof

      assume

       A1: F is maximal & F is consistent;

      let p;

      hereby

        assume

         A2: F |- p;

        assume not p in F;

        then ( 'not' p) in F by A1;

        then F |- ( 'not' p) by th42;

        hence contradiction by A2, A1;

      end;

      assume p in F;

      hence F |- p by th42;

    end;

    theorem :: PL_AXIOM:70

    

     ct: F |= A implies F |- A

    proof

      assume

       A0: F |= A & not F |- A;

      then

      consider G such that

       A1: (F \/ {( 'not' A)}) c= G and

       A1a: G is consistent and

       A1b: G is maximal by th37, th34;

      set M = { ( Prop n) where n be Element of NAT : ( Prop n) in G };

      M c= props

      proof

        let a be object;

        assume a in M;

        then

        consider k such that

         A7: ( Prop k) = a & ( Prop k) in G;

        thus a in props by A7, defprops;

      end;

      then

      reconsider M as PLModel;

      defpred P[ Element of PL-WFF ] means ($1 in G iff M |= $1);

      

       H0: P[ FaLSUM ]

      proof

        hereby

          assume FaLSUM in G;

          then G |- FaLSUM & G |- ( 'not' FaLSUM ) by thaa, th42;

          hence M |= FaLSUM by A1a;

        end;

        assume M |= FaLSUM ;

        hence thesis by Def11;

      end;

      

       H1: for n holds P[( Prop n)]

      proof

        let n;

        hereby

          assume ( Prop n) in G;

          then ( Prop n) in M;

          hence M |= ( Prop n) by Def11;

        end;

        assume M |= ( Prop n);

        then ( Prop n) in M by Def11;

        then

        consider k such that

         A6: ( Prop n) = ( Prop k) & ( Prop k) in G;

        thus ( Prop n) in G by A6;

      end;

      

       H2: for r, s st P[r] & P[s] holds P[(r => s)]

      proof

        let r, s;

        assume

         A10: P[r] & P[s];

        per cases ;

          suppose

           S1: (r => s) in G;

          hereby

            assume

             A11: (r => s) in G;

            per cases ;

              suppose r in G;

              then

               A12: G |- r by th42;

              G |- (r => s) by A11, th42;

              then G |- s by A12, th43;

              then M |= s by A10, inder, A1a, A1b;

              then ((( SAT M) . r) => (( SAT M) . s)) = 1;

              hence M |= (r => s) by Def11;

            end;

              suppose not r in G;

              then not M |= r by A10;

              then (( SAT M) . r) = 0 by XBOOLEAN:def 3;

              then ((( SAT M) . r) => (( SAT M) . s)) = 1;

              hence M |= (r => s) by Def11;

            end;

          end;

          assume M |= (r => s);

          thus (r => s) in G by S1;

        end;

          suppose

           S2: not (r => s) in G;

          thus (r => s) in G implies M |= (r => s) by S2;

          assume

           A14: M |= (r => s);

          ( 'not' (r => s)) in G by S2, A1b;

          then

           A16: G |- ( 'not' (r => s)) by th42;

          now

            assume s in G;

            then

             A17: G |- s by th42;

            (s => (r => s)) in PL_axioms by withplax;

            then G |- (s => (r => s)) by th42;

            then G |- (r => s) by th43, A17;

            hence contradiction by A16, A1a;

          end;

          then

           A13: not M |= s by A10;

          now

            assume ( 'not' r) in G;

            then

             A15: G |- ( 'not' r) by th42;

            G |- (( 'not' r) => (r => s)) by naab;

            then G |- (r => s) by th43, A15;

            hence contradiction by A16, A1a;

          end;

          then M |= r by A10, A1b;

          then not ((( SAT M) . r) => (( SAT M) . s)) = 1 by A13;

          hence (r => s) in G by A14, Def11;

        end;

      end;

      

       A2: for B holds P[B] from PLInd( H0, H1, H2);

      

       A4: F c= G by XBOOLE_1: 11, A1;

      

       A3: M |= F by A4, A2;

       {( 'not' A)} c= G by A1, XBOOLE_1: 11;

      then M |= ( 'not' A) by A2, ZFMISC_1: 31;

      then not M |= A by semnot;

      hence contradiction by A0, A3;

    end;

    theorem :: PL_AXIOM:71

    A is tautology iff ( {} PL-WFF ) |- A by tautsat, sth, ct;