:: Introduction to Modal Propositional Logic
:: by Alicia de la Cruz
::
:: Received September 30, 1991
:: Copyright (c) 1991 Association of Mizar Users
Lm1:
for m being Element of NAT holds {} is_a_proper_prefix_of <*m*>
:: deftheorem defines Root MODAL_1:def 1 :
:: deftheorem defines Root MODAL_1:def 2 :
theorem :: MODAL_1:1
canceled;
theorem :: MODAL_1:2
canceled;
theorem Th3: :: MODAL_1:3
theorem :: MODAL_1:4
theorem Th5: :: MODAL_1:5
theorem :: MODAL_1:6
theorem :: MODAL_1:7
theorem :: MODAL_1:8
canceled;
theorem :: MODAL_1:9
theorem :: MODAL_1:10
theorem Th11: :: MODAL_1:11
theorem :: MODAL_1:12
theorem Th13: :: MODAL_1:13
theorem :: MODAL_1:14
canceled;
theorem Th15: :: MODAL_1:15
theorem Th16: :: MODAL_1:16
theorem Th17: :: MODAL_1:17
theorem Th18: :: MODAL_1:18
theorem :: MODAL_1:19
theorem Th20: :: MODAL_1:20
theorem :: MODAL_1:21
canceled;
theorem Th22: :: MODAL_1:22
theorem Th23: :: MODAL_1:23
theorem Th24: :: MODAL_1:24
theorem Th25: :: MODAL_1:25
theorem Th26: :: MODAL_1:26
theorem Th27: :: MODAL_1:27
Lm2:
for f being Function st dom f is finite holds
f is finite
theorem Th28: :: MODAL_1:28
theorem Th29: :: MODAL_1:29
theorem Th30: :: MODAL_1:30
:: deftheorem defines MP-variables MODAL_1:def 3 :
:: deftheorem defines MP-conectives MODAL_1:def 4 :
theorem Th31: :: MODAL_1:31
:: deftheorem Def5 defines DOMAIN_DecoratedTree MODAL_1:def 5 :
definition
func MP-WFF -> DOMAIN_DecoratedTree of
[:NAT ,NAT :] means :
Def6:
:: MODAL_1:def 6
( ( 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 & ( not
branchdeg v = 0 or
x . v = [0 ,0 ] or ex
k being
Element of
NAT st
x . v = [3,k] ) & ( not
branchdeg v = 1 or
x . v = [1,0 ] or
x . v = [1,1] ) & (
branchdeg v = 2 implies
x . v = [2,0 ] ) ) ) ) );
existence
ex b1 being DOMAIN_DecoratedTree of [:NAT ,NAT :] st
( ( for x being DecoratedTree of [:NAT ,NAT :] st x in b1 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT ,NAT :] holds
( x in b1 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) )
uniqueness
for b1, b2 being DOMAIN_DecoratedTree of [:NAT ,NAT :] st ( for x being DecoratedTree of [:NAT ,NAT :] st x in b1 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT ,NAT :] holds
( x in b1 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) & ( for x being DecoratedTree of [:NAT ,NAT :] st x in b2 holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT ,NAT :] holds
( x in b2 iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines MP-WFF MODAL_1:def 6 :
:: deftheorem defines the_arity_of MODAL_1:def 7 :
:: deftheorem Def8 defines @ MODAL_1:def 8 :
theorem Th32: :: MODAL_1:32
theorem Th33: :: MODAL_1:33
theorem Th34: :: MODAL_1:34
definition
let A be
MP-wff;
func 'not' A -> MP-wff equals :: MODAL_1:def 9
((elementary_tree 1) --> [1,0 ]) with-replacement <*0 *>,
A;
coherence
((elementary_tree 1) --> [1,0 ]) with-replacement <*0 *>,A is MP-wff
by Th32;
func (#) A -> MP-wff equals :: MODAL_1:def 10
((elementary_tree 1) --> [1,1]) with-replacement <*0 *>,
A;
coherence
((elementary_tree 1) --> [1,1]) with-replacement <*0 *>,A is MP-wff
by Th33;
let B be
MP-wff;
func A '&' B -> MP-wff equals :: MODAL_1:def 11
(((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 Th34;
end;
:: deftheorem defines 'not' MODAL_1:def 9 :
:: deftheorem defines (#) MODAL_1:def 10 :
:: deftheorem defines '&' MODAL_1:def 11 :
:: deftheorem defines ? MODAL_1:def 12 :
:: deftheorem defines 'or' MODAL_1:def 13 :
:: deftheorem defines => MODAL_1:def 14 :
theorem Th35: :: MODAL_1:35
theorem Th36: :: MODAL_1:36
:: deftheorem defines @ MODAL_1:def 15 :
theorem Th37: :: MODAL_1:37
Lm3:
for n, m being Element of NAT holds <*0 *> in dom ((elementary_tree 1) --> [n,m])
theorem Th38: :: MODAL_1:38
theorem Th39: :: MODAL_1:39
theorem Th40: :: MODAL_1:40
for
A,
B,
A1,
B1 being
MP-wff st
A '&' B = A1 '&' B1 holds
(
A = A1 &
B = B1 )
:: deftheorem defines VERUM MODAL_1:def 16 :
theorem :: MODAL_1:41
canceled;
theorem Th42: :: MODAL_1:42
theorem Th43: :: MODAL_1:43
theorem Th44: :: MODAL_1:44
theorem Th45: :: MODAL_1:45
theorem Th46: :: MODAL_1:46
:: deftheorem Def17 defines atomic MODAL_1:def 17 :
:: deftheorem Def18 defines negative MODAL_1:def 18 :
:: deftheorem Def19 defines necessitive MODAL_1:def 19 :
:: deftheorem Def20 defines conjunctive MODAL_1:def 20 :
theorem :: MODAL_1:47
theorem Th48: :: MODAL_1:48
theorem Th49: :: MODAL_1:49
theorem Th50: :: MODAL_1:50
theorem Th51: :: MODAL_1:51
Lm4:
for A, B being MP-wff holds
( VERUM <> 'not' A & VERUM <> (#) A & VERUM <> A '&' B )
Lm5:
[0 ,0 ] is MP-conective
Lm6:
for p being MP-variable holds VERUM <> @ p
theorem :: MODAL_1:52