:: HILBERT1 semantic presentation begin definition let D be set ; attrD is with_VERUM means :Def1: :: HILBERT1:def 1 <*0*> in D; end; :: deftheorem Def1 defines with_VERUM HILBERT1:def_1_:_ for D being set holds ( D is with_VERUM iff <*0*> in D ); definition let D be set ; attrD is with_implication means :Def2: :: HILBERT1:def 2 for p, q being FinSequence st p in D & q in D holds (<*1*> ^ p) ^ q in D; end; :: deftheorem Def2 defines with_implication HILBERT1:def_2_:_ for D being set holds ( D is with_implication iff for p, q being FinSequence st p in D & q in D holds (<*1*> ^ p) ^ q in D ); definition let D be set ; attrD is with_conjunction means :Def3: :: HILBERT1:def 3 for p, q being FinSequence st p in D & q in D holds (<*2*> ^ p) ^ q in D; end; :: deftheorem Def3 defines with_conjunction HILBERT1:def_3_:_ for D being set holds ( D is with_conjunction iff for p, q being FinSequence st p in D & q in D holds (<*2*> ^ p) ^ q in D ); definition let D be set ; attrD is with_propositional_variables means :Def4: :: HILBERT1:def 4 for n being Element of NAT holds <*(3 + n)*> in D; end; :: deftheorem Def4 defines with_propositional_variables HILBERT1:def_4_:_ for D being set holds ( D is with_propositional_variables iff for n being Element of NAT holds <*(3 + n)*> in D ); definition let D be set ; attrD is HP-closed means :Def5: :: HILBERT1:def 5 ( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables ); end; :: deftheorem Def5 defines HP-closed HILBERT1:def_5_:_ for D being set holds ( D is HP-closed iff ( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables ) ); Lm1: for D being set st D is HP-closed holds not D is empty proof let D be set ; ::_thesis: ( D is HP-closed implies not D is empty ) assume D is HP-closed ; ::_thesis: not D is empty then D is with_VERUM by Def5; hence not D is empty by Def1; ::_thesis: verum end; registration cluster HP-closed -> non empty with_VERUM with_implication with_conjunction with_propositional_variables for set ; coherence for b1 being set st b1 is HP-closed holds ( b1 is with_VERUM & b1 is with_implication & b1 is with_conjunction & b1 is with_propositional_variables & not b1 is empty ) by Def5, Lm1; cluster with_VERUM with_implication with_conjunction with_propositional_variables -> HP-closed for Element of K6((NAT *)); coherence for b1 being Subset of (NAT *) st b1 is with_VERUM & b1 is with_implication & b1 is with_conjunction & b1 is with_propositional_variables holds b1 is HP-closed by Def5; end; definition func HP-WFF -> set means :Def6: :: HILBERT1:def 6 ( it is HP-closed & ( for D being set st D is HP-closed holds it c= D ) ); existence ex b1 being set st ( b1 is HP-closed & ( for D being set st D is HP-closed holds b1 c= D ) ) proof A1: <*0*> in NAT * by FINSEQ_1:def_11; defpred S1[ set ] means for D being set st D is HP-closed holds \$1 in D; consider D0 being set such that A2: for x being set holds ( x in D0 iff ( x in NAT * & S1[x] ) ) from XBOOLE_0:sch_1(); A3: for D being set st D is HP-closed holds <*0*> in D by Def1; then reconsider D0 = D0 as non empty set by A2, A1; take D0 ; ::_thesis: ( D0 is HP-closed & ( for D being set st D is HP-closed holds D0 c= D ) ) A4: D0 c= NAT * proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in NAT * ) thus ( not x in D0 or x in NAT * ) by A2; ::_thesis: verum end; for p, q being FinSequence st p in D0 & q in D0 holds (<*2*> ^ p) ^ q in D0 proof let p, q be FinSequence; ::_thesis: ( p in D0 & q in D0 implies (<*2*> ^ p) ^ q in D0 ) assume that A5: p in D0 and A6: q in D0 ; ::_thesis: (<*2*> ^ p) ^ q in D0 A7: q in NAT * by A2, A6; A8: for D being set st D is HP-closed holds (<*2*> ^ p) ^ q in D proof let D be set ; ::_thesis: ( D is HP-closed implies (<*2*> ^ p) ^ q in D ) assume A9: D is HP-closed ; ::_thesis: (<*2*> ^ p) ^ q in D then A10: q in D by A2, A6; p in D by A2, A5, A9; hence (<*2*> ^ p) ^ q in D by A9, A10, Def3; ::_thesis: verum 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 (<*2*> ^ p) ^ q in D0 by A2, A8; ::_thesis: verum end; then A11: D0 is with_conjunction by Def3; for p, q being FinSequence st p in D0 & q in D0 holds (<*1*> ^ p) ^ q in D0 proof let p, q be FinSequence; ::_thesis: ( p in D0 & q in D0 implies (<*1*> ^ p) ^ q in D0 ) assume that A12: p in D0 and A13: q in D0 ; ::_thesis: (<*1*> ^ p) ^ q in D0 A14: q in NAT * by A2, A13; A15: for D being set st D is HP-closed holds (<*1*> ^ p) ^ q in D proof let D be set ; ::_thesis: ( D is HP-closed implies (<*1*> ^ p) ^ q in D ) assume A16: D is HP-closed ; ::_thesis: (<*1*> ^ p) ^ q in D then A17: q in D by A2, A13; p in D by A2, A12, A16; hence (<*1*> ^ p) ^ q in D by A16, A17, Def2; ::_thesis: verum 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 (<*1*> ^ p) ^ q in D0 by A2, A15; ::_thesis: verum end; then A18: D0 is with_implication by Def2; for n being Element of NAT holds <*(3 + n)*> in D0 proof let n be Element of NAT ; ::_thesis: <*(3 + n)*> in D0 set p = 3 + n; reconsider h = <*(3 + n)*> as FinSequence of NAT ; A19: h in NAT * by FINSEQ_1:def_11; for D being set st D is HP-closed holds <*(3 + n)*> in D by Def4; hence <*(3 + n)*> in D0 by A2, A19; ::_thesis: verum end; then A20: D0 is with_propositional_variables by Def4; <*0*> in D0 by A2, A1, A3; then D0 is with_VERUM by Def1; hence D0 is HP-closed by A4, A20, A18, A11; ::_thesis: for D being set st D is HP-closed holds D0 c= D let D be set ; ::_thesis: ( D is HP-closed implies D0 c= D ) assume A21: D is HP-closed ; ::_thesis: D0 c= D let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in D ) assume x in D0 ; ::_thesis: x in D hence x in D by A2, A21; ::_thesis: verum end; uniqueness for b1, b2 being set st b1 is HP-closed & ( for D being set st D is HP-closed holds b1 c= D ) & b2 is HP-closed & ( for D being set st D is HP-closed holds b2 c= D ) holds b1 = b2 proof let D1, D2 be set ; ::_thesis: ( D1 is HP-closed & ( for D being set st D is HP-closed holds D1 c= D ) & D2 is HP-closed & ( for D being set st D is HP-closed holds D2 c= D ) implies D1 = D2 ) assume that A22: D1 is HP-closed and A23: for D being set st D is HP-closed holds D1 c= D and A24: D2 is HP-closed and A25: for D being set st D is HP-closed holds D2 c= D ; ::_thesis: D1 = D2 A26: D2 c= D1 by A22, A25; D1 c= D2 by A23, A24; hence D1 = D2 by A26, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def6 defines HP-WFF HILBERT1:def_6_:_ for b1 being set holds ( b1 = HP-WFF iff ( b1 is HP-closed & ( for D being set st D is HP-closed holds b1 c= D ) ) ); registration cluster HP-WFF -> HP-closed ; coherence HP-WFF is HP-closed by Def6; end; registration cluster non empty HP-closed for set ; existence ex b1 being set st ( b1 is HP-closed & not b1 is empty ) proof take HP-WFF ; ::_thesis: ( HP-WFF is HP-closed & not HP-WFF is empty ) thus ( HP-WFF is HP-closed & not HP-WFF is empty ) ; ::_thesis: verum end; end; registration cluster HP-WFF -> functional ; coherence HP-WFF is functional proof HP-WFF c= NAT * by Def5; hence HP-WFF is functional ; ::_thesis: verum end; end; registration cluster -> FinSequence-like for Element of HP-WFF ; coherence for b1 being Element of HP-WFF holds b1 is FinSequence-like proof let p be Element of HP-WFF ; ::_thesis: p is FinSequence-like HP-WFF c= NAT * by Def5; hence p is FinSequence-like ; ::_thesis: verum end; end; definition mode HP-formula is Element of HP-WFF ; end; definition func VERUM -> HP-formula equals :: HILBERT1:def 7 <*0*>; correctness coherence <*0*> is HP-formula; by Def1; let p, q be Element of HP-WFF ; funcp => q -> HP-formula equals :: HILBERT1:def 8 (<*1*> ^ p) ^ q; coherence (<*1*> ^ p) ^ q is HP-formula by Def2; funcp '&' q -> HP-formula equals :: HILBERT1:def 9 (<*2*> ^ p) ^ q; correctness coherence (<*2*> ^ p) ^ q is HP-formula; by Def3; end; :: deftheorem defines VERUM HILBERT1:def_7_:_ VERUM = <*0*>; :: deftheorem defines => HILBERT1:def_8_:_ for p, q being Element of HP-WFF holds p => q = (<*1*> ^ p) ^ q; :: deftheorem defines '&' HILBERT1:def_9_:_ for p, q being Element of HP-WFF holds p '&' q = (<*2*> ^ p) ^ q; definition let T be Subset of HP-WFF; attrT is Hilbert_theory means :Def10: :: HILBERT1:def 10 ( VERUM in T & ( for p, q, r being 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; :: deftheorem Def10 defines Hilbert_theory HILBERT1:def_10_:_ for T being Subset of HP-WFF holds ( T is Hilbert_theory iff ( VERUM in T & ( for p, q, r being 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 ) ) ) ) ); definition let X be Subset of HP-WFF; func CnPos X -> Subset of HP-WFF means :Def11: :: HILBERT1:def 11 for r being Element of HP-WFF holds ( r in it iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ); existence ex b1 being Subset of HP-WFF st for r being Element of HP-WFF holds ( r in b1 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ) proof defpred S1[ set ] means for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds \$1 in T; consider Y being set such that A1: for a being set holds ( a in Y iff ( a in HP-WFF & S1[a] ) ) from XBOOLE_0:sch_1(); Y c= HP-WFF proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in HP-WFF ) assume a in Y ; ::_thesis: a in HP-WFF hence a in HP-WFF by A1; ::_thesis: verum end; then reconsider Z = Y as Subset of HP-WFF ; take Z ; ::_thesis: for r being Element of HP-WFF holds ( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ) thus for r being Element of HP-WFF holds ( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of HP-WFF st ( for r being Element of HP-WFF holds ( r in b1 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ) ) & ( for r being Element of HP-WFF holds ( r in b2 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ) ) holds b1 = b2 proof let Y, Z be Subset of HP-WFF; ::_thesis: ( ( for r being Element of HP-WFF holds ( r in Y iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ) ) & ( for r being Element of HP-WFF holds ( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ) ) implies Y = Z ) assume that A2: for r being Element of HP-WFF holds ( r in Y iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ) and A3: for r being Element of HP-WFF holds ( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ) ; ::_thesis: Y = Z for a being set holds ( a in Y iff a in Z ) proof let a be set ; ::_thesis: ( a in Y iff a in Z ) hereby ::_thesis: ( a in Z implies a in Y ) assume A4: a in Y ; ::_thesis: a in Z then reconsider t = a as Element of HP-WFF ; for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds t in T by A2, A4; hence a in Z by A3; ::_thesis: verum end; assume A5: a in Z ; ::_thesis: a in Y then reconsider t = a as Element of HP-WFF ; for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds t in T by A3, A5; hence a in Y by A2; ::_thesis: verum end; hence Y = Z by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def11 defines CnPos HILBERT1:def_11_:_ for X, b2 being Subset of HP-WFF holds ( b2 = CnPos X iff for r being Element of HP-WFF holds ( r in b2 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds r in T ) ); definition func HP_TAUT -> Subset of HP-WFF equals :: HILBERT1:def 12 CnPos ({} HP-WFF); correctness coherence CnPos ({} HP-WFF) is Subset of HP-WFF; ; end; :: deftheorem defines HP_TAUT HILBERT1:def_12_:_ HP_TAUT = CnPos ({} HP-WFF); theorem Th1: :: HILBERT1:1 for X being Subset of HP-WFF holds VERUM in CnPos X proof let X be Subset of HP-WFF; ::_thesis: VERUM in CnPos X for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds VERUM in T by Def10; hence VERUM in CnPos X by Def11; ::_thesis: verum end; theorem Th2: :: HILBERT1:2 for X being Subset of HP-WFF for p, q being Element of HP-WFF holds p => (q => (p '&' q)) in CnPos X proof let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds p => (q => (p '&' q)) in CnPos X let p, q be Element of HP-WFF ; ::_thesis: p => (q => (p '&' q)) in CnPos X for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds p => (q => (p '&' q)) in T by Def10; hence p => (q => (p '&' q)) in CnPos X by Def11; ::_thesis: verum end; theorem Th3: :: HILBERT1:3 for X being Subset of HP-WFF for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) in CnPos X proof let X be Subset of HP-WFF; ::_thesis: for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) in CnPos X let p, q, r be Element of HP-WFF ; ::_thesis: (p => (q => r)) => ((p => q) => (p => r)) in CnPos X for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds (p => (q => r)) => ((p => q) => (p => r)) in T by Def10; hence (p => (q => r)) => ((p => q) => (p => r)) in CnPos X by Def11; ::_thesis: verum end; theorem Th4: :: HILBERT1:4 for X being Subset of HP-WFF for p, q being Element of HP-WFF holds p => (q => p) in CnPos X proof let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds p => (q => p) in CnPos X let p, q be Element of HP-WFF ; ::_thesis: p => (q => p) in CnPos X for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds p => (q => p) in T by Def10; hence p => (q => p) in CnPos X by Def11; ::_thesis: verum end; theorem Th5: :: HILBERT1:5 for X being Subset of HP-WFF for p, q being Element of HP-WFF holds (p '&' q) => p in CnPos X proof let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds (p '&' q) => p in CnPos X let p, q be Element of HP-WFF ; ::_thesis: (p '&' q) => p in CnPos X for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds (p '&' q) => p in T by Def10; hence (p '&' q) => p in CnPos X by Def11; ::_thesis: verum end; theorem Th6: :: HILBERT1:6 for X being Subset of HP-WFF for p, q being Element of HP-WFF holds (p '&' q) => q in CnPos X proof let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds (p '&' q) => q in CnPos X let p, q be Element of HP-WFF ; ::_thesis: (p '&' q) => q in CnPos X for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds (p '&' q) => q in T by Def10; hence (p '&' q) => q in CnPos X by Def11; ::_thesis: verum end; theorem Th7: :: HILBERT1:7 for X being Subset of HP-WFF for p, q being Element of HP-WFF st p in CnPos X & p => q in CnPos X holds q in CnPos X proof let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF st p in CnPos X & p => q in CnPos X holds q in CnPos X let p, q be Element of HP-WFF ; ::_thesis: ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) assume that A1: p in CnPos X and A2: p => q in CnPos X ; ::_thesis: q in CnPos X for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds q in T proof let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & X c= T implies q in T ) assume that A3: T is Hilbert_theory and A4: X c= T ; ::_thesis: q in T A5: p => q in T by A2, A3, A4, Def11; p in T by A1, A3, A4, Def11; hence q in T by A3, A5, Def10; ::_thesis: verum end; hence q in CnPos X by Def11; ::_thesis: verum end; theorem Th8: :: HILBERT1:8 for T, X being Subset of HP-WFF st T is Hilbert_theory & X c= T holds CnPos X c= T proof let T, X be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & X c= T implies CnPos X c= T ) assume that A1: T is Hilbert_theory and A2: X c= T ; ::_thesis: CnPos X c= T let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos X or a in T ) thus ( not a in CnPos X or a in T ) by A1, A2, Def11; ::_thesis: verum end; theorem Th9: :: HILBERT1:9 for X being Subset of HP-WFF holds X c= CnPos X proof let X be Subset of HP-WFF; ::_thesis: X c= CnPos X let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in CnPos X ) assume A1: a in X ; ::_thesis: a in CnPos X then reconsider t = a as Element of HP-WFF ; for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds t in T by A1; hence a in CnPos X by Def11; ::_thesis: verum end; theorem Th10: :: HILBERT1:10 for X, Y being Subset of HP-WFF st X c= Y holds CnPos X c= CnPos Y proof let X, Y be Subset of HP-WFF; ::_thesis: ( X c= Y implies CnPos X c= CnPos Y ) assume A1: X c= Y ; ::_thesis: CnPos X c= CnPos Y thus CnPos X c= CnPos Y ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos X or a in CnPos Y ) assume A2: a in CnPos X ; ::_thesis: a in CnPos Y then reconsider t = a as Element of HP-WFF ; for T being Subset of HP-WFF st T is Hilbert_theory & Y c= T holds t in T proof let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & Y c= T implies t in T ) assume that A3: T is Hilbert_theory and A4: Y c= T ; ::_thesis: t in T X c= T by A1, A4, XBOOLE_1:1; hence t in T by A2, A3, Def11; ::_thesis: verum end; hence a in CnPos Y by Def11; ::_thesis: verum end; end; Lm2: for X being Subset of HP-WFF holds CnPos (CnPos X) c= CnPos X proof let X be Subset of HP-WFF; ::_thesis: CnPos (CnPos X) c= CnPos X let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos (CnPos X) or a in CnPos X ) assume A1: a in CnPos (CnPos X) ; ::_thesis: a in CnPos X then reconsider t = a as Element of HP-WFF ; for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds t in T proof let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & X c= T implies t in T ) assume that A2: T is Hilbert_theory and A3: X c= T ; ::_thesis: t in T CnPos X c= T by A2, A3, Th8; hence t in T by A1, A2, Def11; ::_thesis: verum end; hence a in CnPos X by Def11; ::_thesis: verum end; theorem :: HILBERT1:11 for X being Subset of HP-WFF holds CnPos (CnPos X) = CnPos X proof let X be Subset of HP-WFF; ::_thesis: CnPos (CnPos X) = CnPos X A1: CnPos X c= CnPos (CnPos X) by Th9; CnPos (CnPos X) c= CnPos X by Lm2; hence CnPos (CnPos X) = CnPos X by A1, XBOOLE_0:def_10; ::_thesis: verum end; Lm3: for X being Subset of HP-WFF holds CnPos X is Hilbert_theory proof let X be Subset of HP-WFF; ::_thesis: CnPos X is Hilbert_theory thus VERUM in CnPos X by Th1; :: according to HILBERT1:def_10 ::_thesis: for p, q, r being Element of HP-WFF holds ( p => (q => p) in CnPos X & (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) ) let p, q, r be Element of HP-WFF ; ::_thesis: ( p => (q => p) in CnPos X & (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) ) thus p => (q => p) in CnPos X by Th4; ::_thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) ) thus (p => (q => r)) => ((p => q) => (p => r)) in CnPos X by Th3; ::_thesis: ( (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) ) thus (p '&' q) => p in CnPos X by Th5; ::_thesis: ( (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) ) thus (p '&' q) => q in CnPos X by Th6; ::_thesis: ( p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) ) thus p => (q => (p '&' q)) in CnPos X by Th2; ::_thesis: ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) thus ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) by Th7; ::_thesis: verum end; registration let X be Subset of HP-WFF; cluster CnPos X -> Hilbert_theory ; coherence CnPos X is Hilbert_theory by Lm3; end; theorem Th12: :: HILBERT1:12 for T being Subset of HP-WFF holds ( T is Hilbert_theory iff CnPos T = T ) proof let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory iff CnPos T = T ) hereby ::_thesis: ( CnPos T = T implies T is Hilbert_theory ) assume A1: T is Hilbert_theory ; ::_thesis: CnPos T = T A2: CnPos T c= T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos T or a in T ) assume a in CnPos T ; ::_thesis: a in T hence a in T by A1, Def11; ::_thesis: verum end; T c= CnPos T by Th9; hence CnPos T = T by A2, XBOOLE_0:def_10; ::_thesis: verum end; thus ( CnPos T = T implies T is Hilbert_theory ) ; ::_thesis: verum end; theorem :: HILBERT1:13 for T being Subset of HP-WFF st T is Hilbert_theory holds HP_TAUT c= T proof let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory implies HP_TAUT c= T ) assume A1: T is Hilbert_theory ; ::_thesis: HP_TAUT c= T HP_TAUT c= CnPos T by Th10, XBOOLE_1:2; hence HP_TAUT c= T by A1, Th12; ::_thesis: verum end; registration cluster HP_TAUT -> Hilbert_theory ; coherence HP_TAUT is Hilbert_theory ; end; begin theorem Th14: :: HILBERT1:14 for p being Element of HP-WFF holds p => p in HP_TAUT proof let p be Element of HP-WFF ; ::_thesis: p => p in HP_TAUT 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 p => p in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem Th15: :: HILBERT1:15 for q, p being Element of HP-WFF st q in HP_TAUT holds p => q in HP_TAUT proof let q, p be Element of HP-WFF ; ::_thesis: ( q in HP_TAUT implies p => q in HP_TAUT ) q => (p => q) in HP_TAUT by Def10; hence ( q in HP_TAUT implies p => q in HP_TAUT ) by Def10; ::_thesis: verum end; theorem :: HILBERT1:16 for p being Element of HP-WFF holds p => VERUM in HP_TAUT by Th1, Th15; theorem :: HILBERT1:17 for p, q being Element of HP-WFF holds (p => q) => (p => p) in HP_TAUT by Th14, Th15; theorem :: HILBERT1:18 for q, p being Element of HP-WFF holds (q => p) => (p => p) in HP_TAUT by Th14, Th15; theorem Th19: :: HILBERT1:19 for q, r, p being Element of HP-WFF holds (q => r) => ((p => q) => (p => r)) in HP_TAUT proof let q, r, p be Element of HP-WFF ; ::_thesis: (q => r) => ((p => q) => (p => r)) in HP_TAUT 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 (q => r) => ((p => q) => (p => r)) in HP_TAUT by A3, Def10; ::_thesis: verum end; theorem Th20: :: HILBERT1:20 for p, q, r being Element of HP-WFF st p => (q => r) in HP_TAUT holds q => (p => r) in HP_TAUT proof let p, q, r be Element of HP-WFF ; ::_thesis: ( p => (q => r) in HP_TAUT implies q => (p => r) in HP_TAUT ) assume A1: p => (q => r) in HP_TAUT ; ::_thesis: q => (p => 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 q => (p => r) in HP_TAUT by A3, Def10; ::_thesis: verum end; theorem Th21: :: HILBERT1:21 for p, q, r being Element of HP-WFF holds (p => q) => ((q => r) => (p => r)) in HP_TAUT proof let p, q, r be Element of HP-WFF ; ::_thesis: (p => q) => ((q => r) => (p => r)) in HP_TAUT (q => r) => ((p => q) => (p => r)) in HP_TAUT by Th19; hence (p => q) => ((q => r) => (p => r)) in HP_TAUT by Th20; ::_thesis: verum end; theorem Th22: :: HILBERT1:22 for p, q, r being Element of HP-WFF st p => q in HP_TAUT holds (q => r) => (p => r) in HP_TAUT proof let p, q, r be Element of HP-WFF ; ::_thesis: ( p => q in HP_TAUT implies (q => r) => (p => r) in HP_TAUT ) assume A1: p => q in HP_TAUT ; ::_thesis: (q => r) => (p => r) in HP_TAUT (p => q) => ((q => r) => (p => r)) in HP_TAUT by Th21; hence (q => r) => (p => r) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem Th23: :: HILBERT1:23 for p, q, r being Element of HP-WFF st p => q in HP_TAUT & q => r in HP_TAUT holds p => r in HP_TAUT proof let p, q, r be Element of HP-WFF ; ::_thesis: ( p => q in HP_TAUT & q => r in HP_TAUT implies p => r in HP_TAUT ) assume that A1: p => q in HP_TAUT and A2: q => r in HP_TAUT ; ::_thesis: p => 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 p => r in HP_TAUT by A2, Def10; ::_thesis: verum end; Lm4: for q, r, p, s being Element of HP-WFF holds (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT proof let q, r, p, s be Element of HP-WFF ; ::_thesis: (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT (p => q) => ((q => r) => (p => r)) in HP_TAUT by Th21; hence (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT by Th22; ::_thesis: verum end; theorem Th24: :: HILBERT1:24 for p, q, r, s being Element of HP-WFF holds (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT proof let p, q, r, s be Element of HP-WFF ; ::_thesis: (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT 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 (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem :: HILBERT1:25 for p, q, r being Element of HP-WFF holds ((p => q) => r) => (q => r) in HP_TAUT proof let p, q, r be Element of HP-WFF ; ::_thesis: ((p => q) => r) => (q => r) in HP_TAUT A1: (q => (p => q)) => (((p => q) => r) => (q => r)) in HP_TAUT by Th21; q => (p => q) in HP_TAUT by Def10; hence ((p => q) => r) => (q => r) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem Th26: :: HILBERT1:26 for p, q, r being Element of HP-WFF holds (p => (q => r)) => (q => (p => r)) in HP_TAUT proof let p, q, r be Element of HP-WFF ; ::_thesis: (p => (q => r)) => (q => (p => r)) in HP_TAUT 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 (p => (q => r)) => (q => (p => r)) in HP_TAUT by Th20; ::_thesis: verum end; theorem Th27: :: HILBERT1:27 for p, q being Element of HP-WFF holds (p => (p => q)) => (p => q) in HP_TAUT proof let p, q be Element of HP-WFF ; ::_thesis: (p => (p => q)) => (p => q) in HP_TAUT (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 (p => (p => q)) => (p => q) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem :: HILBERT1:28 for q, p being Element of HP-WFF holds q => ((q => p) => p) in HP_TAUT proof let q, p be Element of HP-WFF ; ::_thesis: q => ((q => p) => p) in HP_TAUT A1: ((q => p) => (q => p)) => (q => ((q => p) => p)) in HP_TAUT by Th26; (q => p) => (q => p) in HP_TAUT by Th14; hence q => ((q => p) => p) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem Th29: :: HILBERT1:29 for s, q, p being Element of HP-WFF st s => (q => p) in HP_TAUT & q in HP_TAUT holds s => p in HP_TAUT proof let s, q, p be Element of HP-WFF ; ::_thesis: ( s => (q => p) in HP_TAUT & q in HP_TAUT implies s => p in HP_TAUT ) assume that A1: s => (q => p) in HP_TAUT and A2: q in HP_TAUT ; ::_thesis: s => p 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 s => p in HP_TAUT by A2, Def10; ::_thesis: verum end; begin theorem Th30: :: HILBERT1:30 for p being Element of HP-WFF holds p => (p '&' p) in HP_TAUT proof let p be Element of HP-WFF ; ::_thesis: p => (p '&' p) in HP_TAUT A1: (p => (p => (p '&' p))) => (p => (p '&' p)) in HP_TAUT by Th27; p => (p => (p '&' p)) in HP_TAUT by Def10; hence p => (p '&' p) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem Th31: :: HILBERT1:31 for p, q being Element of HP-WFF holds ( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) ) proof let p, q be Element of HP-WFF ; ::_thesis: ( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) ) hereby ::_thesis: ( p in HP_TAUT & q in HP_TAUT implies p '&' q in HP_TAUT ) A1: (p '&' q) => q in HP_TAUT by Def10; assume A2: p '&' q in HP_TAUT ; ::_thesis: ( p in HP_TAUT & 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; ::_thesis: verum end; assume that A3: p in HP_TAUT and A4: q in HP_TAUT ; ::_thesis: p '&' q in HP_TAUT p => (q => (p '&' q)) in HP_TAUT by Def10; then q => (p '&' q) in HP_TAUT by A3, Def10; hence p '&' q in HP_TAUT by A4, Def10; ::_thesis: verum end; theorem :: HILBERT1:32 for p, q being Element of HP-WFF st p '&' q in HP_TAUT holds q '&' p in HP_TAUT proof let p, q be Element of HP-WFF ; ::_thesis: ( p '&' q in HP_TAUT implies q '&' p in HP_TAUT ) assume A1: p '&' q in HP_TAUT ; ::_thesis: q '&' p in HP_TAUT then A2: q in HP_TAUT by Th31; p in HP_TAUT by A1, Th31; hence q '&' p in HP_TAUT by A2, Th31; ::_thesis: verum end; theorem Th33: :: HILBERT1:33 for p, q, r being Element of HP-WFF holds ((p '&' q) => r) => (p => (q => r)) in HP_TAUT proof let p, q, r be Element of HP-WFF ; ::_thesis: ((p '&' q) => r) => (p => (q => r)) in HP_TAUT set qp = q => (p '&' q); set pr = ((p '&' q) => r) => (q => r); A1: (p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r)))) => ((p => (q => (p '&' q))) => (p => (((p '&' q) => r) => (q => r)))) 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 => (q => (p '&' q))) => (p => (((p '&' q) => r) => (q => r))) 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 ((p '&' q) => r) => (p => (q => r)) in HP_TAUT by A3, Def10; ::_thesis: verum end; theorem Th34: :: HILBERT1:34 for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p '&' q) => r) in HP_TAUT proof let p, q, r be Element of HP-WFF ; ::_thesis: (p => (q => r)) => ((p '&' q) => r) in HP_TAUT 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 (p => (q => r)) => ((p '&' q) => r) in HP_TAUT by A4, Th23; ::_thesis: verum end; theorem Th35: :: HILBERT1:35 for r, p, q being Element of HP-WFF holds (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT proof let r, p, q be Element of HP-WFF ; ::_thesis: (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT 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 (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT by A1, Th23; ::_thesis: verum end; theorem Th36: :: HILBERT1:36 for p, q being Element of HP-WFF holds ((p => q) '&' p) => q in HP_TAUT proof let p, q be Element of HP-WFF ; ::_thesis: ((p => q) '&' p) => q in HP_TAUT set P = p => q; A1: (p => q) => (p => q) in HP_TAUT by Th14; ((p => q) => (p => q)) => (((p => q) '&' p) => q) in HP_TAUT by Th34; hence ((p => q) '&' p) => q in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem :: HILBERT1:37 for p, q, s being Element of HP-WFF holds (((p => q) '&' p) '&' s) => q in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (((p => q) '&' p) '&' s) => q in HP_TAUT set P = (p => q) '&' p; A1: ((p => q) '&' p) => q in HP_TAUT by Th36; (((p => q) '&' p) '&' s) => ((p => q) '&' p) in HP_TAUT by Def10; hence (((p => q) '&' p) '&' s) => q in HP_TAUT by A1, Th23; ::_thesis: verum end; theorem :: HILBERT1:38 for q, s, p being Element of HP-WFF holds (q => s) => ((p '&' q) => s) in HP_TAUT proof let q, s, p be Element of HP-WFF ; ::_thesis: (q => s) => ((p '&' q) => s) in HP_TAUT set P = p '&' q; A1: (p '&' q) => q in HP_TAUT by Def10; ((p '&' q) => q) => ((q => s) => ((p '&' q) => s)) in HP_TAUT by Th21; hence (q => s) => ((p '&' q) => s) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem Th39: :: HILBERT1:39 for q, s, p being Element of HP-WFF holds (q => s) => ((q '&' p) => s) in HP_TAUT proof let q, s, p be Element of HP-WFF ; ::_thesis: (q => s) => ((q '&' p) => s) in HP_TAUT set P = q '&' p; A1: (q '&' p) => q in HP_TAUT by Def10; ((q '&' p) => q) => ((q => s) => ((q '&' p) => s)) in HP_TAUT by Th21; hence (q => s) => ((q '&' p) => s) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem Th40: :: HILBERT1:40 for p, s, q being Element of HP-WFF holds ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT proof let p, s, q be Element of HP-WFF ; ::_thesis: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT set P = p '&' s; A1: ((p '&' s) => q) => (((p '&' s) => s) => ((p '&' s) => (q '&' s))) in HP_TAUT by Th35; (p '&' s) => s in HP_TAUT by Def10; hence ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by A1, Th29; ::_thesis: verum end; theorem Th41: :: HILBERT1:41 for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT A1: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by Th40; (p => q) => ((p '&' s) => q) in HP_TAUT by Th39; hence (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by A1, Th23; ::_thesis: verum end; theorem Th42: :: HILBERT1:42 for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT set P = p => q; set Q = p '&' s; set S = q '&' s; A1: (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by Th41; ((p => q) => ((p '&' s) => (q '&' s))) => (((p => q) '&' (p '&' s)) => (q '&' s)) in HP_TAUT by Th34; hence ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem Th43: :: HILBERT1:43 for p, q being Element of HP-WFF holds (p '&' q) => (q '&' p) in HP_TAUT proof let p, q be Element of HP-WFF ; ::_thesis: (p '&' q) => (q '&' p) in HP_TAUT set P = p '&' q; A1: (p '&' q) => q in HP_TAUT by Def10; A2: (p '&' q) => p in HP_TAUT by Def10; ((p '&' q) => q) => (((p '&' q) => p) => ((p '&' q) => (q '&' p))) in HP_TAUT by Th35; then ((p '&' q) => p) => ((p '&' q) => (q '&' p)) in HP_TAUT by A1, Def10; hence (p '&' q) => (q '&' p) in HP_TAUT by A2, Def10; ::_thesis: verum end; theorem Th44: :: HILBERT1:44 for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT A1: (q '&' s) => (s '&' q) in HP_TAUT by Th43; ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT by Th42; hence ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum end; theorem Th45: :: HILBERT1:45 for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT set P = p => q; set Q = p '&' s; set S = s '&' q; A1: ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT by Th44; (((p => q) '&' (p '&' s)) => (s '&' q)) => ((p => q) => ((p '&' s) => (s '&' q))) in HP_TAUT by Th33; hence (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem Th46: :: HILBERT1:46 for p, q, s being Element of HP-WFF holds (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT set P = p => q; set Q = p '&' s; set S = s '&' q; set T = s '&' p; A1: (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT by Th45; A2: (s '&' p) => (p '&' s) in HP_TAUT by Th43; ((p => q) => ((p '&' s) => (s '&' q))) => (((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q)))) in HP_TAUT by Th24; then ((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q))) in HP_TAUT by A1, Def10; hence (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT by A2, Def10; ::_thesis: verum end; theorem :: HILBERT1:47 for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT proof let p, s, q be Element of HP-WFF ; ::_thesis: (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT set P = s '&' q; set Q = q '&' s; A1: (s '&' q) => (q '&' s) in HP_TAUT by Th43; ((s '&' q) => (q '&' s)) => ((p '&' (s '&' q)) => (p '&' (q '&' s))) in HP_TAUT by Th46; hence (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem :: HILBERT1:48 for p, q, s being Element of HP-WFF holds ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT set P = p => q; set Q = p => s; set S = p => (q '&' s); A1: (p => q) => ((p => s) => (p => (q '&' s))) in HP_TAUT by Th35; ((p => q) => ((p => s) => (p => (q '&' s)))) => (((p => q) '&' (p => s)) => (p => (q '&' s))) in HP_TAUT by Th34; hence ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT by A1, Def10; ::_thesis: verum end; Lm5: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => q in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => q in HP_TAUT A1: (p '&' q) => q in HP_TAUT by Def10; ((p '&' q) '&' s) => (p '&' q) in HP_TAUT by Def10; hence ((p '&' q) '&' s) => q in HP_TAUT by A1, Th23; ::_thesis: verum end; Lm6: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT set P = (p '&' q) '&' s; A1: ((p '&' q) '&' s) => q in HP_TAUT by Lm5; (((p '&' q) '&' s) => q) => ((((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q)) in HP_TAUT by Th46; hence (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT by A1, Def10; ::_thesis: verum end; Lm7: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT 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 ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum end; Lm8: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' s) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (p '&' s) in HP_TAUT set P = p '&' q; A1: (p '&' q) => p in HP_TAUT by Def10; ((p '&' q) => p) => (((p '&' q) '&' s) => (p '&' s)) in HP_TAUT by Th41; hence ((p '&' q) '&' s) => (p '&' s) in HP_TAUT by A1, Def10; ::_thesis: verum end; Lm9: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT set P = (p '&' q) '&' s; set Q = p '&' s; A1: ((p '&' q) '&' s) => (p '&' s) in HP_TAUT by Lm8; (((p '&' q) '&' s) => (p '&' s)) => ((((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q)) in HP_TAUT by Th41; hence (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT by A1, Def10; ::_thesis: verum end; Lm10: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT 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 ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum end; Lm11: for p, s, q being Element of HP-WFF holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT proof let p, s, q be Element of HP-WFF ; ::_thesis: ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT set P = p '&' s; set Q = s '&' p; A1: (p '&' s) => (s '&' p) in HP_TAUT by Th43; ((p '&' s) => (s '&' p)) => (((p '&' s) '&' q) => ((s '&' p) '&' q)) in HP_TAUT by Th41; hence ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT by A1, Def10; ::_thesis: verum end; Lm12: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT A1: ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT by Lm11; ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT by Lm10; hence ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum end; Lm13: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT A1: ((s '&' p) '&' q) => ((s '&' q) '&' p) in HP_TAUT by Lm10; ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT by Lm12; hence ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT by A1, Th23; ::_thesis: verum end; Lm14: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT A1: ((s '&' q) '&' p) => (p '&' (s '&' q)) in HP_TAUT by Th43; ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT by Lm13; hence ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT by A1, Th23; ::_thesis: verum end; Lm15: for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT proof let p, s, q be Element of HP-WFF ; ::_thesis: (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT set P = s '&' q; set Q = q '&' s; A1: (s '&' q) => (q '&' s) in HP_TAUT by Th43; ((s '&' q) => (q '&' s)) => ((p '&' (s '&' q)) => (p '&' (q '&' s))) in HP_TAUT by Th46; hence (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem :: HILBERT1:49 for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT A1: (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT by Lm15; ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT by Lm14; hence ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT by A1, Th23; ::_thesis: verum end; Lm16: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT A1: (p '&' (s '&' q)) => ((s '&' q) '&' p) in HP_TAUT by Th43; (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT by Lm15; hence (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT by A1, Th23; ::_thesis: verum end; Lm17: for s, q, p being Element of HP-WFF holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT proof let s, q, p be Element of HP-WFF ; ::_thesis: ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT set P = s '&' q; set Q = q '&' s; A1: (s '&' q) => (q '&' s) in HP_TAUT by Th43; ((s '&' q) => (q '&' s)) => (((s '&' q) '&' p) => ((q '&' s) '&' p)) in HP_TAUT by Th41; hence ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT by A1, Def10; ::_thesis: verum end; Lm18: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT A1: ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT by Lm17; (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT by Lm16; hence (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT by A1, Th23; ::_thesis: verum end; Lm19: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT A1: ((q '&' s) '&' p) => ((p '&' s) '&' q) in HP_TAUT by Lm13; (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT by Lm18; hence (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum end; Lm20: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT set P = q '&' s; set Q = s '&' q; A1: (q '&' s) => (s '&' q) in HP_TAUT by Th43; ((q '&' s) => (s '&' q)) => ((p '&' (q '&' s)) => (p '&' (s '&' q))) in HP_TAUT by Th46; hence (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT by A1, Def10; ::_thesis: verum end; theorem :: HILBERT1:50 for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT proof let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT A1: (p '&' (s '&' q)) => ((p '&' q) '&' s) in HP_TAUT by Lm19; (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT by Lm20; hence (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT by A1, Th23; ::_thesis: verum end;