:: Introduction to Modal Propositional Logic
:: by Alicia de la Cruz
::
:: Received September 30, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

Lm1:  for m being Element of NAT holds {} is_a_proper_prefix_of <*m*>
proofend;

definition
let Z be Tree;
func Root Z ->  Element of Z equals :: MODAL_1:def 1
 {} ;
coherence
 {} is Element of Z by TREES_1:22;
end;

:: deftheorem  defines Root MODAL_1:def_1_:_
 for Z being Tree holds Root Z = {} ;

definition
let D be non empty set ;
let T be DecoratedTree of D;
func Root T ->  Element of D equals :: MODAL_1:def 2
T . (Root (dom T));
coherence
 T . (Root (dom T)) is Element of D ;
end;

:: deftheorem  defines Root MODAL_1:def_2_:_
 for D being non empty set
for T being DecoratedTree of D holds Root T = T . (Root (dom T));

theorem Th1: :: MODAL_1:1
for n, m being Element of NAT
for s being FinSequence of NAT st n <> m holds
not <*n*>,<*m*> ^ s are_c=-comparable
proofend;

theorem :: MODAL_1:2
for s being FinSequence of NAT st s <> {} holds
ex w being FinSequence of NAT ex n being Element of NAT st s = <*n*> ^ w by FINSEQ_2:130;

theorem Th3: :: MODAL_1:3
for n, m being Element of NAT
for s being FinSequence of NAT st n <> m holds
not <*n*> is_a_proper_prefix_of <*m*> ^ s
proofend;

theorem :: MODAL_1:4
for n, m being Element of NAT
for s being FinSequence of NAT st n <> m holds
not <*n*> is_a_prefix_of <*m*> ^ s by TREES_1:50;

theorem :: MODAL_1:5
for n, m being Element of NAT holds not <*n*> is_a_proper_prefix_of <*m*> by TREES_1:52;

theorem :: MODAL_1:6
elementary_tree 1 = {{},<*0*>} by TREES_1:51;

theorem :: MODAL_1:7
elementary_tree 2 = {{},<*0*>,<*1*>} by TREES_1:53;

theorem Th8: :: MODAL_1:8
for Z being Tree
for n, m being Element of NAT st n <= m &amp; <*m*> in Z holds
<*n*> in Z
proofend;

theorem :: MODAL_1:9
for w, t, s being FinSequence of NAT st w ^ t is_a_proper_prefix_of w ^ s holds
t is_a_proper_prefix_of s by TREES_1:49;

theorem Th10: :: MODAL_1:10
for t1 being DecoratedTree of [:NAT,NAT:] holds t1 in PFuncs ((NAT *),[:NAT,NAT:])
proofend;

theorem Th11: :: MODAL_1:11
for Z, Z1, Z2 being Tree
for z being Element of Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds
Z1 = Z2
proofend;

theorem Th12: :: MODAL_1:12
for D being non empty set
for Z, Z1, Z2 being DecoratedTree of D
for z being Element of dom Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds
Z1 = Z2
proofend;

theorem Th13: :: MODAL_1:13
for Z1, Z2 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z1 st v = w &amp; w is_a_proper_prefix_of p holds
succ v = succ w
proofend;

theorem Th14: :: MODAL_1:14
for Z1, Z2 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z1 st v = w &amp; not p,w are_c=-comparable holds
succ v = succ w
proofend;

theorem :: MODAL_1:15
for Z1, Z2 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z2 st v = p ^ w holds
succ v, succ w are_equipotent by TREES_2:37;

theorem Th16: :: MODAL_1:16
for Z1 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1
for w being Element of Z1 | p st v = p ^ w holds
succ v, succ w are_equipotent
proofend;

theorem Th17: :: MODAL_1:17
for Z being finite Tree st branchdeg (Root Z) = 0 holds
( card Z = 1 &amp; Z = {{}} )
proofend;

theorem Th18: :: MODAL_1:18
for Z being finite Tree st branchdeg (Root Z) = 1 holds
succ (Root Z) = {<*0*>}
proofend;

theorem Th19: :: MODAL_1:19
for Z being finite Tree st branchdeg (Root Z) = 2 holds
succ (Root Z) = {<*0*>,<*1*>}
proofend;

theorem Th20: :: MODAL_1:20
for Z being Tree
for o being Element of Z st o <> Root Z holds
( Z | o, {  (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z  }  are_equipotent &amp; not Root Z in  {  (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z  }  )
proofend;

theorem Th21: :: MODAL_1:21
for Z being finite Tree
for o being Element of Z st o <> Root Z holds
card (Z | o) < card Z
proofend;

theorem Th22: :: MODAL_1:22
for Z being finite Tree
for z being Element of Z st succ (Root Z) = {z} holds
Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z))
proofend;

