hilbert1.miz



    begin

    definition

      let D be set;

      :: HILBERT1:def1

      attr D is with_VERUM means

      : Def1: <* 0 *> in D;

    end

    definition

      let D be set;

      :: HILBERT1:def2

      attr D is with_implication means

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

    end

    definition

      let D be set;

      :: HILBERT1:def3

      attr D is with_conjunction means

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

    end

    definition

      let D be set;

      :: HILBERT1:def4

      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;

      :: HILBERT1:def5

      attr D is HP-closed means

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

    end

    

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

    proof

      let D be set;

      assume D is HP-closed;

      then D is with_VERUM;

      hence thesis;

    end;

    registration

      cluster HP-closed -> with_VERUM with_implication with_conjunction with_propositional_variables non empty for set;

      coherence by Lm1;

      cluster with_VERUM with_implication with_conjunction with_propositional_variables -> HP-closed for Subset of ( NAT * );

      coherence ;

    end

    definition

      :: HILBERT1:def6

      func HP-WFF -> set means

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

      existence

      proof

        

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

        defpred P[ set] means for D be set st D is HP-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 HP-closed holds <* 0 *> in D by Def1;

        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 (( <*2*> ^ 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 HP-closed holds (( <*2*> ^ p) ^ q) in D

          proof

            let D be set;

            assume

             A9: D is HP-closed;

            then

             A10: q in D by A2, A6;

            p in D by A2, A5, A9;

            hence thesis by A9, A10, Def3;

          end;

          p in ( NAT * ) by A2, A5;

          then

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

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

          hence thesis by A2, A8;

        end;

        then

         A11: D0 is with_conjunction;

        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

           A12: p in D0 and

           A13: q in D0;

          

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

          

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

          proof

            let D be set;

            assume

             A16: D is HP-closed;

            then

             A17: q in D by A2, A13;

            p in D by A2, A12, A16;

            hence thesis by A16, A17, Def2;

          end;

          p in ( NAT * ) by A2, A12;

          then

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

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

          hence thesis by A2, A15;

        end;

        then

         A18: D0 is with_implication;

        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 HP-closed holds <*p*> in D by Def4;

          hence thesis by A2, A19;

        end;

        then

         A20: D0 is with_propositional_variables;

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

        then D0 is with_VERUM;

        hence D0 is HP-closed by A4, A20, A18, A11;

        let D be set such that

         A21: D is HP-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 HP-closed and

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

         A24: D2 is HP-closed and

         A25: for D be set st D is HP-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 HP-WFF -> HP-closed;

      coherence by Def6;

    end

    registration

      cluster HP-closed non empty for set;

      existence

      proof

        take HP-WFF ;

        thus thesis;

      end;

    end

    registration

      cluster HP-WFF -> functional;

      coherence

      proof

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

        hence thesis;

      end;

    end

    registration

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

      coherence

      proof

        let p be Element of HP-WFF ;

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

        hence thesis;

      end;

    end

    definition

      mode HP-formula is Element of HP-WFF ;

    end

    definition

      :: HILBERT1:def7

      func VERUM -> HP-formula equals <* 0 *>;

      correctness by Def1;

      let p,q be Element of HP-WFF ;

      :: HILBERT1:def8

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

      coherence by Def2;

      :: HILBERT1:def9

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

      correctness by Def3;

    end

    reserve T,X,Y for Subset of HP-WFF ;

    reserve p,q,r,s for Element of HP-WFF ;

    definition

      let T be Subset of HP-WFF ;

      :: HILBERT1:def10

      attr T is Hilbert_theory means

      : Def10: VERUM in T & for p,q,r be Element of HP-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 in T & (p => q) in T implies q in T);

      correctness ;

    end

    definition

      let X;

      :: HILBERT1:def11

      func CnPos X -> Subset of HP-WFF means

      : Def11: r in it iff for T st T is Hilbert_theory & X c= T holds r in T;

      existence

      proof

        defpred P[ set] means (for T st T is Hilbert_theory & X c= T holds $1 in T);

        consider Y be set such that

         A1: for a be set holds a in Y iff a in HP-WFF & P[a] from XFAMILY:sch 1;

        Y c= HP-WFF by A1;

        then

        reconsider Z = Y as Subset of HP-WFF ;

        take Z;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let Y,Z be Subset of HP-WFF such that

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

         A3: r in Z iff for T st T is Hilbert_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 HP-WFF ;

            for T st T is Hilbert_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 HP-WFF ;

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

          hence thesis by A2;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      :: HILBERT1:def12

      func HP_TAUT -> Subset of HP-WFF equals ( CnPos ( {} HP-WFF ));

      correctness ;

    end

    theorem :: HILBERT1:1

    

     Th1: VERUM in ( CnPos X)

    proof

      T is Hilbert_theory & X c= T implies VERUM in T;

      hence thesis by Def11;

    end;

    theorem :: HILBERT1:2

    

     Th2: (p => (q => (p '&' q))) in ( CnPos X)

    proof

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

      hence thesis by Def11;

    end;

    theorem :: HILBERT1:3

    

     Th3: ((p => (q => r)) => ((p => q) => (p => r))) in ( CnPos X)

    proof

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

      hence thesis by Def11;

    end;

    theorem :: HILBERT1:4

    

     Th4: (p => (q => p)) in ( CnPos X)

    proof

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

      hence thesis by Def11;

    end;

    theorem :: HILBERT1:5

    

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

    proof

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

      hence thesis by Def11;

    end;

    theorem :: HILBERT1:6

    

     Th6: ((p '&' q) => q) in ( CnPos X)

    proof

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

      hence thesis by Def11;

    end;

    theorem :: HILBERT1:7

    

     Th7: p in ( CnPos X) & (p => q) in ( CnPos X) implies q in ( CnPos X)

    proof

      assume that

       A1: p in ( CnPos X) and

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

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

      proof

        assume that

         A3: T is Hilbert_theory and

         A4: X c= T;

        

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

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

        hence thesis by A3, A5;

      end;

      hence thesis by Def11;

    end;

    theorem :: HILBERT1:8

    

     Th8: T is Hilbert_theory & X c= T implies ( CnPos X) c= T by Def11;

    theorem :: HILBERT1:9

    

     Th9: X c= ( CnPos X)

    proof

      let a be object;

      assume

       A1: a in X;

      then

      reconsider t = a as Element of HP-WFF ;

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

      hence thesis by Def11;

    end;

    theorem :: HILBERT1:10

    

     Th10: X c= Y implies ( CnPos X) c= ( CnPos Y)

    proof

      assume

       A1: X c= Y;

      thus ( CnPos X) c= ( CnPos Y)

      proof

        let a be object;

        assume

         A2: a in ( CnPos X);

        then

        reconsider t = a as Element of HP-WFF ;

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

        proof

          let T such that

           A3: T is Hilbert_theory and

           A4: Y c= T;

          X c= T by A1, A4;

          hence thesis by A2, A3, Def11;

        end;

        hence thesis by Def11;

      end;

    end;

    

     Lm2: ( CnPos ( CnPos X)) c= ( CnPos X)

    proof

      let a be object;

      assume

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

      then

      reconsider t = a as Element of HP-WFF ;

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

      proof

        let T;

        assume that

         A2: T is Hilbert_theory and

         A3: X c= T;

        ( CnPos X) c= T by A2, A3, Th8;

        hence thesis by A1, A2, Def11;

      end;

      hence thesis by Def11;

    end;

    theorem :: HILBERT1:11

    ( CnPos ( CnPos X)) = ( CnPos X)

    proof

      

       A1: ( CnPos X) c= ( CnPos ( CnPos X)) by Th9;

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

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    

     Lm3: ( CnPos X) is Hilbert_theory by Th1, Th4, Th3, Th5, Th6, Th2, Th7;

    registration

      let X be Subset of HP-WFF ;

      cluster ( CnPos X) -> Hilbert_theory;

      coherence by Lm3;

    end

    theorem :: HILBERT1:12

    

     Th12: T is Hilbert_theory iff ( CnPos T) = T

    proof

      hereby

        assume

         A1: T is Hilbert_theory;

        

         A2: ( CnPos T) c= T by A1, Def11;

        T c= ( CnPos T) by Th9;

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

      end;

      thus thesis;

    end;

    theorem :: HILBERT1:13

    T is Hilbert_theory implies HP_TAUT c= T

    proof

      assume

       A1: T is Hilbert_theory;

       HP_TAUT c= ( CnPos T) by Th10, XBOOLE_1: 2;

      hence thesis by A1, Th12;

    end;

    registration

      cluster HP_TAUT -> Hilbert_theory;

      coherence ;

    end

    begin

    theorem :: HILBERT1:14

    

     Th14: (p => p) in HP_TAUT

    proof

      

       A1: (p => (p => p)) in HP_TAUT by Def10;

      

       A2: (p => ((p => p) => p)) in HP_TAUT by Def10;

      ((p => ((p => p) => p)) => ((p => (p => p)) => (p => p))) in HP_TAUT by Def10;

      then ((p => (p => p)) => (p => p)) in HP_TAUT by A2, Def10;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:15

    

     Th15: q in HP_TAUT implies (p => q) in HP_TAUT

    proof

      (q => (p => q)) in HP_TAUT by Def10;

      hence thesis by Def10;

    end;

    theorem :: HILBERT1:16

    (p => VERUM ) in HP_TAUT by Th1, Th15;

    theorem :: HILBERT1:17

    ((p => q) => (p => p)) in HP_TAUT by Th14, Th15;

    theorem :: HILBERT1:18

    ((q => p) => (p => p)) in HP_TAUT by Th14, Th15;

    theorem :: HILBERT1:19

    

     Th19: ((q => r) => ((p => q) => (p => r))) in HP_TAUT

    proof

      

       A1: ((p => (q => r)) => ((p => q) => (p => r))) in HP_TAUT by Def10;

      

       A2: (((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) => (((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r))))) in HP_TAUT by Def10;

      (((p => (q => r)) => ((p => q) => (p => r))) => ((q => r) => ((p => (q => r)) => ((p => q) => (p => r))))) in HP_TAUT by Def10;

      then ((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in HP_TAUT by A1, Def10;

      then

       A3: (((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r)))) in HP_TAUT by A2, Def10;

      ((q => r) => (p => (q => r))) in HP_TAUT by Def10;

      hence thesis by A3, Def10;

    end;

    theorem :: HILBERT1:20

    

     Th20: (p => (q => r)) in HP_TAUT implies (q => (p => r)) in HP_TAUT

    proof

      assume

       A1: (p => (q => r)) in HP_TAUT ;

      

       A2: (((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r)))) in HP_TAUT by Th19;

      ((p => (q => r)) => ((p => q) => (p => r))) in HP_TAUT by Def10;

      then ((p => q) => (p => r)) in HP_TAUT by A1, Def10;

      then

       A3: ((q => (p => q)) => (q => (p => r))) in HP_TAUT by A2, Def10;

      (q => (p => q)) in HP_TAUT by Def10;

      hence thesis by A3, Def10;

    end;

    theorem :: HILBERT1:21

    

     Th21: ((p => q) => ((q => r) => (p => r))) in HP_TAUT

    proof

      ((q => r) => ((p => q) => (p => r))) in HP_TAUT by Th19;

      hence thesis by Th20;

    end;

    theorem :: HILBERT1:22

    

     Th22: (p => q) in HP_TAUT implies ((q => r) => (p => r)) in HP_TAUT

    proof

      assume

       A1: (p => q) in HP_TAUT ;

      ((p => q) => ((q => r) => (p => r))) in HP_TAUT by Th21;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:23

    

     Th23: (p => q) in HP_TAUT & (q => r) in HP_TAUT implies (p => r) in HP_TAUT

    proof

      assume that

       A1: (p => q) in HP_TAUT and

       A2: (q => r) in HP_TAUT ;

      ((p => q) => ((q => r) => (p => r))) in HP_TAUT by Th21;

      then ((q => r) => (p => r)) in HP_TAUT by A1, Def10;

      hence thesis by A2, Def10;

    end;

    

     Lm4: ((((q => r) => (p => r)) => s) => ((p => q) => s)) in HP_TAUT

    proof

      ((p => q) => ((q => r) => (p => r))) in HP_TAUT by Th21;

      hence thesis by Th22;

    end;

    theorem :: HILBERT1:24

    

     Th24: ((p => (q => r)) => ((s => q) => (p => (s => r)))) in HP_TAUT

    proof

      

       A1: ((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) in HP_TAUT by Lm4;

      (((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) => ((p => (q => r)) => ((s => q) => (p => (s => r))))) in HP_TAUT by Lm4;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:25

    (((p => q) => r) => (q => r)) in HP_TAUT

    proof

      

       A1: ((q => (p => q)) => (((p => q) => r) => (q => r))) in HP_TAUT by Th21;

      (q => (p => q)) in HP_TAUT by Def10;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:26

    

     Th26: ((p => (q => r)) => (q => (p => r))) in HP_TAUT

    proof

      

       A1: (q => (p => q)) in HP_TAUT by Def10;

      ((p => (q => r)) => ((p => q) => (p => r))) in HP_TAUT by Def10;

      then

       A2: ((p => q) => ((p => (q => r)) => (p => r))) in HP_TAUT by Th20;

      (((p => q) => ((p => (q => r)) => (p => r))) => ((q => (p => q)) => (q => ((p => (q => r)) => (p => r))))) in HP_TAUT by Th19;

      then ((q => (p => q)) => (q => ((p => (q => r)) => (p => r)))) in HP_TAUT by A2, Def10;

      then (q => ((p => (q => r)) => (p => r))) in HP_TAUT by A1, Def10;

      hence thesis by Th20;

    end;

    theorem :: HILBERT1:27

    

     Th27: ((p => (p => q)) => (p => q)) in HP_TAUT

    proof

      ((p => (p => q)) => ((p => p) => (p => q))) in HP_TAUT by Def10;

      then

       A1: ((p => p) => ((p => (p => q)) => (p => q))) in HP_TAUT by Th20;

      (p => p) in HP_TAUT by Th14;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:28

    (q => ((q => p) => p)) in HP_TAUT

    proof

      

       A1: (((q => p) => (q => p)) => (q => ((q => p) => p))) in HP_TAUT by Th26;

      ((q => p) => (q => p)) in HP_TAUT by Th14;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:29

    

     Th29: (s => (q => p)) in HP_TAUT & q in HP_TAUT implies (s => p) in HP_TAUT

    proof

      assume that

       A1: (s => (q => p)) in HP_TAUT and

       A2: q in HP_TAUT ;

      ((s => (q => p)) => (q => (s => p))) in HP_TAUT by Th26;

      then (q => (s => p)) in HP_TAUT by A1, Def10;

      hence thesis by A2, Def10;

    end;

    begin

    theorem :: HILBERT1:30

    

     Th30: (p => (p '&' p)) in HP_TAUT

    proof

      

       A1: ((p => (p => (p '&' p))) => (p => (p '&' p))) in HP_TAUT by Th27;

      (p => (p => (p '&' p))) in HP_TAUT by Def10;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:31

    

     Th31: (p '&' q) in HP_TAUT iff p in HP_TAUT & q in HP_TAUT

    proof

      hereby

        

         A1: ((p '&' q) => q) in HP_TAUT by Def10;

        assume

         A2: (p '&' q) in HP_TAUT ;

        ((p '&' q) => p) in HP_TAUT by Def10;

        hence p in HP_TAUT & q in HP_TAUT by A2, A1, Def10;

      end;

      assume that

       A3: p in HP_TAUT and

       A4: q in HP_TAUT ;

      (p => (q => (p '&' q))) in HP_TAUT by Def10;

      then (q => (p '&' q)) in HP_TAUT by A3, Def10;

      hence thesis by A4, Def10;

    end;

    theorem :: HILBERT1:32

    (p '&' q) in HP_TAUT implies (q '&' p) in HP_TAUT

    proof

      assume

       A1: (p '&' q) in HP_TAUT ;

      then

       A2: q in HP_TAUT by Th31;

      p in HP_TAUT by A1, Th31;

      hence thesis by A2, Th31;

    end;

    theorem :: HILBERT1:33

    

     Th33: (((p '&' q) => r) => (p => (q => r))) in HP_TAUT

    proof

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

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

      

       A1: ((p => (qp => pr)) => ((p => qp) => (p => pr))) in HP_TAUT by Def10;

      

       A2: (p => (q => (p '&' q))) in HP_TAUT by Def10;

      (p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r)))) in HP_TAUT by Th15, Th21;

      then ((p => qp) => (p => pr)) in HP_TAUT by A1, Def10;

      then

       A3: (p => (((p '&' q) => r) => (q => r))) in HP_TAUT by A2, Def10;

      ((p => (((p '&' q) => r) => (q => r))) => (((p '&' q) => r) => (p => (q => r)))) in HP_TAUT by Th26;

      hence thesis by A3, Def10;

    end;

    theorem :: HILBERT1:34

    

     Th34: ((p => (q => r)) => ((p '&' q) => r)) in HP_TAUT

    proof

      

       A1: (((p '&' q) => q) => ((q => r) => ((p '&' q) => r))) in HP_TAUT by Th21;

      ((p '&' q) => q) in HP_TAUT by Def10;

      then ((q => r) => ((p '&' q) => r)) in HP_TAUT by A1, Def10;

      then

       A2: (p => ((q => r) => ((p '&' q) => r))) in HP_TAUT by Th15;

      

       A3: ((p => ((p '&' q) => r)) => ((p '&' q) => (p => r))) in HP_TAUT by Th26;

      ((p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r)))) in HP_TAUT by Def10;

      then ((p => (q => r)) => (p => ((p '&' q) => r))) in HP_TAUT by A2, Def10;

      then

       A4: ((p => (q => r)) => ((p '&' q) => (p => r))) in HP_TAUT by A3, Th23;

      

       A5: ((p '&' q) => p) in HP_TAUT by Def10;

      (((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r))) in HP_TAUT by Def10;

      then (((p '&' q) => (p => r)) => ((p '&' q) => r)) in HP_TAUT by A5, Th29;

      hence thesis by A4, Th23;

    end;

    theorem :: HILBERT1:35

    

     Th35: ((r => p) => ((r => q) => (r => (p '&' q)))) in HP_TAUT

    proof

      

       A1: ((r => (q => (p '&' q))) => ((r => q) => (r => (p '&' q)))) in HP_TAUT by Def10;

      (p => (q => (p '&' q))) in HP_TAUT by Def10;

      then

       A2: (r => (p => (q => (p '&' q)))) in HP_TAUT by Th15;

      ((r => (p => (q => (p '&' q)))) => ((r => p) => (r => (q => (p '&' q))))) in HP_TAUT by Def10;

      then ((r => p) => (r => (q => (p '&' q)))) in HP_TAUT by A2, Def10;

      hence thesis by A1, Th23;

    end;

    theorem :: HILBERT1:36

    

     Th36: (((p => q) '&' p) => q) in HP_TAUT

    proof

      set P = (p => q);

      

       A1: (P => P) in HP_TAUT by Th14;

      ((P => P) => ((P '&' p) => q)) in HP_TAUT by Th34;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:37

    ((((p => q) '&' p) '&' s) => q) in HP_TAUT

    proof

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

      

       A1: (P => q) in HP_TAUT by Th36;

      ((P '&' s) => P) in HP_TAUT by Def10;

      hence thesis by A1, Th23;

    end;

    theorem :: HILBERT1:38

    ((q => s) => ((p '&' q) => s)) in HP_TAUT

    proof

      set P = (p '&' q);

      

       A1: (P => q) in HP_TAUT by Def10;

      ((P => q) => ((q => s) => (P => s))) in HP_TAUT by Th21;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:39

    

     Th39: ((q => s) => ((q '&' p) => s)) in HP_TAUT

    proof

      set P = (q '&' p);

      

       A1: (P => q) in HP_TAUT by Def10;

      ((P => q) => ((q => s) => (P => s))) in HP_TAUT by Th21;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:40

    

     Th40: (((p '&' s) => q) => ((p '&' s) => (q '&' s))) in HP_TAUT

    proof

      set P = (p '&' s);

      

       A1: ((P => q) => ((P => s) => (P => (q '&' s)))) in HP_TAUT by Th35;

      (P => s) in HP_TAUT by Def10;

      hence thesis by A1, Th29;

    end;

    theorem :: HILBERT1:41

    

     Th41: ((p => q) => ((p '&' s) => (q '&' s))) in HP_TAUT

    proof

      

       A1: (((p '&' s) => q) => ((p '&' s) => (q '&' s))) in HP_TAUT by Th40;

      ((p => q) => ((p '&' s) => q)) in HP_TAUT by Th39;

      hence thesis by A1, Th23;

    end;

    theorem :: HILBERT1:42

    

     Th42: (((p => q) '&' (p '&' s)) => (q '&' s)) in HP_TAUT

    proof

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

      

       A1: (P => (Q => S)) in HP_TAUT by Th41;

      ((P => (Q => S)) => ((P '&' Q) => S)) in HP_TAUT by Th34;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:43

    

     Th43: ((p '&' q) => (q '&' p)) in HP_TAUT

    proof

      set P = (p '&' q);

      

       A1: (P => q) in HP_TAUT by Def10;

      

       A2: (P => p) in HP_TAUT by Def10;

      ((P => q) => ((P => p) => (P => (q '&' p)))) in HP_TAUT by Th35;

      then ((P => p) => (P => (q '&' p))) in HP_TAUT by A1, Def10;

      hence thesis by A2, Def10;

    end;

    theorem :: HILBERT1:44

    

     Th44: (((p => q) '&' (p '&' s)) => (s '&' q)) in HP_TAUT

    proof

      

       A1: ((q '&' s) => (s '&' q)) in HP_TAUT by Th43;

      (((p => q) '&' (p '&' s)) => (q '&' s)) in HP_TAUT by Th42;

      hence thesis by A1, Th23;

    end;

    theorem :: HILBERT1:45

    

     Th45: ((p => q) => ((p '&' s) => (s '&' q))) in HP_TAUT

    proof

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

      

       A1: ((P '&' Q) => S) in HP_TAUT by Th44;

      (((P '&' Q) => S) => (P => (Q => S))) in HP_TAUT by Th33;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:46

    

     Th46: ((p => q) => ((s '&' p) => (s '&' q))) in HP_TAUT

    proof

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

      

       A1: (P => (Q => S)) in HP_TAUT by Th45;

      

       A2: (T => Q) in HP_TAUT by Th43;

      ((P => (Q => S)) => ((T => Q) => (P => (T => S)))) in HP_TAUT by Th24;

      then ((T => Q) => (P => (T => S))) in HP_TAUT by A1, Def10;

      hence thesis by A2, Def10;

    end;

    theorem :: HILBERT1:47

    ((p '&' (s '&' q)) => (p '&' (q '&' s))) in HP_TAUT

    proof

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

      

       A1: (P => Q) in HP_TAUT by Th43;

      ((P => Q) => ((p '&' P) => (p '&' Q))) in HP_TAUT by Th46;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:48

    (((p => q) '&' (p => s)) => (p => (q '&' s))) in HP_TAUT

    proof

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

      

       A1: (P => (Q => S)) in HP_TAUT by Th35;

      ((P => (Q => S)) => ((P '&' Q) => S)) in HP_TAUT by Th34;

      hence thesis by A1, Def10;

    end;

    

     Lm5: (((p '&' q) '&' s) => q) in HP_TAUT

    proof

      

       A1: ((p '&' q) => q) in HP_TAUT by Def10;

      (((p '&' q) '&' s) => (p '&' q)) in HP_TAUT by Def10;

      hence thesis by A1, Th23;

    end;

    

     Lm6: ((((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q)) in HP_TAUT

    proof

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

      

       A1: (P => q) in HP_TAUT by Lm5;

      ((P => q) => ((P '&' P) => (P '&' q))) in HP_TAUT by Th46;

      hence thesis by A1, Def10;

    end;

    

     Lm7: (((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q)) in HP_TAUT

    proof

      

       A1: ((((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q)) in HP_TAUT by Lm6;

      (((p '&' q) '&' s) => (((p '&' q) '&' s) '&' ((p '&' q) '&' s))) in HP_TAUT by Th30;

      hence thesis by A1, Th23;

    end;

    

     Lm8: (((p '&' q) '&' s) => (p '&' s)) in HP_TAUT

    proof

      set P = (p '&' q);

      

       A1: (P => p) in HP_TAUT by Def10;

      ((P => p) => ((P '&' s) => (p '&' s))) in HP_TAUT by Th41;

      hence thesis by A1, Def10;

    end;

    

     Lm9: ((((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q)) in HP_TAUT

    proof

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

      

       A1: (P => Q) in HP_TAUT by Lm8;

      ((P => Q) => ((P '&' q) => (Q '&' q))) in HP_TAUT by Th41;

      hence thesis by A1, Def10;

    end;

    

     Lm10: (((p '&' q) '&' s) => ((p '&' s) '&' q)) in HP_TAUT

    proof

      

       A1: ((((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q)) in HP_TAUT by Lm9;

      (((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q)) in HP_TAUT by Lm7;

      hence thesis by A1, Th23;

    end;

    

     Lm11: (((p '&' s) '&' q) => ((s '&' p) '&' q)) in HP_TAUT

    proof

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

      

       A1: (P => Q) in HP_TAUT by Th43;

      ((P => Q) => ((P '&' q) => (Q '&' q))) in HP_TAUT by Th41;

      hence thesis by A1, Def10;

    end;

    

     Lm12: (((p '&' q) '&' s) => ((s '&' p) '&' q)) in HP_TAUT

    proof

      

       A1: (((p '&' s) '&' q) => ((s '&' p) '&' q)) in HP_TAUT by Lm11;

      (((p '&' q) '&' s) => ((p '&' s) '&' q)) in HP_TAUT by Lm10;

      hence thesis by A1, Th23;

    end;

    

     Lm13: (((p '&' q) '&' s) => ((s '&' q) '&' p)) in HP_TAUT

    proof

      

       A1: (((s '&' p) '&' q) => ((s '&' q) '&' p)) in HP_TAUT by Lm10;

      (((p '&' q) '&' s) => ((s '&' p) '&' q)) in HP_TAUT by Lm12;

      hence thesis by A1, Th23;

    end;

    

     Lm14: (((p '&' q) '&' s) => (p '&' (s '&' q))) in HP_TAUT

    proof

      

       A1: (((s '&' q) '&' p) => (p '&' (s '&' q))) in HP_TAUT by Th43;

      (((p '&' q) '&' s) => ((s '&' q) '&' p)) in HP_TAUT by Lm13;

      hence thesis by A1, Th23;

    end;

    

     Lm15: ((p '&' (s '&' q)) => (p '&' (q '&' s))) in HP_TAUT

    proof

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

      

       A1: ((s '&' q) => (q '&' s)) in HP_TAUT by Th43;

      ((P => Q) => ((p '&' P) => (p '&' Q))) in HP_TAUT by Th46;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:49

    (((p '&' q) '&' s) => (p '&' (q '&' s))) in HP_TAUT

    proof

      

       A1: ((p '&' (s '&' q)) => (p '&' (q '&' s))) in HP_TAUT by Lm15;

      (((p '&' q) '&' s) => (p '&' (s '&' q))) in HP_TAUT by Lm14;

      hence thesis by A1, Th23;

    end;

    

     Lm16: ((p '&' (q '&' s)) => ((s '&' q) '&' p)) in HP_TAUT

    proof

      

       A1: ((p '&' (s '&' q)) => ((s '&' q) '&' p)) in HP_TAUT by Th43;

      ((p '&' (q '&' s)) => (p '&' (s '&' q))) in HP_TAUT by Lm15;

      hence thesis by A1, Th23;

    end;

    

     Lm17: (((s '&' q) '&' p) => ((q '&' s) '&' p)) in HP_TAUT

    proof

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

      

       A1: ((s '&' q) => (q '&' s)) in HP_TAUT by Th43;

      ((P => Q) => ((P '&' p) => (Q '&' p))) in HP_TAUT by Th41;

      hence thesis by A1, Def10;

    end;

    

     Lm18: ((p '&' (q '&' s)) => ((q '&' s) '&' p)) in HP_TAUT

    proof

      

       A1: (((s '&' q) '&' p) => ((q '&' s) '&' p)) in HP_TAUT by Lm17;

      ((p '&' (q '&' s)) => ((s '&' q) '&' p)) in HP_TAUT by Lm16;

      hence thesis by A1, Th23;

    end;

    

     Lm19: ((p '&' (q '&' s)) => ((p '&' s) '&' q)) in HP_TAUT

    proof

      

       A1: (((q '&' s) '&' p) => ((p '&' s) '&' q)) in HP_TAUT by Lm13;

      ((p '&' (q '&' s)) => ((q '&' s) '&' p)) in HP_TAUT by Lm18;

      hence thesis by A1, Th23;

    end;

    

     Lm20: ((p '&' (q '&' s)) => (p '&' (s '&' q))) in HP_TAUT

    proof

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

      

       A1: ((q '&' s) => (s '&' q)) in HP_TAUT by Th43;

      ((P => Q) => ((p '&' P) => (p '&' Q))) in HP_TAUT by Th46;

      hence thesis by A1, Def10;

    end;

    theorem :: HILBERT1:50

    ((p '&' (q '&' s)) => ((p '&' q) '&' s)) in HP_TAUT

    proof

      

       A1: ((p '&' (s '&' q)) => ((p '&' q) '&' s)) in HP_TAUT by Lm19;

      ((p '&' (q '&' s)) => (p '&' (s '&' q))) in HP_TAUT by Lm20;

      hence thesis by A1, Th23;

    end;