:: Hilbert Positive Propositional Calculus :: by Adam Grabowski :: :: Received February 20, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users 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 proofend; 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 ) ) proofend; 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 proofend; 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 ) proofend; end; registration cluster HP-WFF -> functional ; coherence HP-WFF is functional proofend; end; registration cluster -> FinSequence-like for Element of HP-WFF ; coherence for b1 being Element of HP-WFF holds b1 is FinSequence-like proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th9: :: HILBERT1:9 for X being Subset of HP-WFF holds X c= CnPos X proofend; theorem Th10: :: HILBERT1:10 for X, Y being Subset of HP-WFF st X c= Y holds CnPos X c= CnPos Y proofend; Lm2: for X being Subset of HP-WFF holds CnPos (CnPos X) c= CnPos X proofend; theorem :: HILBERT1:11 for X being Subset of HP-WFF holds CnPos (CnPos X) = CnPos X proofend; Lm3: for X being Subset of HP-WFF holds CnPos X is Hilbert_theory proofend; 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 ) proofend; theorem :: HILBERT1:13 for T being Subset of HP-WFF st T is Hilbert_theory holds HP_TAUT c= T proofend; 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 proofend; theorem Th15: :: HILBERT1:15 for q, p being Element of HP-WFF st q in HP_TAUT holds p => q in HP_TAUT proofend; 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 proofend; 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 proofend; theorem Th21: :: HILBERT1:21 for p, q, r being Element of HP-WFF holds (p => q) => ((q => r) => (p => r)) in HP_TAUT proofend; 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 proofend; 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 proofend; Lm4: for q, r, p, s being Element of HP-WFF holds (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT proofend; 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 proofend; theorem :: HILBERT1:25 for p, q, r being Element of HP-WFF holds ((p => q) => r) => (q => r) in HP_TAUT proofend; theorem Th26: :: HILBERT1:26 for p, q, r being Element of HP-WFF holds (p => (q => r)) => (q => (p => r)) in HP_TAUT proofend; theorem Th27: :: HILBERT1:27 for p, q being Element of HP-WFF holds (p => (p => q)) => (p => q) in HP_TAUT proofend; theorem :: HILBERT1:28 for q, p being Element of HP-WFF holds q => ((q => p) => p) in HP_TAUT proofend; 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 proofend; begin theorem Th30: :: HILBERT1:30 for p being Element of HP-WFF holds p => (p '&' p) in HP_TAUT proofend; 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 ) ) proofend; theorem :: HILBERT1:32 for p, q being Element of HP-WFF st p '&' q in HP_TAUT holds q '&' p in HP_TAUT proofend; theorem Th33: :: HILBERT1:33 for p, q, r being Element of HP-WFF holds ((p '&' q) => r) => (p => (q => r)) in HP_TAUT proofend; theorem Th34: :: HILBERT1:34 for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p '&' q) => r) in HP_TAUT proofend; theorem Th35: :: HILBERT1:35 for r, p, q being Element of HP-WFF holds (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT proofend; theorem Th36: :: HILBERT1:36 for p, q being Element of HP-WFF holds ((p => q) '&' p) => q in HP_TAUT proofend; theorem :: HILBERT1:37 for p, q, s being Element of HP-WFF holds (((p => q) '&' p) '&' s) => q in HP_TAUT proofend; theorem :: HILBERT1:38 for q, s, p being Element of HP-WFF holds (q => s) => ((p '&' q) => s) in HP_TAUT proofend; theorem Th39: :: HILBERT1:39 for q, s, p being Element of HP-WFF holds (q => s) => ((q '&' p) => s) in HP_TAUT proofend; theorem Th40: :: HILBERT1:40 for p, s, q being Element of HP-WFF holds ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT proofend; theorem Th41: :: HILBERT1:41 for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT proofend; theorem Th42: :: HILBERT1:42 for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT proofend; theorem Th43: :: HILBERT1:43 for p, q being Element of HP-WFF holds (p '&' q) => (q '&' p) in HP_TAUT proofend; theorem Th44: :: HILBERT1:44 for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT proofend; theorem Th45: :: HILBERT1:45 for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT proofend; theorem Th46: :: HILBERT1:46 for p, q, s being Element of HP-WFF holds (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT proofend; theorem :: HILBERT1:47 for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT proofend; theorem :: HILBERT1:48 for p, q, s being Element of HP-WFF holds ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT proofend; Lm5: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => q in HP_TAUT proofend; Lm6: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT proofend; Lm7: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT proofend; Lm8: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' s) in HP_TAUT proofend; Lm9: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT proofend; Lm10: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT proofend; Lm11: for p, s, q being Element of HP-WFF holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT proofend; Lm12: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT proofend; Lm13: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT proofend; Lm14: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT proofend; Lm15: for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT proofend; theorem :: HILBERT1:49 for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT proofend; Lm16: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT proofend; Lm17: for s, q, p being Element of HP-WFF holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT proofend; Lm18: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT proofend; Lm19: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT proofend; Lm20: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT proofend; theorem :: HILBERT1:50 for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT proofend;