| ⊢ | (f ⊃ g) ⊃ f ⊃ g | FNextImpDist |
Proof:
1 | ⟨skip⟩(¬f ∨ g) ⊃ (⟨skip⟩¬f) ∨ (⟨skip⟩g) | |
2 | (¬f ∨ g) ≡⟨skip⟩(¬f ∨ g) | |
3 | ¬f ≡⟨skip⟩¬f | |
4 | g ≡⟨skip⟩g | |
5 | (¬f ∨ g) ⊃ ¬f ∨ g | |
6 | ¬f ⊃ ¬ f | |
7 | (¬f ∨ g) ⊃ ¬ f ∨ g | |
8 | (f ⊃ g) ⊃ f ⊃ g | 7, def. of ⊃ |
qed
The remaining proofs are for ultimately deducing PTL Axiom A4 as FL theorem FBoxImpNowAndWeakNext. The following derived rule FRightSkipChopImpSkipChopRule can be readily generalised to allow some arbitrary FE formula in place of skip. In addition, a version can be proven which uses ≡ instead of ⊃ .