:: Intuitionistic Propositional Calculus in the Extended Framework with Modal :: Operator, Part I :: by Takao Inou\'e :: :: Received April 3, 2003 :: Copyright (c) 2003-2021 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, RELAT_1, TARSKI, XBOOLE_0, FUNCT_1, QC_LANG2, XBOOLEAN, INTPRO_1; 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; requirements NUMERALS, BOOLE, SUBSET; begin :: Intuitionistic propositional calculus IPC in the extended :: language with modal operator definition let E be set; attr E is with_FALSUM means :: INTPRO_1:def 1 <*0*>in E; end; definition let E be set; attr E is with_int_implication means :: INTPRO_1:def 2 for p, q being FinSequence st p in E & q in E holds <*1*>^p^q in E; end; definition let E be set; attr E is with_int_conjunction means :: INTPRO_1:def 3 for p, q being FinSequence st p in E & q in E holds <*2*>^p^q in E; end; definition let E be set; attr E is with_int_disjunction means :: INTPRO_1:def 4 for p, q being FinSequence st p in E & q in E holds <*3*>^p^q in E; end; definition let E be set; attr E is with_int_propositional_variables means :: INTPRO_1:def 5 for n being Element of NAT holds <* 5+2*n *> in E; end; definition let E be set; attr E is with_modal_operator means :: INTPRO_1:def 6 for p being FinSequence st p in E holds <*6*>^p in E; end; :: We reserve <*4*> for verum for a possible formulation. :: So do we <* 5+2*n+1 *> for every n >= 1 for introduction of a number of :: other logical connectives (e.g. for polymodal logics, :: hybrid logics, recent computer-oriented logics and so on). definition let E be set; attr E is MC-closed means :: INTPRO_1:def 7 E c= NAT* & E is with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator; end; registration cluster MC-closed -> with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator non empty for set; cluster with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator -> MC-closed for Subset of NAT*; end; definition func MC-wff -> set means :: INTPRO_1:def 8 it is MC-closed & for E being set st E is MC-closed holds it c= E; end; registration cluster MC-wff -> MC-closed; end; registration cluster MC-closed non empty for set; end; registration cluster MC-wff -> functional; end; registration cluster -> FinSequence-like for Element of MC-wff; end; definition mode MC-formula is Element of MC-wff; end; definition func FALSUM -> MC-formula equals :: INTPRO_1:def 9 <*0*>; let p, q be Element of MC-wff; func p => q -> MC-formula equals :: INTPRO_1:def 10 <*1*>^p^q; func p '&' q -> MC-formula equals :: INTPRO_1:def 11 <*2*>^p^q; func p 'or' q -> MC-formula equals :: INTPRO_1:def 12 <*3*>^p^q; end; definition let p be Element of MC-wff; func Nes p -> MC-formula equals :: INTPRO_1:def 13 <*6*>^p; end; reserve T, X, Y for Subset of MC-wff; reserve p, q, r, s for Element of MC-wff; definition let T be Subset of MC-wff; attr T is IPC_theory means :: INTPRO_1:def 14 for p, q, r being Element of MC-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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & (p in T & p => q in T implies q in T); end; definition let X; func CnIPC X -> Subset of MC-wff means :: INTPRO_1:def 15 r in it iff for T st T is IPC_theory & X c= T holds r in T; end; definition func IPC-Taut -> Subset of MC-wff equals :: INTPRO_1:def 16 CnIPC({}(MC-wff)); end; definition let p be Element of MC-wff; func neg p -> MC-formula equals :: INTPRO_1:def 17 (p => FALSUM); end; definition func IVERUM -> MC-formula equals :: INTPRO_1:def 18 (FALSUM => FALSUM); end; theorem :: INTPRO_1:1 p => (q => p) in CnIPC (X); theorem :: INTPRO_1:2 (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X); theorem :: INTPRO_1:3 p '&' q => p in CnIPC(X); theorem :: INTPRO_1:4 p '&' q => q in CnIPC(X); theorem :: INTPRO_1:5 p => (q => (p '&' q)) in CnIPC (X); theorem :: INTPRO_1:6 p => (p 'or' q) in CnIPC (X); theorem :: INTPRO_1:7 q => (p 'or' q) in CnIPC (X); theorem :: INTPRO_1:8 (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X); theorem :: INTPRO_1:9 FALSUM => p in CnIPC (X); theorem :: INTPRO_1:10 p in CnIPC(X) & p => q in CnIPC(X) implies q in CnIPC(X); theorem :: INTPRO_1:11 T is IPC_theory & X c= T implies CnIPC(X) c= T; theorem :: INTPRO_1:12 X c= CnIPC(X); theorem :: INTPRO_1:13 X c= Y implies CnIPC(X) c= CnIPC(Y); theorem :: INTPRO_1:14 CnIPC(CnIPC(X)) = CnIPC(X); registration let X be Subset of MC-wff; cluster CnIPC(X) -> IPC_theory; end; theorem :: INTPRO_1:15 T is IPC_theory iff CnIPC(T) = T; theorem :: INTPRO_1:16 T is IPC_theory implies IPC-Taut c= T; registration cluster IPC-Taut -> IPC_theory; end; begin :: Formulas provable in IPC : implication theorem :: INTPRO_1:17 p => p in IPC-Taut; theorem :: INTPRO_1:18 q in IPC-Taut implies p => q in IPC-Taut; theorem :: INTPRO_1:19 IVERUM in IPC-Taut; theorem :: INTPRO_1:20 (p => q) => (p => p) in IPC-Taut; theorem :: INTPRO_1:21 (q => p) => (p => p) in IPC-Taut; theorem :: INTPRO_1:22 (q => r) => ((p => q) => (p => r)) in IPC-Taut; theorem :: INTPRO_1:23 p => (q => r) in IPC-Taut implies q => (p => r) in IPC-Taut; theorem :: INTPRO_1:24 :: Hypothetical syllogism (p => q) => ((q => r) => (p => r)) in IPC-Taut; theorem :: INTPRO_1:25 p => q in IPC-Taut implies (q => r) => (p => r) in IPC-Taut; theorem :: INTPRO_1:26 p => q in IPC-Taut & q => r in IPC-Taut implies p => r in IPC-Taut; theorem :: INTPRO_1:27 (p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut; theorem :: INTPRO_1:28 ((p => q) => r) => (q => r) in IPC-Taut; theorem :: INTPRO_1:29 :: Contraposition (p => (q => r)) => (q => (p => r)) in IPC-Taut; theorem :: INTPRO_1:30 :: A Hilbert axiom (p => (p => q)) => (p => q) in IPC-Taut; theorem :: INTPRO_1:31 :: Modus ponendo ponens q => ((q => p) => p) in IPC-Taut; theorem :: INTPRO_1:32 s => (q => p) in IPC-Taut & q in IPC-Taut implies s => p in IPC-Taut; begin :: Formulas provable in IPC : conjunction theorem :: INTPRO_1:33 p => (p '&' p) in IPC-Taut; theorem :: INTPRO_1:34 (p '&' q) in IPC-Taut iff p in IPC-Taut & q in IPC-Taut; theorem :: INTPRO_1:35 (p '&' q) in IPC-Taut iff (q '&' p) in IPC-Taut; theorem :: INTPRO_1:36 (( p '&' q ) => r ) => ( p => ( q => r )) in IPC-Taut; theorem :: INTPRO_1:37 ( p => ( q => r )) => (( p '&' q ) => r ) in IPC-Taut; theorem :: INTPRO_1:38 ( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in IPC-Taut; theorem :: INTPRO_1:39 ( (p => q) '&' p ) => q in IPC-Taut; theorem :: INTPRO_1:40 (( (p => q) '&' p ) '&' s ) => q in IPC-Taut; theorem :: INTPRO_1:41 (q => s) => (( p '&' q ) => s) in IPC-Taut; theorem :: INTPRO_1:42 (q => s) => (( q '&' p ) => s) in IPC-Taut; theorem :: INTPRO_1:43 ( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut; theorem :: INTPRO_1:44 ( p => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut; theorem :: INTPRO_1:45 (( p => q ) '&' ( p '&' s )) => ( q '&' s ) in IPC-Taut; theorem :: INTPRO_1:46 ( p '&' q ) => ( q '&' p ) in IPC-Taut; theorem :: INTPRO_1:47 ( p => q ) '&' ( p '&' s ) => ( s '&' q ) in IPC-Taut; theorem :: INTPRO_1:48 ( p => q ) => (( p '&' s ) => ( s '&' q )) in IPC-Taut; theorem :: INTPRO_1:49 ( p => q ) => (( s '&' p ) => ( s '&' q )) in IPC-Taut; theorem :: INTPRO_1:50 ( p '&' (s '&' q) ) => ( p '&' (q '&' s) ) in IPC-Taut; theorem :: INTPRO_1:51 ( ( p => q ) '&' (p => s) ) => ( p => (q '&' s) ) in IPC-Taut; theorem :: INTPRO_1:52 (p '&' q) '&' s => p '&' (q '&' s) in IPC-Taut; theorem :: INTPRO_1:53 p '&' (q '&' s) => (p '&' q) '&' s in IPC-Taut; begin :: Formulas provable in IPC: disjunction theorem :: INTPRO_1:54 (p 'or' p) => p in IPC-Taut; theorem :: INTPRO_1:55 p in IPC-Taut or q in IPC-Taut implies (p 'or' q) in IPC-Taut; theorem :: INTPRO_1:56 (p 'or' q) => (q 'or' p) in IPC-Taut; theorem :: INTPRO_1:57 (p 'or' q) in IPC-Taut iff (q 'or' p) in IPC-Taut; theorem :: INTPRO_1:58 (p => q) => (p => (q 'or' s)) in IPC-Taut; theorem :: INTPRO_1:59 (p => q) => (p => (s 'or' q)) in IPC-Taut; theorem :: INTPRO_1:60 ( p => q ) => ((p 'or' s) => (q 'or' s)) in IPC-Taut; theorem :: INTPRO_1:61 p => q in IPC-Taut implies (p 'or' s) => (q 'or' s) in IPC-Taut; theorem :: INTPRO_1:62 ( p => q ) => (( s 'or' p ) => ( s 'or' q )) in IPC-Taut; theorem :: INTPRO_1:63 p => q in IPC-Taut implies ( s 'or' p ) => ( s 'or' q ) in IPC-Taut; theorem :: INTPRO_1:64 ( p 'or' (q 'or' s) ) => ( q 'or' (p 'or' s) ) in IPC-Taut; theorem :: INTPRO_1:65 ( p 'or' (q 'or' s) ) => ( (p 'or' q) 'or' s ) in IPC-Taut; theorem :: INTPRO_1:66 ( (p 'or' q) 'or' s ) => ( p 'or' (q 'or' s) ) in IPC-Taut; begin :: Classical propositional calculus CPC reserve T, X, Y for Subset of MC-wff; reserve p, q, r for Element of MC-wff; definition let T be Subset of MC-wff; attr T is CPC_theory means :: INTPRO_1:def 19 for p, q, r being Element of MC-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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & (p in T & p => q in T implies q in T); end; theorem :: INTPRO_1:67 T is CPC_theory implies T is IPC_theory; definition let X; func CnCPC X -> Subset of MC-wff means :: INTPRO_1:def 20 r in it iff for T st T is CPC_theory & X c= T holds r in T; end; definition func CPC-Taut -> Subset of MC-wff equals :: INTPRO_1:def 21 CnCPC({}(MC-wff)); end; theorem :: INTPRO_1:68 CnIPC (X) c= CnCPC (X); theorem :: INTPRO_1:69 p => (q => p) in CnCPC (X) & (p => (q => r)) => ((p => q) => (p => r)) in CnCPC (X) & p '&' q => p in CnCPC (X) & p '&' q => q in CnCPC (X) & p => (q => (p '&' q)) in CnCPC (X) & p => (p 'or' q) in CnCPC (X) & q => (p 'or' q) in CnCPC (X) & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC (X) & FALSUM => p in CnCPC (X) & p 'or' (p => FALSUM) in CnCPC (X); theorem :: INTPRO_1:70 p in CnCPC(X) & p => q in CnCPC(X) implies q in CnCPC(X); theorem :: INTPRO_1:71 T is CPC_theory & X c= T implies CnCPC(X) c= T; theorem :: INTPRO_1:72 X c= CnCPC(X); theorem :: INTPRO_1:73 X c= Y implies CnCPC(X) c= CnCPC(Y); theorem :: INTPRO_1:74 CnCPC(CnCPC(X)) = CnCPC(X); registration let X be Subset of MC-wff; cluster CnCPC(X) -> CPC_theory; end; theorem :: INTPRO_1:75 T is CPC_theory iff CnCPC(T) = T; theorem :: INTPRO_1:76 T is CPC_theory implies CPC-Taut c= T; registration cluster CPC-Taut -> CPC_theory; end; theorem :: INTPRO_1:77 IPC-Taut c= CPC-Taut; begin :: Modal calculus S4 reserve T, X, Y for Subset of MC-wff; reserve p, q, r for Element of MC-wff; definition let T be Subset of MC-wff; attr T is S4_theory means :: INTPRO_1:def 22 for p, q, r being Element of MC-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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & (Nes (p => q)) => ((Nes p) => (Nes q)) in T & (Nes p) => p in T & (Nes p) => Nes (Nes p) in T & (p in T & p => q in T implies q in T) & (p in T implies Nes p in T); end; theorem :: INTPRO_1:78 T is S4_theory implies T is CPC_theory; theorem :: INTPRO_1:79 T is S4_theory implies T is IPC_theory; definition let X; func CnS4 X -> Subset of MC-wff means :: INTPRO_1:def 23 r in it iff for T st T is S4_theory & X c= T holds r in T; end; definition func S4-Taut -> Subset of MC-wff equals :: INTPRO_1:def 24 CnS4({}(MC-wff)); end; theorem :: INTPRO_1:80 CnCPC (X) c= CnS4 (X); theorem :: INTPRO_1:81 CnIPC (X) c= CnS4 (X); theorem :: INTPRO_1:82 p => (q => p) in CnS4 (X) & (p => (q => r)) => ((p => q) => (p => r)) in CnS4 (X) & p '&' q => p in CnS4 (X) & p '&' q => q in CnS4 (X) & p => (q => (p '&' q)) in CnS4 (X) & p => (p 'or' q) in CnS4 (X) & q => (p 'or' q) in CnS4 (X) & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 (X) & FALSUM => p in CnS4 (X) & p 'or' (p => FALSUM) in CnS4 (X); theorem :: INTPRO_1:83 p in CnS4 (X) & p => q in CnS4 (X) implies q in CnS4 (X); theorem :: INTPRO_1:84 (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 (X); theorem :: INTPRO_1:85 (Nes p) => p in CnS4 (X); theorem :: INTPRO_1:86 (Nes p) => Nes (Nes p) in CnS4 (X); theorem :: INTPRO_1:87 p in CnS4 (X) implies Nes p in CnS4 (X); theorem :: INTPRO_1:88 T is S4_theory & X c= T implies CnS4(X) c= T; theorem :: INTPRO_1:89 X c= CnS4(X); theorem :: INTPRO_1:90 X c= Y implies CnS4(X) c= CnS4(Y); theorem :: INTPRO_1:91 CnS4(CnS4(X)) = CnS4(X); registration let X be Subset of MC-wff; cluster CnS4(X) -> S4_theory; end; theorem :: INTPRO_1:92 T is S4_theory iff CnS4(T) = T; theorem :: INTPRO_1:93 T is S4_theory implies S4-Taut c= T; registration cluster S4-Taut -> S4_theory; end; theorem :: INTPRO_1:94 CPC-Taut c= S4-Taut; theorem :: INTPRO_1:95 IPC-Taut c= S4-Taut;