ITL
© 1996-2018







8.6 Some Properties of Together with

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

¬f ≡¬f DiamondNotEqvNotBox

Proof:

1
¬f ≡¬f

qed

f f DfDiamondEqvDiamondDf

Proof:

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

qed

¬f ≡¬f DfDiamondNotEqvNotBfBox

Proof:

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

qed

¬f ≡¬f DiamondDfNotEqvNotBoxBf

Proof:

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

qed

f f BfBoxEqvBoxBf

Proof:

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

qed







2018-10-21
Contact | Home | ITL home | Course | Proofs | Algebra | FL