| |
| 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.
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 | |
6 | f ≡f | 5, def. of |
| ⊢ ¬f ≡¬f | | DfDfNotEqvNotBfBf |
1 | ¬f ≡¬f | |
2 | ¬f ≡¬f | |
3 | ¬f ≡¬f | |
4 | ¬f ≡¬f | |
1 | ¬f ≡¬f | |
2 | ¬f ≡¬f | |
3 | ¬f ≡¬f | |
4 | ¬f ≡¬f | |
5 | ¬f ≡¬f | |
6 | f ≡f | |
|
| |
Next