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 ≡⟨skip⟩f
FL2
⊢
f ≡⟨skip∗⟩f
FL3
⊢
⟨w?⟩f ≡ w ∧ f
FL4
⊢
⟨E0∨ E1⟩f ≡⟨E0⟩f ∨⟨E1⟩f
FL5
⊢
⟨E0; E1⟩f ≡⟨E0⟩⟨E1⟩f
FL6
⊢
⟨E⟩(f ∨ g) ⊃⟨E⟩f ∨⟨E⟩g
FL7
⊢
⟨E∗⟩f ≡ f ∨⟨E ; E∗⟩f
FL8
⊢
(f ⊃ g) ⊃⟨E⟩f ⊃⟨E⟩g
FL9
⊢
f ⊃f
FL10
⊢
(f ⊃f) ∧ f ⊃f
FL11
⊢
empty
FL12
⊢
f ⊃ g, ⊢ f ⇒ ⊢ g
FLMP
⊢
f ⇒ ⊢f
FLBoxGen
⊢
⟨E0⟩empty ⊃⟨E0⟩empty ⇒ ⊢ ⟨E0⟩f ⊃⟨E1⟩f
FInf3
⊢
(more ∧⟨E0⟩empty)⟨E1⟩empty ⇒ ⊢ ⟨E0∗⟩f ⊃⟨E1∗⟩f
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.