:: Hilbert Positive Propositional Calculus :: by Adam Grabowski :: :: Received February 20, 1999 :: Copyright (c) 1999-2019 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; begin :: Definition of the language definition let D be set; attr D is with_VERUM means :: HILBERT1:def 1 <*0*> in D; end; definition let D be set; attr D is with_implication means :: HILBERT1:def 2 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 :: HILBERT1:def 3 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 :: HILBERT1:def 4 for n being Element of NAT holds <*3+n*> in D; end; definition let D be set; attr D is HP-closed means :: HILBERT1:def 5 D c= NAT* & D is with_VERUM with_implication with_conjunction with_propositional_variables; end; registration cluster HP-closed -> with_VERUM with_implication with_conjunction with_propositional_variables non empty for set; cluster with_VERUM with_implication with_conjunction with_propositional_variables -> HP-closed for Subset of NAT*; end; definition func HP-WFF -> set means :: HILBERT1:def 6 it is HP-closed & for D being set st D is HP-closed holds it c= D; end; registration cluster HP-WFF -> HP-closed; end; registration cluster HP-closed non empty for set; end; registration cluster HP-WFF -> functional; end; registration cluster -> FinSequence-like for Element of HP-WFF; end; definition mode HP-formula is Element of HP-WFF; end; definition func VERUM -> HP-formula equals :: HILBERT1:def 7 <*0*>; let p, q be Element of HP-WFF; func p => q -> HP-formula equals :: HILBERT1:def 8 <*1*>^p^q; func p '&' q -> HP-formula equals :: HILBERT1:def 9 <*2*>^p^q; 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 :: 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); end; definition let X; func CnPos X -> Subset of HP-WFF means :: HILBERT1:def 11 r in it iff for T st T is Hilbert_theory & X c= T holds r in T; end; definition func HP_TAUT -> Subset of HP-WFF equals :: HILBERT1:def 12 CnPos({}(HP-WFF)); end; theorem :: HILBERT1:1 VERUM in CnPos (X); theorem :: HILBERT1:2 p => (q => (p '&' q)) in CnPos (X); theorem :: HILBERT1:3 (p => (q => r)) => ((p => q) => (p => r)) in CnPos (X); theorem :: HILBERT1:4 p => (q => p) in CnPos (X); theorem :: HILBERT1:5 p '&' q => p in CnPos(X); theorem :: HILBERT1:6 p '&' q => q in CnPos(X); theorem :: HILBERT1:7 p in CnPos(X) & p => q in CnPos(X) implies q in CnPos(X); theorem :: HILBERT1:8 T is Hilbert_theory & X c= T implies CnPos(X) c= T; theorem :: HILBERT1:9 X c= CnPos(X); theorem :: HILBERT1:10 X c= Y implies CnPos(X) c= CnPos(Y); theorem :: HILBERT1:11 CnPos(CnPos(X)) = CnPos(X); registration let X be Subset of HP-WFF; cluster CnPos(X) -> Hilbert_theory; end; theorem :: HILBERT1:12 T is Hilbert_theory iff CnPos(T) = T; theorem :: HILBERT1:13 T is Hilbert_theory implies HP_TAUT c= T; registration cluster HP_TAUT -> Hilbert_theory; end; begin :: The tautologies of the Hilbert calculus - implicational part theorem :: HILBERT1:14 p => p in HP_TAUT; theorem :: HILBERT1:15 q in HP_TAUT implies p => q in HP_TAUT; theorem :: HILBERT1:16 p => VERUM in HP_TAUT; theorem :: HILBERT1:17 (p => q) => (p => p) in HP_TAUT; theorem :: HILBERT1:18 (q => p) => (p => p) in HP_TAUT; theorem :: HILBERT1:19 (q => r) => ((p => q) => (p => r)) in HP_TAUT; theorem :: HILBERT1:20 p => (q => r) in HP_TAUT implies q => (p => r) in HP_TAUT; theorem :: HILBERT1:21 :: Hypothetical syllogism (p => q) => ((q => r) => (p => r)) in HP_TAUT; theorem :: HILBERT1:22 p => q in HP_TAUT implies (q => r) => (p => r) in HP_TAUT; theorem :: HILBERT1:23 p => q in HP_TAUT & q => r in HP_TAUT implies p => r in HP_TAUT; theorem :: HILBERT1:24 (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT; theorem :: HILBERT1:25 ((p => q) => r) => (q => r) in HP_TAUT; theorem :: HILBERT1:26 :: Contraposition (p => (q => r)) => (q => (p => r)) in HP_TAUT; theorem :: HILBERT1:27 :: A Hilbert axiom (p => (p => q)) => (p => q) in HP_TAUT; theorem :: HILBERT1:28 :: Modus ponendo ponens q => ((q => p) => p) in HP_TAUT; theorem :: HILBERT1:29 s => (q => p) in HP_TAUT & q in HP_TAUT implies s => p in HP_TAUT; begin :: Conjunctional part of the calculus theorem :: HILBERT1:30 p => (p '&' p) in HP_TAUT; theorem :: HILBERT1:31 (p '&' q) in HP_TAUT iff p in HP_TAUT & q in HP_TAUT; theorem :: HILBERT1:32 (p '&' q) in HP_TAUT implies (q '&' p) in HP_TAUT; theorem :: HILBERT1:33 (( p '&' q ) => r ) => ( p => ( q => r )) in HP_TAUT; theorem :: HILBERT1:34 ( p => ( q => r )) => (( p '&' q ) => r ) in HP_TAUT; theorem :: HILBERT1:35 ( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in HP_TAUT; theorem :: HILBERT1:36 ( (p => q) '&' p ) => q in HP_TAUT; theorem :: HILBERT1:37 (( (p => q) '&' p ) '&' s ) => q in HP_TAUT; theorem :: HILBERT1:38 (q => s) => (( p '&' q ) => s) in HP_TAUT; theorem :: HILBERT1:39 (q => s) => (( q '&' p ) => s) in HP_TAUT; theorem :: HILBERT1:40 ( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in HP_TAUT; theorem :: HILBERT1:41 ( p => q ) => ((p '&' s) => (q '&' s)) in HP_TAUT; theorem :: HILBERT1:42 ( p => q ) '&' ( p '&' s ) => ( q '&' s ) in HP_TAUT; theorem :: HILBERT1:43 ( p '&' q ) => ( q '&' p ) in HP_TAUT; theorem :: HILBERT1:44 ( p => q ) '&' ( p '&' s ) => ( s '&' q ) in HP_TAUT; theorem :: HILBERT1:45 ( p => q ) => (( p '&' s ) => ( s '&' q )) in HP_TAUT; theorem :: HILBERT1:46 ( p => q ) => (( s '&' p ) => ( s '&' q )) in HP_TAUT; theorem :: HILBERT1:47 ( p '&' (s '&' q) ) => ( p '&' (q '&' s) ) in HP_TAUT; theorem :: HILBERT1:48 ( ( p => q ) '&' (p => s) ) => ( p => (q '&' s) ) in HP_TAUT; theorem :: HILBERT1:49 (p '&' q) '&' s => p '&' (q '&' s) in HP_TAUT; theorem :: HILBERT1:50 p '&' (q '&' s) => (p '&' q) '&' s in HP_TAUT;