Lm2:  for f being Function st dom f is finite holds
f is finite
proofend;

theorem Th23: :: MODAL_1:23
for D being non empty set
for Z being finite DecoratedTree of D
for z being Element of dom Z st succ (Root (dom Z)) = {z} holds
Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))
proofend;

theorem Th24: :: MODAL_1:24
for Z being Tree
for x1, x2 being Element of Z st x1 = <*0*> &amp; x2 = <*1*> &amp; succ (Root Z) = {x1,x2} holds
Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))
proofend;

theorem Th25: :: MODAL_1:25
for D being non empty set
for Z being DecoratedTree of D
for x1, x2 being Element of dom Z st x1 = <*0*> &amp; x2 = <*1*> &amp; succ (Root (dom Z)) = {x1,x2} holds
Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))
proofend;

definition
func MP-variables  ->  set  equals :: MODAL_1:def 3
[:{3},NAT:];
coherence
 [:{3},NAT:] is set ;
end;

:: deftheorem  defines MP-variables MODAL_1:def_3_:_
 MP-variables = [:{3},NAT:];

registration
cluster MP-variables  ->  non empty ;
coherence
 not MP-variables is 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:];
coherence
 [:{0,1,2},NAT:] is set ;
end;

:: deftheorem  defines MP-conectives MODAL_1:def_4_:_
 MP-conectives = [:{0,1,2},NAT:];

registration
cluster MP-conectives  ->  non empty ;
coherence
 not MP-conectives is empty ;
end;

definition
mode MP-conective is Element of MP-conectives ;
end;

theorem Th26: :: MODAL_1:26
MP-conectives misses MP-variables
proofend;

definition
let T be finite Tree;
let v be Element of T;
:: original:branchdeg
redefine func branchdeg v ->  Element of NAT ;
coherence
 branchdeg v is Element of NAT
proofend;
end;

definition
func MP-WFF  ->  DTree-set of [:NAT,NAT:] means :Def5: :: MODAL_1:def 5
( ( for x being DecoratedTree of [:NAT,NAT:] st x in it holds
x is finite ) &amp; ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in it iff for v being Element of dom x holds
( branchdeg v <= 2 &amp; ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) &amp; ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) &amp; ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) );
existence
 ex b1 being DTree-set of [:NAT,NAT:] st
( ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds
x is finite ) &amp; ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b1 iff for v being Element of dom x holds
( branchdeg v <= 2 &amp; ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) &amp; ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) &amp; ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) )
proofend;
uniqueness
 for b1, b2 being DTree-set of [:NAT,NAT:] st ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds
x is finite ) &amp; ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b1 iff for v being Element of dom x holds
( branchdeg v <= 2 &amp; ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) &amp; ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) &amp; ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) &amp; ( for x being DecoratedTree of [:NAT,NAT:] st x in b2 holds
x is finite ) &amp; ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b2 iff for v being Element of dom x holds
( branchdeg v <= 2 &amp; ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) &amp; ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) &amp; ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines MP-WFF MODAL_1:def_5_:_
 for b1 being DTree-set of [:NAT,NAT:] holds
( b1 = MP-WFF iff ( ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds
x is finite ) &amp; ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b1 iff for v being Element of dom x holds
( branchdeg v <= 2 &amp; ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) &amp; ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) &amp; ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) );

:: [0,0] = VERUM
:: [1,0] = negation
:: [1,1] = modal operator of necessity
:: [2,0] = &amp;
definition
mode MP-wff is Element of MP-WFF ;
end;

registration
cluster  ->  finite for Element of MP-WFF ;
coherence
 for b1 being MP-wff holds b1 is finite by Def5;
end;

definition
let A be MP-wff;
let a be Element of dom A;
:: original:|
redefine funcA | a ->  MP-wff;
coherence
 A | a is MP-wff
proofend;
end;

definition
let a be Element of MP-conectives ;
func the_arity_of a ->  Element of NAT  equals :: MODAL_1:def 6
a `1 ;
coherence
 a `1 is Element of NAT
proofend;
end;

