| ⊢ f ⊃ f | FBoxImpWeakNextBox |
Proof:
1 | ¬¬¬f ⊃ ¬f | |
2 | ¬¬¬f ⊃ ¬f | |
3 | ¬f ⊃ ¬f | |
4 | ¬¬¬f ⊃ ¬f | |
5 | ¬ f ⊃ ¬f | 4, def. of |
6 | ¬¬f ⊃ ¬¬ f | |
7 | f ⊃ f | 6, def. of , |
qed
Below is a proof of PTL Axiom A4: