begin
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
canceled;
theorem
canceled;
theorem Th3:
theorem
theorem Th5:
theorem
theorem
theorem
canceled;
theorem
theorem
theorem Th11:
theorem
theorem Th13:
theorem
canceled;
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem
canceled;
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
Lm2:
for f being Function st dom f is finite holds
f is finite
theorem Th28:
theorem Th29:
theorem Th30:
:: deftheorem defines MP-variables MODAL_1:def 3 :
:: deftheorem defines MP-conectives MODAL_1:def 4 :
theorem Th31:
:: deftheorem Def5 defines DOMAIN_DecoratedTree MODAL_1:def 5 :
definition
func MP-WFF -> DOMAIN_DecoratedTree of
[:NAT ,NAT :] means :
Def6:
( ( 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:
theorem Th33:
theorem Th34:
definition
let A be
MP-wff;
func 'not' A -> MP-wff equals
((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
((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
(((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:
theorem Th36:
:: deftheorem defines @ MODAL_1:def 15 :
theorem Th37:
Lm3:
for n, m being Element of NAT holds <*0 *> in dom ((elementary_tree 1) --> [n,m])
theorem Th38:
theorem Th39:
theorem Th40:
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
canceled;
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
:: 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
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
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