ITL
© 1996-2018







8.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

Proof:

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 

qed

¬f ≡¬f DfNotEqvNotBf

Proof:

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

qed

¬f ≡¬f DfDfNotEqvNotBfBf

Proof:

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

qed

f f BfBfEqvBf

Proof:

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

qed

f f BfImpBfBf

Proof:

1
f f
2
f f
1,Prop

qed







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