ITL
© 1996-2018







17.4 Some Properties of involving the Modal System K4

We now consider how to establish for the PITL operator the axiom “4” (PITL Theorem BfImpBfBf) found in the modal systems K4 and S4.


f f DfDfEqvDf


1
(f true) true f (true true)
2
true true
3
(true true) true
2, def. of 
4
f (true true) f true
5
(f true) true f true
1, 4,EqvChain
6
f f
5, def. of 


¬f ≡¬f DfNotEqvNotBf


1
f ≡¬¬f
def. of 
2
¬f ≡¬f


¬f ≡¬f DfDfNotEqvNotBfBf


1
¬f ≡¬f
2
¬f ¬f
3
¬f ≡¬f
4
¬f ≡¬f
2, 3,EqvChain


f f BfBfEqvBf


1
¬f ¬f
2
¬f ≡¬f
3
¬f ¬f
1, 2,Prop
4
¬f ≡¬f
5
¬f ≡¬f
3, 4,EqvChain
6
f f
5,Prop


f f BfImpBfBf


1
f f
2
f f
1,Prop







2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL