intpro_1.miz



    begin

    definition

      let E be set;

      :: INTPRO_1:def1

      attr E is with_FALSUM means

      : Def1: <* 0 *> in E;

    end

    definition

      let E be set;

      :: INTPRO_1:def2

      attr E is with_int_implication means

      : Def2: for p,q be FinSequence st p in E & q in E holds (( <*1*> ^ p) ^ q) in E;

    end

    definition

      let E be set;

      :: INTPRO_1:def3

      attr E is with_int_conjunction means

      : Def3: for p,q be FinSequence st p in E & q in E holds (( <*2*> ^ p) ^ q) in E;

    end

    definition

      let E be set;

      :: INTPRO_1:def4

      attr E is with_int_disjunction means

      : Def4: for p,q be FinSequence st p in E & q in E holds (( <*3*> ^ p) ^ q) in E;

    end

    definition

      let E be set;

      :: INTPRO_1:def5

      attr E is with_int_propositional_variables means

      : Def5: for n be Element of NAT holds <*(5 + (2 * n))*> in E;

    end

    definition

      let E be set;

      :: INTPRO_1:def6

      attr E is with_modal_operator means

      : Def6: for p be FinSequence st p in E holds ( <*6*> ^ p) in E;

    end

    definition

      let E be set;

      :: INTPRO_1:def7

      attr E is MC-closed means

      : Def7: E c= ( NAT * ) & E is with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator;

    end

    

     Lm1: for E be set st E is MC-closed holds E is non empty

    proof

      let E be set;

      assume E is MC-closed;

      then E is with_FALSUM;

      hence thesis;

    end;

    registration

      cluster MC-closed -> with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator non empty for set;

      coherence by Lm1;

      cluster with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator -> MC-closed for Subset of ( NAT * );

      coherence ;

    end

    definition

      :: INTPRO_1:def8

      func MC-wff -> set means

      : Def8: it is MC-closed & for E be set st E is MC-closed holds it c= E;

      existence

      proof

        

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

        defpred P[ object] means for E be set st E is MC-closed holds $1 in E;

        consider E0 be set such that

         A2: for x be object holds x in E0 iff x in ( NAT * ) & P[x] from XBOOLE_0:sch 1;

        

         A3: for E be set st E is MC-closed holds <* 0 *> in E by Def1;

        then

        reconsider E0 as non empty set by A2, A1;

        take E0;

        

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

        for p be FinSequence st p in E0 holds ( <*6*> ^ p) in E0

        proof

          let p be FinSequence such that

           A5: p in E0;

          p in ( NAT * ) by A2, A5;

          then

          reconsider p9 = p as FinSequence of NAT by FINSEQ_1:def 11;

          

           A6: for E be set st E is MC-closed holds ( <*6*> ^ p) in E

          proof

            let E be set;

            assume

             A7: E is MC-closed;

            then p in E by A2, A5;

            hence thesis by A7, Def6;

          end;

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

          hence thesis by A2, A6;

        end;

        then

         A8: E0 is with_modal_operator;

        for n be Element of NAT holds <*(5 + (2 * n))*> in E0

        proof

          let n be Element of NAT ;

          set p = (5 + (2 * n));

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

          

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

          for E be set st E is MC-closed holds <*p*> in E by Def5;

          hence thesis by A2, A9;

        end;

        then

         A10: E0 is with_int_propositional_variables;

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

        proof

          let p,q be FinSequence such that

           A11: p in E0 and

           A12: q in E0;

          

           A13: q in ( NAT * ) by A2, A12;

          

           A14: for E be set st E is MC-closed holds (( <*3*> ^ p) ^ q) in E

          proof

            let E be set;

            assume

             A15: E is MC-closed;

            then

             A16: q in E by A2, A12;

            p in E by A2, A11, A15;

            hence thesis by A15, A16, Def4;

          end;

          p in ( NAT * ) by A2, A11;

          then

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

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

          hence thesis by A2, A14;

        end;

        then

         A17: E0 is with_int_disjunction;

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

        proof

          let p,q be FinSequence such that

           A18: p in E0 and

           A19: q in E0;

          

           A20: q in ( NAT * ) by A2, A19;

          

           A21: for E be set st E is MC-closed holds (( <*2*> ^ p) ^ q) in E

          proof

            let E be set;

            assume

             A22: E is MC-closed;

            then

             A23: q in E by A2, A19;

            p in E by A2, A18, A22;

            hence thesis by A22, A23, Def3;

          end;

          p in ( NAT * ) by A2, A18;

          then

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

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

          hence thesis by A2, A21;

        end;

        then

         A24: E0 is with_int_conjunction;

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

        proof

          let p,q be FinSequence such that

           A25: p in E0 and

           A26: q in E0;

          

           A27: q in ( NAT * ) by A2, A26;

          

           A28: for E be set st E is MC-closed holds (( <*1*> ^ p) ^ q) in E

          proof

            let E be set;

            assume

             A29: E is MC-closed;

            then

             A30: q in E by A2, A26;

            p in E by A2, A25, A29;

            hence thesis by A29, A30, Def2;

          end;

          p in ( NAT * ) by A2, A25;

          then

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

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

          hence thesis by A2, A28;

        end;

        then

         A31: E0 is with_int_implication;

         <* 0 *> in E0 by A2, A1, A3;

        then E0 is with_FALSUM;

        hence E0 is MC-closed by A4, A10, A31, A24, A17, A8;

        let E be set such that

         A32: E is MC-closed;

        let x be object;

        assume x in E0;

        hence thesis by A2, A32;

      end;

      uniqueness

      proof

        let E1,E2 be set such that

         A33: E1 is MC-closed and

         A34: for E be set st E is MC-closed holds E1 c= E and

         A35: E2 is MC-closed and

         A36: for E be set st E is MC-closed holds E2 c= E;

        

         A37: E2 c= E1 by A33, A36;

        E1 c= E2 by A34, A35;

        hence thesis by A37, XBOOLE_0:def 10;

      end;

    end

    registration

      cluster MC-wff -> MC-closed;

      coherence by Def8;

    end

    registration

      cluster MC-closed non empty for set;

      existence

      proof

        take MC-wff ;

        thus thesis;

      end;

    end

    registration

      cluster MC-wff -> functional;

      coherence

      proof

         MC-wff c= ( NAT * ) by Def7;

        hence thesis;

      end;

    end

    registration

      cluster -> FinSequence-like for Element of MC-wff ;

      coherence

      proof

        let p be Element of MC-wff ;

         MC-wff c= ( NAT * ) by Def7;

        hence thesis;

      end;

    end

    definition

      mode MC-formula is Element of MC-wff ;

    end

    definition

      :: INTPRO_1:def9

      func FALSUM -> MC-formula equals <* 0 *>;

      correctness by Def1;

      let p,q be Element of MC-wff ;

      :: INTPRO_1:def10

      func p => q -> MC-formula equals (( <*1*> ^ p) ^ q);

      correctness by Def2;

      :: INTPRO_1:def11

      func p '&' q -> MC-formula equals (( <*2*> ^ p) ^ q);

      correctness by Def3;

      :: INTPRO_1:def12

      func p 'or' q -> MC-formula equals (( <*3*> ^ p) ^ q);

      correctness by Def4;

    end

    definition

      let p be Element of MC-wff ;

      :: INTPRO_1:def13

      func Nes p -> MC-formula equals ( <*6*> ^ p);

      correctness by Def6;

    end

    reserve T,X,Y for Subset of MC-wff ;

    reserve p,q,r,s for Element of MC-wff ;

    definition

      let T be Subset of MC-wff ;

      :: INTPRO_1:def14

      attr T is IPC_theory means

      : Def14: for p,q,r be Element of MC-wff holds (p => (q => p)) in T & ((p => (q => r)) => ((p => q) => (p => r))) in T & ((p '&' q) => p) in T & ((p '&' q) => q) in T & (p => (q => (p '&' q))) in T & (p => (p 'or' q)) in T & (q => (p 'or' q)) in T & ((p => r) => ((q => r) => ((p 'or' q) => r))) in T & ( FALSUM => p) in T & (p in T & (p => q) in T implies q in T);

      correctness ;

    end

    definition

      let X;

      :: INTPRO_1:def15

      func CnIPC X -> Subset of MC-wff means

      : Def15: r in it iff for T st T is IPC_theory & X c= T holds r in T;

      existence

      proof

        defpred P[ object] means for T st T is IPC_theory & X c= T holds $1 in T;

        consider Y be set such that

         A1: for a be object holds a in Y iff a in MC-wff & P[a] from XBOOLE_0:sch 1;

        Y c= MC-wff by A1;

        then

        reconsider Z = Y as Subset of MC-wff ;

        take Z;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let Y,Z be Subset of MC-wff such that

         A2: r in Y iff for T st T is IPC_theory & X c= T holds r in T and

         A3: r in Z iff for T st T is IPC_theory & X c= T holds r in T;

        for a be object holds a in Y iff a in Z

        proof

          let a be object;

          hereby

            assume

             A4: a in Y;

            then

            reconsider t = a as Element of MC-wff ;

            for T st T is IPC_theory & X c= T holds t in T by A2, A4;

            hence a in Z by A3;

          end;

          assume

           A5: a in Z;

          then

          reconsider t = a as Element of MC-wff ;

          for T st T is IPC_theory & X c= T holds t in T by A3, A5;

          hence thesis by A2;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      :: INTPRO_1:def16

      func IPC-Taut -> Subset of MC-wff equals ( CnIPC ( {} MC-wff ));

      correctness ;

    end

    definition

      let p be Element of MC-wff ;

      :: INTPRO_1:def17

      func neg p -> MC-formula equals (p => FALSUM );

      correctness ;

    end

    definition

      :: INTPRO_1:def18

      func IVERUM -> MC-formula equals ( FALSUM => FALSUM );

      correctness ;

    end

    theorem :: INTPRO_1:1

    

     Th1: (p => (q => p)) in ( CnIPC X)

    proof

      T is IPC_theory & X c= T implies (p => (q => p)) in T;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:2

    

     Th2: ((p => (q => r)) => ((p => q) => (p => r))) in ( CnIPC X)

    proof

      T is IPC_theory & X c= T implies ((p => (q => r)) => ((p => q) => (p => r))) in T;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:3

    

     Th3: ((p '&' q) => p) in ( CnIPC X)

    proof

      T is IPC_theory & X c= T implies ((p '&' q) => p) in T;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:4

    

     Th4: ((p '&' q) => q) in ( CnIPC X)

    proof

      T is IPC_theory & X c= T implies ((p '&' q) => q) in T;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:5

    

     Th5: (p => (q => (p '&' q))) in ( CnIPC X)

    proof

      T is IPC_theory & X c= T implies (p => (q => (p '&' q))) in T;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:6

    

     Th6: (p => (p 'or' q)) in ( CnIPC X)

    proof

      T is IPC_theory & X c= T implies (p => (p 'or' q)) in T;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:7

    

     Th7: (q => (p 'or' q)) in ( CnIPC X)

    proof

      T is IPC_theory & X c= T implies (q => (p 'or' q)) in T;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:8

    

     Th8: ((p => r) => ((q => r) => ((p 'or' q) => r))) in ( CnIPC X)

    proof

      T is IPC_theory & X c= T implies ((p => r) => ((q => r) => ((p 'or' q) => r))) in T;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:9

    

     Th9: ( FALSUM => p) in ( CnIPC X)

    proof

      T is IPC_theory & X c= T implies ( FALSUM => p) in T;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:10

    

     Th10: p in ( CnIPC X) & (p => q) in ( CnIPC X) implies q in ( CnIPC X)

    proof

      assume that

       A1: p in ( CnIPC X) and

       A2: (p => q) in ( CnIPC X);

      T is IPC_theory & X c= T implies q in T

      proof

        assume that

         A3: T is IPC_theory and

         A4: X c= T;

        

         A5: (p => q) in T by A2, A3, A4, Def15;

        p in T by A1, A3, A4, Def15;

        hence thesis by A3, A5;

      end;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:11

    

     Th11: T is IPC_theory & X c= T implies ( CnIPC X) c= T by Def15;

    theorem :: INTPRO_1:12

    

     Th12: X c= ( CnIPC X)

    proof

      let a be object;

      assume

       A1: a in X;

      then

      reconsider t = a as Element of MC-wff ;

      for T st T is IPC_theory & X c= T holds t in T by A1;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:13

    

     Th13: X c= Y implies ( CnIPC X) c= ( CnIPC Y)

    proof

      assume

       A1: X c= Y;

      thus ( CnIPC X) c= ( CnIPC Y)

      proof

        let a be object;

        assume

         A2: a in ( CnIPC X);

        then

        reconsider t = a as Element of MC-wff ;

        for T st T is IPC_theory & Y c= T holds t in T

        proof

          let T such that

           A3: T is IPC_theory and

           A4: Y c= T;

          X c= T by A1, A4;

          hence thesis by A2, A3, Def15;

        end;

        hence thesis by Def15;

      end;

    end;

    

     Lm2: ( CnIPC ( CnIPC X)) c= ( CnIPC X)

    proof

      let a be object;

      assume

       A1: a in ( CnIPC ( CnIPC X));

      then

      reconsider t = a as Element of MC-wff ;

      for T st T is IPC_theory & X c= T holds t in T

      proof

        let T;

        assume that

         A2: T is IPC_theory and

         A3: X c= T;

        ( CnIPC X) c= T by A2, A3, Th11;

        hence thesis by A1, A2, Def15;

      end;

      hence thesis by Def15;

    end;

    theorem :: INTPRO_1:14

    ( CnIPC ( CnIPC X)) = ( CnIPC X)

    proof

      

       A1: ( CnIPC X) c= ( CnIPC ( CnIPC X)) by Th12;

      ( CnIPC ( CnIPC X)) c= ( CnIPC X) by Lm2;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    

     Lm3: ( CnIPC X) is IPC_theory by Th1, Th2, Th3, Th4, Th5, Th6, Th7, Th8, Th9, Th10;

    registration

      let X be Subset of MC-wff ;

      cluster ( CnIPC X) -> IPC_theory;

      coherence by Lm3;

    end

    theorem :: INTPRO_1:15

    

     Th15: T is IPC_theory iff ( CnIPC T) = T

    proof

      hereby

        assume

         A1: T is IPC_theory;

        

         A2: ( CnIPC T) c= T by A1, Def15;

        T c= ( CnIPC T) by Th12;

        hence ( CnIPC T) = T by A2, XBOOLE_0:def 10;

      end;

      thus thesis;

    end;

    theorem :: INTPRO_1:16

    T is IPC_theory implies IPC-Taut c= T

    proof

      assume

       A1: T is IPC_theory;

       IPC-Taut c= ( CnIPC T) by Th13, XBOOLE_1: 2;

      hence thesis by A1, Th15;

    end;

    registration

      cluster IPC-Taut -> IPC_theory;

      coherence ;

    end

    begin

    theorem :: INTPRO_1:17

    

     Th17: (p => p) in IPC-Taut

    proof

      

       A1: (p => (p => p)) in IPC-Taut by Def14;

      

       A2: (p => ((p => p) => p)) in IPC-Taut by Def14;

      ((p => ((p => p) => p)) => ((p => (p => p)) => (p => p))) in IPC-Taut by Def14;

      then ((p => (p => p)) => (p => p)) in IPC-Taut by A2, Def14;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:18

    

     Th18: q in IPC-Taut implies (p => q) in IPC-Taut

    proof

      (q => (p => q)) in IPC-Taut by Def14;

      hence thesis by Def14;

    end;

    theorem :: INTPRO_1:19

     IVERUM in IPC-Taut by Def14;

    theorem :: INTPRO_1:20

    ((p => q) => (p => p)) in IPC-Taut by Th17, Th18;

    theorem :: INTPRO_1:21

    ((q => p) => (p => p)) in IPC-Taut by Th17, Th18;

    theorem :: INTPRO_1:22

    

     Th22: ((q => r) => ((p => q) => (p => r))) in IPC-Taut

    proof

      

       A1: ((p => (q => r)) => ((p => q) => (p => r))) in IPC-Taut by Def14;

      

       A2: (((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) => (((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r))))) in IPC-Taut by Def14;

      (((p => (q => r)) => ((p => q) => (p => r))) => ((q => r) => ((p => (q => r)) => ((p => q) => (p => r))))) in IPC-Taut by Def14;

      then ((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut by A1, Def14;

      then

       A3: (((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r)))) in IPC-Taut by A2, Def14;

      ((q => r) => (p => (q => r))) in IPC-Taut by Def14;

      hence thesis by A3, Def14;

    end;

    theorem :: INTPRO_1:23

    

     Th23: (p => (q => r)) in IPC-Taut implies (q => (p => r)) in IPC-Taut

    proof

      assume

       A1: (p => (q => r)) in IPC-Taut ;

      

       A2: (((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r)))) in IPC-Taut by Th22;

      ((p => (q => r)) => ((p => q) => (p => r))) in IPC-Taut by Def14;

      then ((p => q) => (p => r)) in IPC-Taut by A1, Def14;

      then

       A3: ((q => (p => q)) => (q => (p => r))) in IPC-Taut by A2, Def14;

      (q => (p => q)) in IPC-Taut by Def14;

      hence thesis by A3, Def14;

    end;

    theorem :: INTPRO_1:24

    

     Th24: ((p => q) => ((q => r) => (p => r))) in IPC-Taut

    proof

      ((q => r) => ((p => q) => (p => r))) in IPC-Taut by Th22;

      hence thesis by Th23;

    end;

    theorem :: INTPRO_1:25

    

     Th25: (p => q) in IPC-Taut implies ((q => r) => (p => r)) in IPC-Taut

    proof

      assume

       A1: (p => q) in IPC-Taut ;

      ((p => q) => ((q => r) => (p => r))) in IPC-Taut by Th24;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:26

    

     Th26: (p => q) in IPC-Taut & (q => r) in IPC-Taut implies (p => r) in IPC-Taut

    proof

      assume that

       A1: (p => q) in IPC-Taut and

       A2: (q => r) in IPC-Taut ;

      ((p => q) => ((q => r) => (p => r))) in IPC-Taut by Th24;

      then ((q => r) => (p => r)) in IPC-Taut by A1, Def14;

      hence thesis by A2, Def14;

    end;

    

     Lm4: ((((q => r) => (p => r)) => s) => ((p => q) => s)) in IPC-Taut

    proof

      ((p => q) => ((q => r) => (p => r))) in IPC-Taut by Th24;

      hence thesis by Th25;

    end;

    theorem :: INTPRO_1:27

    

     Th27: ((p => (q => r)) => ((s => q) => (p => (s => r)))) in IPC-Taut

    proof

      

       A1: ((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) in IPC-Taut by Lm4;

      (((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) => ((p => (q => r)) => ((s => q) => (p => (s => r))))) in IPC-Taut by Lm4;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:28

    (((p => q) => r) => (q => r)) in IPC-Taut

    proof

      

       A1: ((q => (p => q)) => (((p => q) => r) => (q => r))) in IPC-Taut by Th24;

      (q => (p => q)) in IPC-Taut by Def14;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:29

    

     Th29: ((p => (q => r)) => (q => (p => r))) in IPC-Taut

    proof

      

       A1: (q => (p => q)) in IPC-Taut by Def14;

      ((p => (q => r)) => ((p => q) => (p => r))) in IPC-Taut by Def14;

      then

       A2: ((p => q) => ((p => (q => r)) => (p => r))) in IPC-Taut by Th23;

      (((p => q) => ((p => (q => r)) => (p => r))) => ((q => (p => q)) => (q => ((p => (q => r)) => (p => r))))) in IPC-Taut by Th22;

      then ((q => (p => q)) => (q => ((p => (q => r)) => (p => r)))) in IPC-Taut by A2, Def14;

      then (q => ((p => (q => r)) => (p => r))) in IPC-Taut by A1, Def14;

      hence thesis by Th23;

    end;

    theorem :: INTPRO_1:30

    

     Th30: ((p => (p => q)) => (p => q)) in IPC-Taut

    proof

      ((p => (p => q)) => ((p => p) => (p => q))) in IPC-Taut by Def14;

      then

       A1: ((p => p) => ((p => (p => q)) => (p => q))) in IPC-Taut by Th23;

      (p => p) in IPC-Taut by Th17;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:31

    (q => ((q => p) => p)) in IPC-Taut

    proof

      

       A1: (((q => p) => (q => p)) => (q => ((q => p) => p))) in IPC-Taut by Th29;

      ((q => p) => (q => p)) in IPC-Taut by Th17;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:32

    

     Th32: (s => (q => p)) in IPC-Taut & q in IPC-Taut implies (s => p) in IPC-Taut

    proof

      assume that

       A1: (s => (q => p)) in IPC-Taut and

       A2: q in IPC-Taut ;

      ((s => (q => p)) => (q => (s => p))) in IPC-Taut by Th29;

      then (q => (s => p)) in IPC-Taut by A1, Def14;

      hence thesis by A2, Def14;

    end;

    begin

    theorem :: INTPRO_1:33

    

     Th33: (p => (p '&' p)) in IPC-Taut

    proof

      

       A1: ((p => (p => (p '&' p))) => (p => (p '&' p))) in IPC-Taut by Th30;

      (p => (p => (p '&' p))) in IPC-Taut by Def14;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:34

    

     Th34: (p '&' q) in IPC-Taut iff p in IPC-Taut & q in IPC-Taut

    proof

      hereby

        

         A1: ((p '&' q) => q) in IPC-Taut by Def14;

        assume

         A2: (p '&' q) in IPC-Taut ;

        ((p '&' q) => p) in IPC-Taut by Def14;

        hence p in IPC-Taut & q in IPC-Taut by A2, A1, Def14;

      end;

      assume that

       A3: p in IPC-Taut and

       A4: q in IPC-Taut ;

      (p => (q => (p '&' q))) in IPC-Taut by Def14;

      then (q => (p '&' q)) in IPC-Taut by A3, Def14;

      hence thesis by A4, Def14;

    end;

    theorem :: INTPRO_1:35

    (p '&' q) in IPC-Taut iff (q '&' p) in IPC-Taut

    proof

      hereby

        assume

         A1: (p '&' q) in IPC-Taut ;

        then

         A2: q in IPC-Taut by Th34;

        p in IPC-Taut by A1, Th34;

        hence (q '&' p) in IPC-Taut by A2, Th34;

      end;

      assume

       A3: (q '&' p) in IPC-Taut ;

      then

       A4: p in IPC-Taut by Th34;

      q in IPC-Taut by A3, Th34;

      hence thesis by A4, Th34;

    end;

    theorem :: INTPRO_1:36

    

     Th36: (((p '&' q) => r) => (p => (q => r))) in IPC-Taut

    proof

      set qp = (q => (p '&' q));

      set pr = (((p '&' q) => r) => (q => r));

      

       A1: ((p => (qp => pr)) => ((p => qp) => (p => pr))) in IPC-Taut by Def14;

      

       A2: (p => (q => (p '&' q))) in IPC-Taut by Def14;

      (p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r)))) in IPC-Taut by Th18, Th24;

      then ((p => qp) => (p => pr)) in IPC-Taut by A1, Def14;

      then

       A3: (p => (((p '&' q) => r) => (q => r))) in IPC-Taut by A2, Def14;

      ((p => (((p '&' q) => r) => (q => r))) => (((p '&' q) => r) => (p => (q => r)))) in IPC-Taut by Th29;

      hence thesis by A3, Def14;

    end;

    theorem :: INTPRO_1:37

    

     Th37: ((p => (q => r)) => ((p '&' q) => r)) in IPC-Taut

    proof

      

       A1: (((p '&' q) => q) => ((q => r) => ((p '&' q) => r))) in IPC-Taut by Th24;

      ((p '&' q) => q) in IPC-Taut by Def14;

      then ((q => r) => ((p '&' q) => r)) in IPC-Taut by A1, Def14;

      then

       A2: (p => ((q => r) => ((p '&' q) => r))) in IPC-Taut by Th18;

      

       A3: ((p => ((p '&' q) => r)) => ((p '&' q) => (p => r))) in IPC-Taut by Th29;

      ((p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r)))) in IPC-Taut by Def14;

      then ((p => (q => r)) => (p => ((p '&' q) => r))) in IPC-Taut by A2, Def14;

      then

       A4: ((p => (q => r)) => ((p '&' q) => (p => r))) in IPC-Taut by A3, Th26;

      

       A5: ((p '&' q) => p) in IPC-Taut by Def14;

      (((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r))) in IPC-Taut by Def14;

      then (((p '&' q) => (p => r)) => ((p '&' q) => r)) in IPC-Taut by A5, Th32;

      hence thesis by A4, Th26;

    end;

    theorem :: INTPRO_1:38

    

     Th38: ((r => p) => ((r => q) => (r => (p '&' q)))) in IPC-Taut

    proof

      

       A1: ((r => (q => (p '&' q))) => ((r => q) => (r => (p '&' q)))) in IPC-Taut by Def14;

      (p => (q => (p '&' q))) in IPC-Taut by Def14;

      then

       A2: (r => (p => (q => (p '&' q)))) in IPC-Taut by Th18;

      ((r => (p => (q => (p '&' q)))) => ((r => p) => (r => (q => (p '&' q))))) in IPC-Taut by Def14;

      then ((r => p) => (r => (q => (p '&' q)))) in IPC-Taut by A2, Def14;

      hence thesis by A1, Th26;

    end;

    theorem :: INTPRO_1:39

    

     Th39: (((p => q) '&' p) => q) in IPC-Taut

    proof

      set P = (p => q);

      

       A1: (P => P) in IPC-Taut by Th17;

      ((P => P) => ((P '&' p) => q)) in IPC-Taut by Th37;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:40

    ((((p => q) '&' p) '&' s) => q) in IPC-Taut

    proof

      set P = ((p => q) '&' p);

      

       A1: (P => q) in IPC-Taut by Th39;

      ((P '&' s) => P) in IPC-Taut by Def14;

      hence thesis by A1, Th26;

    end;

    theorem :: INTPRO_1:41

    ((q => s) => ((p '&' q) => s)) in IPC-Taut

    proof

      set P = (p '&' q);

      

       A1: (P => q) in IPC-Taut by Def14;

      ((P => q) => ((q => s) => (P => s))) in IPC-Taut by Th24;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:42

    

     Th42: ((q => s) => ((q '&' p) => s)) in IPC-Taut

    proof

      set P = (q '&' p);

      

       A1: (P => q) in IPC-Taut by Def14;

      ((P => q) => ((q => s) => (P => s))) in IPC-Taut by Th24;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:43

    

     Th43: (((p '&' s) => q) => ((p '&' s) => (q '&' s))) in IPC-Taut

    proof

      set P = (p '&' s);

      

       A1: ((P => q) => ((P => s) => (P => (q '&' s)))) in IPC-Taut by Th38;

      (P => s) in IPC-Taut by Def14;

      hence thesis by A1, Th32;

    end;

    theorem :: INTPRO_1:44

    

     Th44: ((p => q) => ((p '&' s) => (q '&' s))) in IPC-Taut

    proof

      

       A1: (((p '&' s) => q) => ((p '&' s) => (q '&' s))) in IPC-Taut by Th43;

      ((p => q) => ((p '&' s) => q)) in IPC-Taut by Th42;

      hence thesis by A1, Th26;

    end;

    theorem :: INTPRO_1:45

    

     Th45: (((p => q) '&' (p '&' s)) => (q '&' s)) in IPC-Taut

    proof

      set P = (p => q), Q = (p '&' s), S = (q '&' s);

      

       A1: (P => (Q => S)) in IPC-Taut by Th44;

      ((P => (Q => S)) => ((P '&' Q) => S)) in IPC-Taut by Th37;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:46

    

     Th46: ((p '&' q) => (q '&' p)) in IPC-Taut

    proof

      set P = (p '&' q);

      

       A1: (P => q) in IPC-Taut by Def14;

      

       A2: (P => p) in IPC-Taut by Def14;

      ((P => q) => ((P => p) => (P => (q '&' p)))) in IPC-Taut by Th38;

      then ((P => p) => (P => (q '&' p))) in IPC-Taut by A1, Def14;

      hence thesis by A2, Def14;

    end;

    theorem :: INTPRO_1:47

    

     Th47: (((p => q) '&' (p '&' s)) => (s '&' q)) in IPC-Taut

    proof

      

       A1: ((q '&' s) => (s '&' q)) in IPC-Taut by Th46;

      (((p => q) '&' (p '&' s)) => (q '&' s)) in IPC-Taut by Th45;

      hence thesis by A1, Th26;

    end;

    theorem :: INTPRO_1:48

    

     Th48: ((p => q) => ((p '&' s) => (s '&' q))) in IPC-Taut

    proof

      set P = (p => q), Q = (p '&' s), S = (s '&' q);

      

       A1: ((P '&' Q) => S) in IPC-Taut by Th47;

      (((P '&' Q) => S) => (P => (Q => S))) in IPC-Taut by Th36;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:49

    

     Th49: ((p => q) => ((s '&' p) => (s '&' q))) in IPC-Taut

    proof

      set P = (p => q), Q = (p '&' s), S = (s '&' q), T = (s '&' p);

      

       A1: (P => (Q => S)) in IPC-Taut by Th48;

      

       A2: (T => Q) in IPC-Taut by Th46;

      ((P => (Q => S)) => ((T => Q) => (P => (T => S)))) in IPC-Taut by Th27;

      then ((T => Q) => (P => (T => S))) in IPC-Taut by A1, Def14;

      hence thesis by A2, Def14;

    end;

    theorem :: INTPRO_1:50

    ((p '&' (s '&' q)) => (p '&' (q '&' s))) in IPC-Taut

    proof

      set P = (s '&' q), Q = (q '&' s);

      

       A1: (P => Q) in IPC-Taut by Th46;

      ((P => Q) => ((p '&' P) => (p '&' Q))) in IPC-Taut by Th49;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:51

    (((p => q) '&' (p => s)) => (p => (q '&' s))) in IPC-Taut

    proof

      set P = (p => q), Q = (p => s), S = (p => (q '&' s));

      

       A1: (P => (Q => S)) in IPC-Taut by Th38;

      ((P => (Q => S)) => ((P '&' Q) => S)) in IPC-Taut by Th37;

      hence thesis by A1, Def14;

    end;

    

     Lm5: (((p '&' q) '&' s) => q) in IPC-Taut

    proof

      

       A1: ((p '&' q) => q) in IPC-Taut by Def14;

      (((p '&' q) '&' s) => (p '&' q)) in IPC-Taut by Def14;

      hence thesis by A1, Th26;

    end;

    

     Lm6: ((((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q)) in IPC-Taut

    proof

      set P = ((p '&' q) '&' s);

      

       A1: (P => q) in IPC-Taut by Lm5;

      ((P => q) => ((P '&' P) => (P '&' q))) in IPC-Taut by Th49;

      hence thesis by A1, Def14;

    end;

    

     Lm7: (((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q)) in IPC-Taut

    proof

      

       A1: ((((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q)) in IPC-Taut by Lm6;

      (((p '&' q) '&' s) => (((p '&' q) '&' s) '&' ((p '&' q) '&' s))) in IPC-Taut by Th33;

      hence thesis by A1, Th26;

    end;

    

     Lm8: (((p '&' q) '&' s) => (p '&' s)) in IPC-Taut

    proof

      set P = (p '&' q);

      

       A1: (P => p) in IPC-Taut by Def14;

      ((P => p) => ((P '&' s) => (p '&' s))) in IPC-Taut by Th44;

      hence thesis by A1, Def14;

    end;

    

     Lm9: ((((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q)) in IPC-Taut

    proof

      set P = ((p '&' q) '&' s), Q = (p '&' s);

      

       A1: (P => Q) in IPC-Taut by Lm8;

      ((P => Q) => ((P '&' q) => (Q '&' q))) in IPC-Taut by Th44;

      hence thesis by A1, Def14;

    end;

    

     Lm10: (((p '&' q) '&' s) => ((p '&' s) '&' q)) in IPC-Taut

    proof

      

       A1: ((((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q)) in IPC-Taut by Lm9;

      (((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q)) in IPC-Taut by Lm7;

      hence thesis by A1, Th26;

    end;

    

     Lm11: (((p '&' s) '&' q) => ((s '&' p) '&' q)) in IPC-Taut

    proof

      set P = (p '&' s), Q = (s '&' p);

      

       A1: (P => Q) in IPC-Taut by Th46;

      ((P => Q) => ((P '&' q) => (Q '&' q))) in IPC-Taut by Th44;

      hence thesis by A1, Def14;

    end;

    

     Lm12: (((p '&' q) '&' s) => ((s '&' p) '&' q)) in IPC-Taut

    proof

      

       A1: (((p '&' s) '&' q) => ((s '&' p) '&' q)) in IPC-Taut by Lm11;

      (((p '&' q) '&' s) => ((p '&' s) '&' q)) in IPC-Taut by Lm10;

      hence thesis by A1, Th26;

    end;

    

     Lm13: (((p '&' q) '&' s) => ((s '&' q) '&' p)) in IPC-Taut

    proof

      

       A1: (((s '&' p) '&' q) => ((s '&' q) '&' p)) in IPC-Taut by Lm10;

      (((p '&' q) '&' s) => ((s '&' p) '&' q)) in IPC-Taut by Lm12;

      hence thesis by A1, Th26;

    end;

    

     Lm14: (((p '&' q) '&' s) => (p '&' (s '&' q))) in IPC-Taut

    proof

      

       A1: (((s '&' q) '&' p) => (p '&' (s '&' q))) in IPC-Taut by Th46;

      (((p '&' q) '&' s) => ((s '&' q) '&' p)) in IPC-Taut by Lm13;

      hence thesis by A1, Th26;

    end;

    

     Lm15: ((p '&' (s '&' q)) => (p '&' (q '&' s))) in IPC-Taut

    proof

      set P = (s '&' q), Q = (q '&' s);

      

       A1: ((s '&' q) => (q '&' s)) in IPC-Taut by Th46;

      ((P => Q) => ((p '&' P) => (p '&' Q))) in IPC-Taut by Th49;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:52

    (((p '&' q) '&' s) => (p '&' (q '&' s))) in IPC-Taut

    proof

      

       A1: ((p '&' (s '&' q)) => (p '&' (q '&' s))) in IPC-Taut by Lm15;

      (((p '&' q) '&' s) => (p '&' (s '&' q))) in IPC-Taut by Lm14;

      hence thesis by A1, Th26;

    end;

    

     Lm16: ((p '&' (q '&' s)) => ((s '&' q) '&' p)) in IPC-Taut

    proof

      

       A1: ((p '&' (s '&' q)) => ((s '&' q) '&' p)) in IPC-Taut by Th46;

      ((p '&' (q '&' s)) => (p '&' (s '&' q))) in IPC-Taut by Lm15;

      hence thesis by A1, Th26;

    end;

    

     Lm17: (((s '&' q) '&' p) => ((q '&' s) '&' p)) in IPC-Taut

    proof

      set P = (s '&' q), Q = (q '&' s);

      

       A1: ((s '&' q) => (q '&' s)) in IPC-Taut by Th46;

      ((P => Q) => ((P '&' p) => (Q '&' p))) in IPC-Taut by Th44;

      hence thesis by A1, Def14;

    end;

    

     Lm18: ((p '&' (q '&' s)) => ((q '&' s) '&' p)) in IPC-Taut

    proof

      

       A1: (((s '&' q) '&' p) => ((q '&' s) '&' p)) in IPC-Taut by Lm17;

      ((p '&' (q '&' s)) => ((s '&' q) '&' p)) in IPC-Taut by Lm16;

      hence thesis by A1, Th26;

    end;

    

     Lm19: ((p '&' (q '&' s)) => ((p '&' s) '&' q)) in IPC-Taut

    proof

      

       A1: (((q '&' s) '&' p) => ((p '&' s) '&' q)) in IPC-Taut by Lm13;

      ((p '&' (q '&' s)) => ((q '&' s) '&' p)) in IPC-Taut by Lm18;

      hence thesis by A1, Th26;

    end;

    

     Lm20: ((p '&' (q '&' s)) => (p '&' (s '&' q))) in IPC-Taut

    proof

      set P = (q '&' s), Q = (s '&' q);

      

       A1: ((q '&' s) => (s '&' q)) in IPC-Taut by Th46;

      ((P => Q) => ((p '&' P) => (p '&' Q))) in IPC-Taut by Th49;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:53

    ((p '&' (q '&' s)) => ((p '&' q) '&' s)) in IPC-Taut

    proof

      

       A1: ((p '&' (s '&' q)) => ((p '&' q) '&' s)) in IPC-Taut by Lm19;

      ((p '&' (q '&' s)) => (p '&' (s '&' q))) in IPC-Taut by Lm20;

      hence thesis by A1, Th26;

    end;

    begin

    theorem :: INTPRO_1:54

    

     Th54: ((p 'or' p) => p) in IPC-Taut

    proof

      

       A1: (p => p) in IPC-Taut by Th17;

      ((p => p) => ((p => p) => ((p 'or' p) => p))) in IPC-Taut by Def14;

      then ((p => p) => ((p 'or' p) => p)) in IPC-Taut by A1, Def14;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:55

    p in IPC-Taut or q in IPC-Taut implies (p 'or' q) in IPC-Taut

    proof

      assume

       A1: p in IPC-Taut or q in IPC-Taut ;

      now

        per cases by A1;

          case

           A2: p in IPC-Taut ;

          (p => (p 'or' q)) in IPC-Taut by Def14;

          hence thesis by A2, Def14;

        end;

          case

           A3: q in IPC-Taut ;

          (q => (p 'or' q)) in IPC-Taut by Def14;

          hence thesis by A3, Def14;

        end;

      end;

      hence thesis;

    end;

    theorem :: INTPRO_1:56

    

     Th56: ((p 'or' q) => (q 'or' p)) in IPC-Taut

    proof

      

       A1: (p => (q 'or' p)) in IPC-Taut by Def14;

      

       A2: (q => (q 'or' p)) in IPC-Taut by Def14;

      ((p => (q 'or' p)) => ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p)))) in IPC-Taut by Def14;

      then ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p))) in IPC-Taut by A1, Def14;

      hence thesis by A2, Def14;

    end;

    theorem :: INTPRO_1:57

    (p 'or' q) in IPC-Taut iff (q 'or' p) in IPC-Taut

    proof

      hereby

        assume

         A1: (p 'or' q) in IPC-Taut ;

        ((p 'or' q) => (q 'or' p)) in IPC-Taut by Th56;

        hence (q 'or' p) in IPC-Taut by A1, Def14;

      end;

      assume

       A2: (q 'or' p) in IPC-Taut ;

      ((q 'or' p) => (p 'or' q)) in IPC-Taut by Th56;

      hence thesis by A2, Def14;

    end;

    theorem :: INTPRO_1:58

    

     Th58: ((p => q) => (p => (q 'or' s))) in IPC-Taut

    proof

      

       A1: ((q => (q 'or' s)) => ((p => q) => (p => (q 'or' s)))) in IPC-Taut by Th22;

      (q => (q 'or' s)) in IPC-Taut by Def14;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:59

    

     Th59: ((p => q) => (p => (s 'or' q))) in IPC-Taut

    proof

      

       A1: ((q => (s 'or' q)) => ((p => q) => (p => (s 'or' q)))) in IPC-Taut by Th22;

      (q => (s 'or' q)) in IPC-Taut by Def14;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:60

    

     Th60: ((p => q) => ((p 'or' s) => (q 'or' s))) in IPC-Taut

    proof

      set P = (p 'or' s), Q = (q 'or' s);

      

       A1: ((p => q) => (p => Q)) in IPC-Taut by Th58;

      ((p => Q) => ((s => Q) => (P => Q))) in IPC-Taut by Def14;

      then

       A2: ((s => Q) => ((p => Q) => (P => Q))) in IPC-Taut by Th23;

      (s => Q) in IPC-Taut by Def14;

      then ((p => Q) => (P => Q)) in IPC-Taut by A2, Def14;

      hence thesis by A1, Th26;

    end;

    theorem :: INTPRO_1:61

    

     Th61: (p => q) in IPC-Taut implies ((p 'or' s) => (q 'or' s)) in IPC-Taut

    proof

      assume

       A1: (p => q) in IPC-Taut ;

      ((p => q) => ((p 'or' s) => (q 'or' s))) in IPC-Taut by Th60;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:62

    

     Th62: ((p => q) => ((s 'or' p) => (s 'or' q))) in IPC-Taut

    proof

      set P = (s 'or' p), Q = (s 'or' q);

      

       A1: (s => Q) in IPC-Taut by Def14;

      

       A2: ((p => q) => (p => Q)) in IPC-Taut by Th59;

      ((s => Q) => ((p => Q) => (P => Q))) in IPC-Taut by Def14;

      then ((p => Q) => (P => Q)) in IPC-Taut by A1, Def14;

      hence thesis by A2, Th26;

    end;

    theorem :: INTPRO_1:63

    

     Th63: (p => q) in IPC-Taut implies ((s 'or' p) => (s 'or' q)) in IPC-Taut

    proof

      assume

       A1: (p => q) in IPC-Taut ;

      ((p => q) => ((s 'or' p) => (s 'or' q))) in IPC-Taut by Th62;

      hence thesis by A1, Def14;

    end;

    theorem :: INTPRO_1:64

    

     Th64: ((p 'or' (q 'or' s)) => (q 'or' (p 'or' s))) in IPC-Taut

    proof

      set P = (p 'or' s), Q = (q 'or' s);

      

       A1: (P => (q 'or' P)) in IPC-Taut by Def14;

      (p => P) in IPC-Taut by Def14;

      then (p => (q 'or' P)) in IPC-Taut by A1, Th26;

      then

       A2: (((q 'or' P) 'or' p) => ((q 'or' P) 'or' (q 'or' P))) in IPC-Taut by Th63;

      (((q 'or' P) 'or' (q 'or' P)) => (q 'or' P)) in IPC-Taut by Th54;

      then

       A3: (((q 'or' P) 'or' p) => (q 'or' P)) in IPC-Taut by A2, Th26;

      (s => P) in IPC-Taut by Def14;

      then ((q 'or' s) => (q 'or' P)) in IPC-Taut by Th63;

      then

       A4: ((p 'or' Q) => (p 'or' (q 'or' P))) in IPC-Taut by Th63;

      ((p 'or' (q 'or' P)) => ((q 'or' P) 'or' p)) in IPC-Taut by Th56;

      then ((p 'or' Q) => ((q 'or' P) 'or' p)) in IPC-Taut by A4, Th26;

      hence thesis by A3, Th26;

    end;

    theorem :: INTPRO_1:65

    ((p 'or' (q 'or' s)) => ((p 'or' q) 'or' s)) in IPC-Taut

    proof

      

       A1: ((s 'or' (p 'or' q)) => ((p 'or' q) 'or' s)) in IPC-Taut by Th56;

      ((q 'or' s) => (s 'or' q)) in IPC-Taut by Th56;

      then

       A2: ((p 'or' (q 'or' s)) => (p 'or' (s 'or' q))) in IPC-Taut by Th63;

      ((p 'or' (s 'or' q)) => (s 'or' (p 'or' q))) in IPC-Taut by Th64;

      then ((p 'or' (q 'or' s)) => (s 'or' (p 'or' q))) in IPC-Taut by A2, Th26;

      hence thesis by A1, Th26;

    end;

    theorem :: INTPRO_1:66

    (((p 'or' q) 'or' s) => (p 'or' (q 'or' s))) in IPC-Taut

    proof

      ((p 'or' q) => (q 'or' p)) in IPC-Taut by Th56;

      then

       A1: (((p 'or' q) 'or' s) => ((q 'or' p) 'or' s)) in IPC-Taut by Th61;

      ((q 'or' p) => (p 'or' q)) in IPC-Taut by Th56;

      then

       A2: ((s 'or' (q 'or' p)) => (s 'or' (p 'or' q))) in IPC-Taut by Th63;

      (((q 'or' p) 'or' s) => (s 'or' (q 'or' p))) in IPC-Taut by Th56;

      then (((p 'or' q) 'or' s) => (s 'or' (q 'or' p))) in IPC-Taut by A1, Th26;

      then

       A3: (((p 'or' q) 'or' s) => (s 'or' (p 'or' q))) in IPC-Taut by A2, Th26;

      ((s 'or' q) => (q 'or' s)) in IPC-Taut by Th56;

      then

       A4: ((p 'or' (s 'or' q)) => (p 'or' (q 'or' s))) in IPC-Taut by Th63;

      ((s 'or' (p 'or' q)) => (p 'or' (s 'or' q))) in IPC-Taut by Th64;

      then (((p 'or' q) 'or' s) => (p 'or' (s 'or' q))) in IPC-Taut by A3, Th26;

      hence thesis by A4, Th26;

    end;

    begin

    reserve T,X,Y for Subset of MC-wff ;

    reserve p,q,r for Element of MC-wff ;

    definition

      let T be Subset of MC-wff ;

      :: INTPRO_1:def19

      attr T is CPC_theory means for p,q,r be Element of MC-wff holds (p => (q => p)) in T & ((p => (q => r)) => ((p => q) => (p => r))) in T & ((p '&' q) => p) in T & ((p '&' q) => q) in T & (p => (q => (p '&' q))) in T & (p => (p 'or' q)) in T & (q => (p 'or' q)) in T & ((p => r) => ((q => r) => ((p 'or' q) => r))) in T & ( FALSUM => p) in T & (p 'or' (p => FALSUM )) in T & (p in T & (p => q) in T implies q in T);

      correctness ;

    end

    theorem :: INTPRO_1:67

    T is CPC_theory implies T is IPC_theory;

    definition

      let X;

      :: INTPRO_1:def20

      func CnCPC X -> Subset of MC-wff means

      : Def20: r in it iff for T st T is CPC_theory & X c= T holds r in T;

      existence

      proof

        defpred P[ object] means for T st T is CPC_theory & X c= T holds $1 in T;

        consider Y be set such that

         A1: for a be object holds a in Y iff a in MC-wff & P[a] from XBOOLE_0:sch 1;

        Y c= MC-wff by A1;

        then

        reconsider Z = Y as Subset of MC-wff ;

        take Z;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let Y,Z be Subset of MC-wff such that

         A2: r in Y iff for T st T is CPC_theory & X c= T holds r in T and

         A3: r in Z iff for T st T is CPC_theory & X c= T holds r in T;

        for a be object holds a in Y iff a in Z

        proof

          let a be object;

          hereby

            assume

             A4: a in Y;

            then

            reconsider t = a as Element of MC-wff ;

            for T st T is CPC_theory & X c= T holds t in T by A2, A4;

            hence a in Z by A3;

          end;

          assume

           A5: a in Z;

          then

          reconsider t = a as Element of MC-wff ;

          for T st T is CPC_theory & X c= T holds t in T by A3, A5;

          hence thesis by A2;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      :: INTPRO_1:def21

      func CPC-Taut -> Subset of MC-wff equals ( CnCPC ( {} MC-wff ));

      correctness ;

    end

    theorem :: INTPRO_1:68

    

     Th68: ( CnIPC X) c= ( CnCPC X)

    proof

      let a be object;

      assume

       A1: a in ( CnIPC X);

      then

      reconsider r = a as Element of MC-wff ;

      for T st T is CPC_theory & X c= T holds r in T

      proof

        let T such that

         A2: T is CPC_theory and

         A3: X c= T;

        T is IPC_theory by A2;

        hence thesis by A1, A3, Def15;

      end;

      hence thesis by Def20;

    end;

    theorem :: INTPRO_1:69

    

     Th69: (p => (q => p)) in ( CnCPC X) & ((p => (q => r)) => ((p => q) => (p => r))) in ( CnCPC X) & ((p '&' q) => p) in ( CnCPC X) & ((p '&' q) => q) in ( CnCPC X) & (p => (q => (p '&' q))) in ( CnCPC X) & (p => (p 'or' q)) in ( CnCPC X) & (q => (p 'or' q)) in ( CnCPC X) & ((p => r) => ((q => r) => ((p 'or' q) => r))) in ( CnCPC X) & ( FALSUM => p) in ( CnCPC X) & (p 'or' (p => FALSUM )) in ( CnCPC X)

    proof

      

       A1: ( CnIPC X) c= ( CnCPC X) by Th68;

      (p => (q => p)) in ( CnIPC X) by Th1;

      hence (p => (q => p)) in ( CnCPC X) by A1;

      

       A2: ( CnIPC X) c= ( CnCPC X) by Th68;

      ((p => (q => r)) => ((p => q) => (p => r))) in ( CnIPC X) by Th2;

      hence ((p => (q => r)) => ((p => q) => (p => r))) in ( CnCPC X) by A2;

      

       A3: ( CnIPC X) c= ( CnCPC X) by Th68;

      ((p '&' q) => p) in ( CnIPC X) by Th3;

      hence ((p '&' q) => p) in ( CnCPC X) by A3;

      

       A4: ( CnIPC X) c= ( CnCPC X) by Th68;

      ((p '&' q) => q) in ( CnIPC X) by Th4;

      hence ((p '&' q) => q) in ( CnCPC X) by A4;

      

       A5: ( CnIPC X) c= ( CnCPC X) by Th68;

      (p => (q => (p '&' q))) in ( CnIPC X) by Th5;

      hence (p => (q => (p '&' q))) in ( CnCPC X) by A5;

      

       A6: ( CnIPC X) c= ( CnCPC X) by Th68;

      (p => (p 'or' q)) in ( CnIPC X) by Th6;

      hence (p => (p 'or' q)) in ( CnCPC X) by A6;

      

       A7: ( CnIPC X) c= ( CnCPC X) by Th68;

      (q => (p 'or' q)) in ( CnIPC X) by Th7;

      hence (q => (p 'or' q)) in ( CnCPC X) by A7;

      

       A8: ( CnIPC X) c= ( CnCPC X) by Th68;

      ((p => r) => ((q => r) => ((p 'or' q) => r))) in ( CnIPC X) by Th8;

      hence ((p => r) => ((q => r) => ((p 'or' q) => r))) in ( CnCPC X) by A8;

      

       A9: ( CnIPC X) c= ( CnCPC X) by Th68;

      ( FALSUM => p) in ( CnIPC X) by Th9;

      hence ( FALSUM => p) in ( CnCPC X) by A9;

      T is CPC_theory & X c= T implies (p 'or' (p => FALSUM )) in T;

      hence (p 'or' (p => FALSUM )) in ( CnCPC X) by Def20;

    end;

    theorem :: INTPRO_1:70

    

     Th70: p in ( CnCPC X) & (p => q) in ( CnCPC X) implies q in ( CnCPC X)

    proof

      assume that

       A1: p in ( CnCPC X) and

       A2: (p => q) in ( CnCPC X);

      T is CPC_theory & X c= T implies q in T

      proof

        assume that

         A3: T is CPC_theory and

         A4: X c= T;

        

         A5: (p => q) in T by A2, A3, A4, Def20;

        p in T by A1, A3, A4, Def20;

        hence thesis by A3, A5;

      end;

      hence thesis by Def20;

    end;

    theorem :: INTPRO_1:71

    

     Th71: T is CPC_theory & X c= T implies ( CnCPC X) c= T by Def20;

    theorem :: INTPRO_1:72

    

     Th72: X c= ( CnCPC X)

    proof

      let a be object;

      assume

       A1: a in X;

      then

      reconsider t = a as Element of MC-wff ;

      for T st T is CPC_theory & X c= T holds t in T by A1;

      hence thesis by Def20;

    end;

    theorem :: INTPRO_1:73

    

     Th73: X c= Y implies ( CnCPC X) c= ( CnCPC Y)

    proof

      assume

       A1: X c= Y;

      thus ( CnCPC X) c= ( CnCPC Y)

      proof

        let a be object;

        assume

         A2: a in ( CnCPC X);

        then

        reconsider t = a as Element of MC-wff ;

        for T st T is CPC_theory & Y c= T holds t in T

        proof

          let T such that

           A3: T is CPC_theory and

           A4: Y c= T;

          X c= T by A1, A4;

          hence thesis by A2, A3, Def20;

        end;

        hence thesis by Def20;

      end;

    end;

    

     Lm21: ( CnCPC ( CnCPC X)) c= ( CnCPC X)

    proof

      let a be object;

      assume

       A1: a in ( CnCPC ( CnCPC X));

      then

      reconsider t = a as Element of MC-wff ;

      for T st T is CPC_theory & X c= T holds t in T

      proof

        let T;

        assume that

         A2: T is CPC_theory and

         A3: X c= T;

        ( CnCPC X) c= T by A2, A3, Th71;

        hence thesis by A1, A2, Def20;

      end;

      hence thesis by Def20;

    end;

    theorem :: INTPRO_1:74

    ( CnCPC ( CnCPC X)) = ( CnCPC X)

    proof

      

       A1: ( CnCPC X) c= ( CnCPC ( CnCPC X)) by Th72;

      ( CnCPC ( CnCPC X)) c= ( CnCPC X) by Lm21;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    

     Lm22: ( CnCPC X) is CPC_theory by Th69, Th70;

    registration

      let X be Subset of MC-wff ;

      cluster ( CnCPC X) -> CPC_theory;

      coherence by Lm22;

    end

    theorem :: INTPRO_1:75

    

     Th75: T is CPC_theory iff ( CnCPC T) = T

    proof

      hereby

        assume

         A1: T is CPC_theory;

        

         A2: ( CnCPC T) c= T by A1, Def20;

        T c= ( CnCPC T) by Th72;

        hence ( CnCPC T) = T by A2, XBOOLE_0:def 10;

      end;

      thus thesis;

    end;

    theorem :: INTPRO_1:76

    T is CPC_theory implies CPC-Taut c= T

    proof

      assume

       A1: T is CPC_theory;

       CPC-Taut c= ( CnCPC T) by Th73, XBOOLE_1: 2;

      hence thesis by A1, Th75;

    end;

    registration

      cluster CPC-Taut -> CPC_theory;

      coherence ;

    end

    theorem :: INTPRO_1:77

     IPC-Taut c= CPC-Taut by Th68;

    begin

    reserve T,X,Y for Subset of MC-wff ;

    reserve p,q,r for Element of MC-wff ;

    definition

      let T be Subset of MC-wff ;

      :: INTPRO_1:def22

      attr T is S4_theory means for p,q,r be Element of MC-wff holds (p => (q => p)) in T & ((p => (q => r)) => ((p => q) => (p => r))) in T & ((p '&' q) => p) in T & ((p '&' q) => q) in T & (p => (q => (p '&' q))) in T & (p => (p 'or' q)) in T & (q => (p 'or' q)) in T & ((p => r) => ((q => r) => ((p 'or' q) => r))) in T & ( FALSUM => p) in T & (p 'or' (p => FALSUM )) in T & (( Nes (p => q)) => (( Nes p) => ( Nes q))) in T & (( Nes p) => p) in T & (( Nes p) => ( Nes ( Nes p))) in T & (p in T & (p => q) in T implies q in T) & (p in T implies ( Nes p) in T);

      correctness ;

    end

    theorem :: INTPRO_1:78

    T is S4_theory implies T is CPC_theory;

    theorem :: INTPRO_1:79

    T is S4_theory implies T is IPC_theory;

    definition

      let X;

      :: INTPRO_1:def23

      func CnS4 X -> Subset of MC-wff means

      : Def23: r in it iff for T st T is S4_theory & X c= T holds r in T;

      existence

      proof

        defpred P[ object] means for T st T is S4_theory & X c= T holds $1 in T;

        consider Y be set such that

         A1: for a be object holds a in Y iff a in MC-wff & P[a] from XBOOLE_0:sch 1;

        Y c= MC-wff by A1;

        then

        reconsider Z = Y as Subset of MC-wff ;

        take Z;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let Y,Z be Subset of MC-wff such that

         A2: r in Y iff for T st T is S4_theory & X c= T holds r in T and

         A3: r in Z iff for T st T is S4_theory & X c= T holds r in T;

        for a be object holds a in Y iff a in Z

        proof

          let a be object;

          hereby

            assume

             A4: a in Y;

            then

            reconsider t = a as Element of MC-wff ;

            for T st T is S4_theory & X c= T holds t in T by A2, A4;

            hence a in Z by A3;

          end;

          assume

           A5: a in Z;

          then

          reconsider t = a as Element of MC-wff ;

          for T st T is S4_theory & X c= T holds t in T by A3, A5;

          hence thesis by A2;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      :: INTPRO_1:def24

      func S4-Taut -> Subset of MC-wff equals ( CnS4 ( {} MC-wff ));

      correctness ;

    end

    theorem :: INTPRO_1:80

    

     Th80: ( CnCPC X) c= ( CnS4 X)

    proof

      let a be object;

      assume

       A1: a in ( CnCPC X);

      then

      reconsider r = a as Element of MC-wff ;

      for T st T is S4_theory & X c= T holds r in T

      proof

        let T such that

         A2: T is S4_theory and

         A3: X c= T;

        T is CPC_theory by A2;

        hence thesis by A1, A3, Def20;

      end;

      hence thesis by Def23;

    end;

    theorem :: INTPRO_1:81

    

     Th81: ( CnIPC X) c= ( CnS4 X)

    proof

      

       A1: ( CnCPC X) c= ( CnS4 X) by Th80;

      ( CnIPC X) c= ( CnCPC X) by Th68;

      hence thesis by A1;

    end;

    theorem :: INTPRO_1:82

    

     Th82: (p => (q => p)) in ( CnS4 X) & ((p => (q => r)) => ((p => q) => (p => r))) in ( CnS4 X) & ((p '&' q) => p) in ( CnS4 X) & ((p '&' q) => q) in ( CnS4 X) & (p => (q => (p '&' q))) in ( CnS4 X) & (p => (p 'or' q)) in ( CnS4 X) & (q => (p 'or' q)) in ( CnS4 X) & ((p => r) => ((q => r) => ((p 'or' q) => r))) in ( CnS4 X) & ( FALSUM => p) in ( CnS4 X) & (p 'or' (p => FALSUM )) in ( CnS4 X)

    proof

      

       A1: ( CnIPC X) c= ( CnS4 X) by Th81;

      (p => (q => p)) in ( CnIPC X) by Th1;

      hence (p => (q => p)) in ( CnS4 X) by A1;

      

       A2: ( CnIPC X) c= ( CnS4 X) by Th81;

      ((p => (q => r)) => ((p => q) => (p => r))) in ( CnIPC X) by Th2;

      hence ((p => (q => r)) => ((p => q) => (p => r))) in ( CnS4 X) by A2;

      

       A3: ( CnIPC X) c= ( CnS4 X) by Th81;

      ((p '&' q) => p) in ( CnIPC X) by Th3;

      hence ((p '&' q) => p) in ( CnS4 X) by A3;

      

       A4: ( CnIPC X) c= ( CnS4 X) by Th81;

      ((p '&' q) => q) in ( CnIPC X) by Th4;

      hence ((p '&' q) => q) in ( CnS4 X) by A4;

      

       A5: ( CnIPC X) c= ( CnS4 X) by Th81;

      (p => (q => (p '&' q))) in ( CnIPC X) by Th5;

      hence (p => (q => (p '&' q))) in ( CnS4 X) by A5;

      

       A6: ( CnIPC X) c= ( CnS4 X) by Th81;

      (p => (p 'or' q)) in ( CnIPC X) by Th6;

      hence (p => (p 'or' q)) in ( CnS4 X) by A6;

      

       A7: ( CnIPC X) c= ( CnS4 X) by Th81;

      (q => (p 'or' q)) in ( CnIPC X) by Th7;

      hence (q => (p 'or' q)) in ( CnS4 X) by A7;

      

       A8: ( CnIPC X) c= ( CnS4 X) by Th81;

      ((p => r) => ((q => r) => ((p 'or' q) => r))) in ( CnIPC X) by Th8;

      hence ((p => r) => ((q => r) => ((p 'or' q) => r))) in ( CnS4 X) by A8;

      

       A9: ( CnIPC X) c= ( CnS4 X) by Th81;

      ( FALSUM => p) in ( CnIPC X) by Th9;

      hence ( FALSUM => p) in ( CnS4 X) by A9;

      T is S4_theory & X c= T implies (p 'or' (p => FALSUM )) in T;

      hence (p 'or' (p => FALSUM )) in ( CnS4 X) by Def23;

    end;

    theorem :: INTPRO_1:83

    

     Th83: p in ( CnS4 X) & (p => q) in ( CnS4 X) implies q in ( CnS4 X)

    proof

      assume that

       A1: p in ( CnS4 X) and

       A2: (p => q) in ( CnS4 X);

      T is S4_theory & X c= T implies q in T

      proof

        assume that

         A3: T is S4_theory and

         A4: X c= T;

        

         A5: (p => q) in T by A2, A3, A4, Def23;

        p in T by A1, A3, A4, Def23;

        hence thesis by A3, A5;

      end;

      hence thesis by Def23;

    end;

    theorem :: INTPRO_1:84

    

     Th84: (( Nes (p => q)) => (( Nes p) => ( Nes q))) in ( CnS4 X)

    proof

      T is S4_theory & X c= T implies (( Nes (p => q)) => (( Nes p) => ( Nes q))) in T;

      hence thesis by Def23;

    end;

    theorem :: INTPRO_1:85

    

     Th85: (( Nes p) => p) in ( CnS4 X)

    proof

      T is S4_theory & X c= T implies (( Nes p) => p) in T;

      hence thesis by Def23;

    end;

    theorem :: INTPRO_1:86

    

     Th86: (( Nes p) => ( Nes ( Nes p))) in ( CnS4 X)

    proof

      T is S4_theory & X c= T implies (( Nes p) => ( Nes ( Nes p))) in T;

      hence thesis by Def23;

    end;

    theorem :: INTPRO_1:87

    

     Th87: p in ( CnS4 X) implies ( Nes p) in ( CnS4 X)

    proof

      assume

       A1: p in ( CnS4 X);

      T is S4_theory & X c= T implies ( Nes p) in T

      proof

        assume that

         A2: T is S4_theory and

         A3: X c= T;

        p in T by A1, A2, A3, Def23;

        hence thesis by A2;

      end;

      hence thesis by Def23;

    end;

    theorem :: INTPRO_1:88

    

     Th88: T is S4_theory & X c= T implies ( CnS4 X) c= T by Def23;

    theorem :: INTPRO_1:89

    

     Th89: X c= ( CnS4 X)

    proof

      let a be object;

      assume

       A1: a in X;

      then

      reconsider t = a as Element of MC-wff ;

      for T st T is S4_theory & X c= T holds t in T by A1;

      hence thesis by Def23;

    end;

    theorem :: INTPRO_1:90

    

     Th90: X c= Y implies ( CnS4 X) c= ( CnS4 Y)

    proof

      assume

       A1: X c= Y;

      thus ( CnS4 X) c= ( CnS4 Y)

      proof

        let a be object;

        assume

         A2: a in ( CnS4 X);

        then

        reconsider t = a as Element of MC-wff ;

        for T st T is S4_theory & Y c= T holds t in T

        proof

          let T such that

           A3: T is S4_theory and

           A4: Y c= T;

          X c= T by A1, A4;

          hence thesis by A2, A3, Def23;

        end;

        hence thesis by Def23;

      end;

    end;

    

     Lm23: ( CnS4 ( CnS4 X)) c= ( CnS4 X)

    proof

      let a be object;

      assume

       A1: a in ( CnS4 ( CnS4 X));

      then

      reconsider t = a as Element of MC-wff ;

      for T st T is S4_theory & X c= T holds t in T

      proof

        let T;

        assume that

         A2: T is S4_theory and

         A3: X c= T;

        ( CnS4 X) c= T by A2, A3, Th88;

        hence thesis by A1, A2, Def23;

      end;

      hence thesis by Def23;

    end;

    theorem :: INTPRO_1:91

    ( CnS4 ( CnS4 X)) = ( CnS4 X)

    proof

      

       A1: ( CnS4 X) c= ( CnS4 ( CnS4 X)) by Th89;

      ( CnS4 ( CnS4 X)) c= ( CnS4 X) by Lm23;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    

     Lm24: ( CnS4 X) is S4_theory by Th82, Th84, Th85, Th86, Th83, Th87;

    registration

      let X be Subset of MC-wff ;

      cluster ( CnS4 X) -> S4_theory;

      coherence by Lm24;

    end

    theorem :: INTPRO_1:92

    

     Th92: T is S4_theory iff ( CnS4 T) = T

    proof

      hereby

        assume

         A1: T is S4_theory;

        

         A2: ( CnS4 T) c= T by A1, Def23;

        T c= ( CnS4 T) by Th89;

        hence ( CnS4 T) = T by A2, XBOOLE_0:def 10;

      end;

      thus thesis;

    end;

    theorem :: INTPRO_1:93

    T is S4_theory implies S4-Taut c= T

    proof

      assume

       A1: T is S4_theory;

       S4-Taut c= ( CnS4 T) by Th90, XBOOLE_1: 2;

      hence thesis by A1, Th92;

    end;

    registration

      cluster S4-Taut -> S4_theory;

      coherence ;

    end

    theorem :: INTPRO_1:94

     CPC-Taut c= S4-Taut by Th80;

    theorem :: INTPRO_1:95

     IPC-Taut c= S4-Taut by Th81;