:: Hilbert Positive Propositional Calculus :: by Adam Grabowski :: :: Received February 20, 1999 :: Copyright (c) 1999-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI, RELAT_1, XBOOLE_0, FUNCT_1, QC_LANG1, XBOOLEAN, HILBERT1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, FINSEQ_1; constructors NAT_1, FINSEQ_1, NUMBERS; registrations SUBSET_1, ORDINAL1, FUNCT_1, FINSEQ_1, XCMPLX_0; requirements NUMERALS, BOOLE, SUBSET; definitions TARSKI; expansions TARSKI; theorems TARSKI, FINSEQ_1, XBOOLE_0, XBOOLE_1; schemes XFAMILY; begin :: Definition of the language definition let D be set; attr D is with_VERUM means :Def1: <*0*> in D; end; definition let D be set; attr D is with_implication means :Def2: for p, q being FinSequence st p in D & q in D holds <*1*>^p^q in D; end; definition let D be set; attr D is with_conjunction means :Def3: for p, q being FinSequence st p in D & q in D holds <*2*>^p^q in D; end; definition let D be set; attr D is with_propositional_variables means :Def4: for n being Element of NAT holds <*3+n*> in D; end; definition let D be set; 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 func HP-WFF -> set means :Def6: it is HP-closed & for D being 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 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* & P[x] from XFAMILY: sch 1; A3: for D being 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 being 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 being 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 being 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 being 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 being 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 being 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 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; 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 func VERUM -> HP-formula equals <*0*>; correctness by Def1; let p, q be Element of HP-WFF; func p => q -> HP-formula equals <*1*>^p^q; coherence by Def2; 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; attr T is Hilbert_theory means :Def10: 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; definition let X; 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 being set such that A1: for a being 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 being 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 func HP_TAUT -> Subset of HP-WFF equals CnPos({}(HP-WFF)); correctness; end; theorem Th1: VERUM in CnPos (X) proof T is Hilbert_theory & X c= T implies VERUM in T; hence thesis by Def11; end; theorem 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 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 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 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 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 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 Th8: T is Hilbert_theory & X c= T implies CnPos(X) c= T by Def11; theorem 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 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 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 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 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 :: The tautologies of the Hilbert calculus - implicational part theorem 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 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 p => VERUM in HP_TAUT by Th1,Th15; theorem (p => q) => (p => p) in HP_TAUT by Th14,Th15; theorem (q => p) => (p => p) in HP_TAUT by Th14,Th15; theorem 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 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 Th21: :: Hypothetical syllogism (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 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 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 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 ((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 Th26: :: Contraposition (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 Th27: :: A Hilbert axiom (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 :: Modus ponendo ponens 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 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 :: Conjunctional part of the calculus theorem 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 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 (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 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 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 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 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 (( (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 (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 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 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 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 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 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 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 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 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 ( 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 ( ( 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 (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 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;