| ⊢ | (¬g ⊃ ¬f) ⊃ f ⊃ g | FBoxContraPosImpDist |
Proof:
1 | (¬g ⊃ ¬f) ⊃ ¬g ⊃ ¬f | |
2 | (¬g ⊃ ¬f) ⊃ ¬¬f ⊃ ¬¬g | |
3 | (¬g ⊃ ¬f) ⊃ f ⊃ g | 2, def. of |
qed
Below is the proof of PTL Axiom A1 as FL theorem FBoxImpDist. In the final step, ImpChain stands for a chain of implications.