5 Deduction of PTL Axioms from the FL Axiom System

(f g) f g A1
f f A2
(f g) f g A3
f f f A4
(f f) f f A5
f is a tautology ⇒ ⊢ f R1
f g, f ⇒ ⊢ g R2
f ⇒ ⊢ f R3
Table 2: Modified version of Pnueli’s complete axiom system

All FL tautologies FLTaut
X ≡⟨skipf FL2
f ≡⟨skipf FL3
w?f w f FL4
E0 E1f ≡⟨E0f ∨⟨E1f FL5
E0 ; E1f ≡⟨E0⟩⟨E1f FL6
E(f g) ⊃⟨Ef ∨⟨Eg FL7
Ef f ∨⟨E ; Ef FL8
(f g) ⊃⟨Ef ⊃⟨Eg FL9
f f FL10
(f f) f f FL11
empty FL12
f g, f ⇒ ⊢ g FLMP
f ⇒ ⊢ f FLBoxGen
E0empty ⊃⟨E0empty ⇒ ⊢ ⟨E0f ⊃⟨E1f FInf3
(more ∧⟨E0empty)E1empty ⇒ ⊢ ⟨E0f ⊃⟨E1f FInf4
Table 3: Axiom system for FL

This appendix contains various FL theorems and their deductions. These include ones corresponding to some of the PTL axioms in Table 2. Most of the PTL axioms and inference rules have identical or nearly identical versions in the FL axiom system in Table 3. The three exceptions are Axioms A1, A3 and A4. We will look at each of them in turn as FL theorems FBoxImpDist, FNextImpDist and FBoxImpNowAndWeakNext, respectively. The trickiest is Axiom A1. The symbol as used here always refers to FL. None of the FE formulas occurring in the proofs contain variables and therefore the proofs also ensure well-formed FLV theorems and derived inference rules for any V.

   FBoxImpDiamondImpDiamond
   FBoxContraPosImpDist
   FBoxImpDist
   FNextNotImpNotNext
   FNextImpDist
   FRightSkipChopImpSkipChopRule
   FNextImpNextRule
   FNextEqvNextRule
   FDiamondEqvNowOrNextDiamond
   FNowImpDiamond
   FNextDiamondImpDiamond
   BoxImpNow
   FBoxImpWeakNextBox
   FBoxImpNowAndWeakNext

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023