:: 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);