ITL
© 1996-2018







17.6 Some Properties of Together with

We make use of the following analogue of Theorem DfNotEqvNotBf for and :


¬f ≡¬f DiamondNotEqvNotBox


1
¬f ≡¬f


f f DfDiamondEqvDiamondDf


1
(true f) true true (f true)
2
( f) true (f true)
1, def. of 
3
f f
2, def. of 


¬f ≡¬f DfDiamondNotEqvNotBfBox


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


¬f ≡¬f DiamondDfNotEqvNotBoxBf


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


f f BfBoxEqvBoxBf


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







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