:: Introduction to Modal Propositional Logic :: by Alicia de la Cruz :: :: Received September 30, 1991 :: Copyright (c) 1991-2016 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 NUMBERS, SUBSET_1, TREES_2, ZFMISC_1, FINSEQ_1, XBOOLE_0, TREES_1, FUNCT_1, RELAT_1, ORDINAL4, NAT_1, CARD_1, XXREAL_0, PARTFUN1, TARSKI, ORDINAL1, ARYTM_3, FINSET_1, FUNCOP_1, MARGREL1, MCART_1, QC_LANG1, XBOOLEAN, VALUED_1, ZF_LANG, MODAL_1, TREES_3; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, WELLORD2, XCMPLX_0, NAT_1, DOMAIN_1, MCART_1, RELAT_1, FUNCT_1, RELSET_1, FINSEQ_1, FUNCOP_1, FINSEQ_2, FUNCT_2, FINSET_1, PARTFUN1, TREES_1, TREES_2, XXREAL_0, TREES_3; constructors PARTFUN1, WELLORD2, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, TREES_2, RELSET_1, FUNCOP_1, TREES_3, XTUPLE_0, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, FINSEQ_1, TREES_1, TREES_2, CARD_1, RELSET_1, TREES_3, XTUPLE_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve x,y,x1,x2,z for set, n,m,k for Nat, t1 for (DecoratedTree of [: NAT,NAT :]), w,s,t,u for FinSequence of NAT, D for non empty set; definition let Z be Tree; func Root Z -> Element of Z equals :: MODAL_1:def 1 {}; end; definition let D; let T be DecoratedTree of D; func Root T -> Element of D equals :: MODAL_1:def 2 T.(Root dom T); end; theorem :: MODAL_1:1 n <> m implies not <*n*>,<*m*>^s are_c=-comparable; ::\$CT theorem :: MODAL_1:3 n <> m implies not <*n*> is_a_proper_prefix_of <*m*>^s; ::\$CT 4 theorem :: MODAL_1:8 for Z being Tree,n,m st n <= m & <*m*> in Z holds <*n*> in Z; theorem :: MODAL_1:9 w^t is_a_proper_prefix_of w^s implies t is_a_proper_prefix_of s ; theorem :: MODAL_1:10 t1 in PFuncs(NAT*,[: NAT,NAT :]); theorem :: MODAL_1:11 for Z,Z1,Z2 being Tree,z being Element of Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2; theorem :: MODAL_1:12 for Z,Z1,Z2 being (DecoratedTree of D),z being Element of dom Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2; theorem :: MODAL_1:13 for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 with-replacement (p,Z2), w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds succ v = succ w; theorem :: MODAL_1:14 for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 with-replacement (p,Z2),w being Element of Z1 st v = w & not p,w are_c=-comparable holds succ v = succ w; theorem :: MODAL_1:15 for Z1,Z2 being Tree,p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 with-replacement (p,Z2),w being Element of Z2 st v = p^w holds succ v,succ w are_equipotent; theorem :: MODAL_1:16 for Z1 being Tree,p being FinSequence of NAT st p in Z1 holds for v being Element of Z1,w being Element of Z1|p st v = p^w holds succ v,succ w are_equipotent; theorem :: MODAL_1:17 for Z being finite Tree st branchdeg (Root Z) = 0 holds card Z = 1 & Z = {{}} ; theorem :: MODAL_1:18 for Z being finite Tree st branchdeg (Root Z) = 1 holds succ ( Root Z) = { <*0*> }; theorem :: MODAL_1:19 for Z being finite Tree st branchdeg (Root Z) = 2 holds succ ( Root Z) = { <*0*>,<*1*> }; reserve s9,w9,v9 for Element of NAT*; theorem :: MODAL_1:20 for Z being Tree,o being Element of Z st o <> Root Z holds Z|o,{ o^s9: o^s9 in Z } are_equipotent & not Root Z in { o^w9 : o^w9 in Z }; theorem :: MODAL_1:21 for Z being finite Tree,o being Element of Z st o <> Root Z holds card (Z|o) < card Z; theorem :: MODAL_1:22 for Z being finite Tree,z being Element of Z st succ (Root Z) = {z} holds Z = elementary_tree 1 with-replacement (<*0*>,Z|z); theorem :: MODAL_1:23 for Z being finite (DecoratedTree of D),z be Element of dom Z st succ (Root dom Z) = {z} holds Z = ((elementary_tree 1) --> Root Z) with-replacement (<*0*>,Z|z); theorem :: MODAL_1:24 for Z being Tree,x1,x2 be Element of Z st x1 = <*0*> & x2 = <*1 *> & succ (Root Z) = {x1,x2} holds Z = (elementary_tree 2 with-replacement (<*0 *>,Z|x1)) with-replacement (<*1*>,Z|x2); theorem :: MODAL_1:25 for Z being (DecoratedTree of D),x1,x2 being Element of dom Z st x1 = <*0*> & x2 = <*1*> & succ (Root dom Z) = {x1,x2} holds Z = ((( elementary_tree 2) --> Root Z) with-replacement (<*0*>, Z|x1)) with-replacement (<*1*>,Z|x2); definition func MP-variables -> set equals :: MODAL_1:def 3 [: {3},NAT :]; end; registration cluster MP-variables -> non empty; end; definition mode MP-variable is Element of MP-variables; end; definition func MP-conectives -> set equals :: MODAL_1:def 4 [: {0,1,2},NAT :]; end; registration cluster MP-conectives -> non empty; end; definition mode MP-conective is Element of MP-conectives; end; theorem :: MODAL_1:26 MP-conectives misses MP-variables; reserve p,q for MP-variable; definition let T be finite Tree,v be Element of T; redefine func branchdeg v -> Nat; end; definition func MP-WFF -> DTree-set of [: NAT,NAT :] means :: MODAL_1:def 5 (for x being DecoratedTree of [: NAT,NAT :] st x in it holds x is finite) & for x being finite DecoratedTree of [: NAT,NAT :] holds x in it iff for v being Element of dom x holds branchdeg v <= 2 & (branchdeg v = 0 implies x .v = [0,0] or ex k st x .v = [3,k]) & (branchdeg v = 1 implies x .v = [1,0] or x .v = [1,1]) & (branchdeg v = 2 implies x .v = [2,0]); end; :: [0,0] = VERUM :: [1,0] = negation :: [1,1] = modal operator of necessity :: [2,0] = & definition mode MP-wff is Element of MP-WFF; end; registration cluster -> finite for MP-wff; end; reserve A,A1,B,B1,C,C1 for MP-wff; definition let A; let a be Element of dom A; redefine func A|a -> MP-wff; end; definition let a be Element of MP-conectives; func the_arity_of a -> Nat equals :: MODAL_1:def 6 a`1; end; definition let D be non empty set, T,T1 be (DecoratedTree of D), p be FinSequence of NAT; assume p in dom T; func @(T,p,T1) -> DecoratedTree of D equals :: MODAL_1:def 7 T with-replacement (p,T1); end; theorem :: MODAL_1:27 ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff; theorem :: MODAL_1:28 ((elementary_tree 1)-->[1,1]) with-replacement (<*0*>,A) is MP-wff; theorem :: MODAL_1:29 (((elementary_tree 2)-->[2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff; definition let A; func 'not' A -> MP-wff equals :: MODAL_1:def 8 ((elementary_tree 1)-->[1,0]) with-replacement (<*0*>,A); func (#) A -> MP-wff equals :: MODAL_1:def 9 ((elementary_tree 1)-->[1,1]) with-replacement ( <*0*>,A); let B; func A '&' B -> MP-wff equals :: MODAL_1:def 10 ((((elementary_tree 2)-->[2,0]) with-replacement (<*0*>,A))) with-replacement (<*1*>,B); end; definition let A; func ? A -> MP-wff equals :: MODAL_1:def 11 'not' (#) 'not' A; let B; func A 'or' B -> MP-wff equals :: MODAL_1:def 12 'not'('not' A '&' 'not' B); func A => B -> MP-wff equals :: MODAL_1:def 13 'not'(A '&' 'not' B); end; theorem :: MODAL_1:30 (elementary_tree 0) --> [3,n] is MP-wff; theorem :: MODAL_1:31 (elementary_tree 0) --> [0,0] is MP-wff; definition let p; func @p -> MP-wff equals :: MODAL_1:def 14 (elementary_tree 0) --> p; end; theorem :: MODAL_1:32 @p = @q implies p = q; theorem :: MODAL_1:33 'not' A = 'not' B implies A = B; theorem :: MODAL_1:34 (#)A = (#)B implies A = B; theorem :: MODAL_1:35 (A '&' B) = (A1 '&' B1) implies A = A1 & B = B1; definition func VERUM -> MP-wff equals :: MODAL_1:def 15 (elementary_tree 0) --> [0,0]; end; theorem :: MODAL_1:36 card dom A = 1 implies A = VERUM or ex p st A = @p; theorem :: MODAL_1:37 card dom A >= 2 implies (ex B st A = 'not' B or A = (#)B) or ex B,C st A = B '&' C; theorem :: MODAL_1:38 card dom A < card dom 'not' A; theorem :: MODAL_1:39 card dom A < card dom (#)A; theorem :: MODAL_1:40 card dom A < card dom(A '&' B) & card dom B < card dom (A '&' B); definition let IT be MP-wff; attr IT is atomic means :: MODAL_1:def 16 ex p st IT = @p; attr IT is negative means :: MODAL_1:def 17 ex A st IT = 'not' A; attr IT is necessitive means :: MODAL_1:def 18 ex A st IT = (#) A; attr IT is conjunctive means :: MODAL_1:def 19 ex A,B st IT = A '&' B; end; registration cluster atomic for MP-wff; cluster negative for MP-wff; cluster necessitive for MP-wff; cluster conjunctive for MP-wff; end; scheme :: MODAL_1:sch 1 MPInd { Prop[Element of MP-WFF] }: for A being Element of MP-WFF holds Prop[ A] provided Prop[VERUM] and for p being MP-variable holds Prop[@p] and for A being Element of MP-WFF st Prop[A] holds Prop['not' A] and for A being Element of MP-WFF st Prop[A] holds Prop[(#) A] and for A, B being Element of MP-WFF st Prop[A] & Prop[B] holds Prop[A '&' B]; theorem :: MODAL_1:41 for A being Element of MP-WFF holds A = VERUM or A is atomic MP-wff or A is negative MP-wff or A is necessitive MP-wff or A is conjunctive MP-wff; theorem :: MODAL_1:42 A = VERUM or (ex p st A = @p) or (ex B st A = 'not' B) or (ex B st A = (#) B) or ex B,C st A = B '&' C; theorem :: MODAL_1:43 @p <> 'not' A & @p <> (#)A & @p <> A '&' B; theorem :: MODAL_1:44 'not' A <> (#)B & 'not' A <> B '&' C; theorem :: MODAL_1:45 (#)A <> B '&' C; theorem :: MODAL_1:46 VERUM <> @p & VERUM <> 'not' A & VERUM <> (#)A & VERUM <> A '&' B; scheme :: MODAL_1:sch 2 MPFuncEx{ D() -> non empty set, d() -> Element of D(), F(Element of MP-variables) -> Element of D(), N,H(Element of D()) -> Element of D(), C(( Element of D()),Element of D()) -> Element of D() }: ex f being Function of MP-WFF, D() st f.VERUM = d() & (for p being MP-variable holds f.@p = F(p)) & ( for A being Element of MP-WFF holds f.('not' A) = N(f.A)) & (for A being Element of MP-WFF holds f.((#)A) = H(f.A)) & for A,B being Element of MP-WFF holds f.(A '&' B) = C(f.A,f.B);