:: deftheorem  defines the_arity_of MODAL_1:def_6_:_
 for a being Element of MP-conectives holds the_arity_of a = a `1 ;

definition
let D be non empty set ;
let T, T1 be DecoratedTree of D;
let p be FinSequence of NAT ;
assume A1: p in dom T ;
func @ (T,p,T1) ->  DecoratedTree of D equals :Def7: :: MODAL_1:def 7
T with-replacement (p,T1);
coherence
 T with-replacement (p,T1) is DecoratedTree of D
proofend;
end;

:: deftheorem Def7 defines @ MODAL_1:def_7_:_
 for D being non empty set
for T, T1 being DecoratedTree of D
for p being FinSequence of NAT st p in dom T holds
@ (T,p,T1) = T with-replacement (p,T1);

theorem Th27: :: MODAL_1:27
for A being MP-wff holds ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff
proofend;

theorem Th28: :: MODAL_1:28
for A being MP-wff holds ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff
proofend;

theorem Th29: :: MODAL_1:29
for A, B being MP-wff holds (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff
proofend;

definition
let A be MP-wff;
func 'not' A ->  MP-wff equals :: MODAL_1:def 8
((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A);
coherence
 ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff by Th27;
func (#) A ->  MP-wff equals :: MODAL_1:def 9
((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A);
coherence
 ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff by Th28;
let B be MP-wff;
funcA '&amp;' B ->  MP-wff equals :: MODAL_1:def 10
(((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B);
coherence
 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff by Th29;
end;

:: deftheorem  defines 'not' MODAL_1:def_8_:_
 for A being MP-wff holds 'not' A = ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A);

:: deftheorem  defines (#) MODAL_1:def_9_:_
 for A being MP-wff holds (#) A = ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A);

:: deftheorem  defines '&amp;' MODAL_1:def_10_:_
 for A, B being MP-wff holds A '&amp;' B = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B);

definition
let A be MP-wff;
func ? A ->  MP-wff equals :: MODAL_1:def 11
 'not' ((#) ('not' A));
correctness
coherence
'not' ((#) ('not' A)) is MP-wff;
;
let B be MP-wff;
funcA 'or' B ->  MP-wff equals :: MODAL_1:def 12
 'not' (('not' A) '&amp;' ('not' B));
correctness
coherence
'not' (('not' A) '&amp;' ('not' B)) is MP-wff;
;
funcA => B ->  MP-wff equals :: MODAL_1:def 13
 'not' (A '&amp;' ('not' B));
correctness
coherence
'not' (A '&amp;' ('not' B)) is MP-wff;
;
end;

:: deftheorem  defines ? MODAL_1:def_11_:_
 for A being MP-wff holds ? A = 'not' ((#) ('not' A));

:: deftheorem  defines 'or' MODAL_1:def_12_:_
 for A, B being MP-wff holds A 'or' B = 'not' (('not' A) '&amp;' ('not' B));

:: deftheorem  defines => MODAL_1:def_13_:_
 for A, B being MP-wff holds A => B = 'not' (A '&amp;' ('not' B));

theorem Th30: :: MODAL_1:30
for n being Element of NAT holds (elementary_tree 0) --> [3,n] is MP-wff
proofend;

theorem Th31: :: MODAL_1:31
(elementary_tree 0) --> [0,0] is MP-wff
proofend;

definition
let p be MP-variable;
func @ p ->  MP-wff equals :: MODAL_1:def 14
(elementary_tree 0) --> p;
coherence
 (elementary_tree 0) --> p is MP-wff
proofend;
end;

:: deftheorem  defines @ MODAL_1:def_14_:_
 for p being MP-variable holds @ p = (elementary_tree 0) --> p;

theorem Th32: :: MODAL_1:32
for p, q being MP-variable st @ p = @ q holds
p = q
proofend;

Lm3:  for n, m being Element of NAT holds <*0*> in dom ((elementary_tree 1) --> [n,m])
proofend;

theorem Th33: :: MODAL_1:33
for A, B being MP-wff st 'not' A = 'not' B holds
A = B
proofend;

theorem Th34: :: MODAL_1:34
for A, B being MP-wff st (#) A = (#) B holds
A = B
proofend;

theorem Th35: :: MODAL_1:35
for A, B, A1, B1 being MP-wff st A '&amp;' B = A1 '&amp;' B1 holds
( A = A1 &amp; B = B1 )
proofend;

definition
func VERUM  ->  MP-wff equals :: MODAL_1:def 15
(elementary_tree 0) --> [0,0];
coherence
 (elementary_tree 0) --> [0,0] is MP-wff by Th31;
end;

:: deftheorem  defines VERUM MODAL_1:def_15_:_
 VERUM = (elementary_tree 0) --> [0,0];

theorem Th36: :: MODAL_1:36
for A being MP-wff holds
( not card (dom A) = 1 or A = VERUM or ex p being MP-variable st A = @ p )
proofend;

theorem Th37: :: MODAL_1:37
for A being MP-wff holds
( not card (dom A) >= 2 or ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&amp;' C )
proofend;

theorem Th38: :: MODAL_1:38
for A being MP-wff holds card (dom A) < card (dom ('not' A))
proofend;

theorem Th39: :: MODAL_1:39
for A being MP-wff holds card (dom A) < card (dom ((#) A))
proofend;

theorem Th40: :: MODAL_1:40
for A, B being MP-wff holds
( card (dom A) < card (dom (A '&amp;' B)) &amp; card (dom B) < card (dom (A '&amp;' B)) )
proofend;

definition
let IT be MP-wff;
attrIT is atomic  means :Def16: :: MODAL_1:def 16
 ex p being MP-variable st IT = @ p;
attrIT is negative  means :Def17: :: MODAL_1:def 17
 ex A being MP-wff st IT = 'not' A;
attrIT is necessitive  means :Def18: :: MODAL_1:def 18
 ex A being MP-wff st IT = (#) A;
attrIT is conjunctive  means :Def19: :: MODAL_1:def 19
 ex A, B being MP-wff st IT = A '&amp;' B;
end;

:: deftheorem Def16 defines atomic MODAL_1:def_16_:_
 for IT being MP-wff holds
( IT is atomic iff ex p being MP-variable st IT = @ p );

:: deftheorem Def17 defines negative MODAL_1:def_17_:_
 for IT being MP-wff holds
( IT is negative iff ex A being MP-wff st IT = 'not' A );

:: deftheorem Def18 defines necessitive MODAL_1:def_18_:_
 for IT being MP-wff holds
( IT is necessitive iff ex A being MP-wff st IT = (#) A );

:: deftheorem Def19 defines conjunctive MODAL_1:def_19_:_
 for IT being MP-wff holds
( IT is conjunctive iff ex A, B being MP-wff st IT = A '&amp;' B );

registration
cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like atomic for Element of MP-WFF ;
existence
 ex b1 being MP-wff st b1 is atomic
proofend;
cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like negative for Element of MP-WFF ;
existence
 ex b1 being MP-wff st b1 is negative
proofend;
cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like necessitive for Element of MP-WFF ;
existence
 ex b1 being MP-wff st b1 is necessitive
proofend;
cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like conjunctive for Element of MP-WFF ;
existence
 ex b1 being MP-wff st b1 is conjunctive
proofend;
end;

scheme :: MODAL_1:sch 1
MPInd{ P1[ Element of MP-WFF ] } :
 for A being Element of MP-WFF holds P1[A]
provided
A1: P1[ VERUM ] and
A2: for p being MP-variable holds P1[ @ p] and
A3: for A being Element of MP-WFF st P1[A] holds
P1[ 'not' A] and
A4: for A being Element of MP-WFF st P1[A] holds
P1[ (#) A] and
A5: for A, B being Element of MP-WFF st P1[A] &amp; P1[B] holds
P1[A '&amp;' B]
proofend;

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

theorem Th42: :: MODAL_1:42
for A being MP-wff holds
( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&amp;' C )
proofend;

theorem Th43: :: MODAL_1:43
for p being MP-variable
for A, B being MP-wff holds
( @ p <> 'not' A &amp; @ p <> (#) A &amp; @ p <> A '&amp;' B )
proofend;

theorem Th44: :: MODAL_1:44
for A, B, C being MP-wff holds
( 'not' A <> (#) B &amp; 'not' A <> B '&amp;' C )
proofend;

theorem Th45: :: MODAL_1:45
for A, B, C being MP-wff holds (#) A <> B '&amp;' C
proofend;

Lm4:  for A, B being MP-wff holds
( VERUM <> 'not' A &amp; VERUM <> (#) A &amp; VERUM <> A '&amp;' B )
proofend;

Lm5:  [0,0] is MP-conective
proofend;

Lm6:  for p being MP-variable holds VERUM <> @ p
proofend;

theorem :: MODAL_1:46
for p being MP-variable
for A, B being MP-wff holds
( VERUM <> @ p &amp; VERUM <> 'not' A &amp; VERUM <> (#) A &amp; VERUM <> A '&amp;' B ) by Lm4, Lm6;

scheme :: MODAL_1:sch 2
MPFuncEx{ F1() ->  non empty set , F2() ->  Element of F1(), F3( Element of MP-variables ) ->  Element of F1(), F4( Element of F1()) ->  Element of F1(), F5( Element of F1()) ->  Element of F1(), F6( Element of F1(), Element of F1()) ->  Element of F1() } :
 ex f being Function of MP-WFF,F1() st
( f . VERUM = F2() &amp; ( for p being MP-variable holds f . (@ p) = F3(p) ) &amp; ( for A being Element of MP-WFF holds f . ('not' A) = F4((f . A)) ) &amp; ( for A being Element of MP-WFF holds f . ((#) A) = F5((f . A)) ) &amp; ( for A, B being Element of MP-WFF holds f . (A '&amp;' B) = F6((f . A),(f . B)) ) )
proofend;