### 14 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: Modiﬁed 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 .

 ⊢ (f ⊃g) ⊃f ⊃g FBoxImpDiamondImpDiamond

Proof:

 1 (f ⊃g) ⊃⟨skip∗⟩f ⊃⟨skip∗⟩g 2 f ≡⟨skip∗⟩f 3 g ≡⟨skip∗⟩g 4 (f ⊃g) ⊃f ⊃g 2, 3,Prop

The following slightly obscure theorem is used in the proof of FBoxImpDist:

 ⊢ (¬g ⊃¬f) ⊃f ⊃g FBoxContraPosImpDist

Proof:

 1 (¬g ⊃¬f) ⊃¬g ⊃¬f FBoxImpDiamondImpDiamond 2 (¬g ⊃¬f) ⊃¬¬f ⊃¬¬g 1,Prop 3 (¬g ⊃¬f) ⊃f ⊃g 2, def. of

Below is the proof of PTL Axiom A1 as FL theorem FBoxImpDist. In the ﬁnal step, ImpChain stands for a chain of implications.

 ⊢ (X ⊃g) ⊃f ⊃g FBoxImpDist

Proof:

 1 (f ⊃g) ⊃(¬g ⊃¬f) 2 ¬(¬g ⊃¬f) ⊃¬(f ⊃g) 1,Prop 3 (¬(¬g ⊃¬f) ⊃¬(f ⊃g)) 2,FLBoxGen 4 (¬(¬g ⊃¬f) ⊃¬(f ⊃g)) ⊃(f ⊃g) ⊃(¬g ⊃¬f) FBoxContraPosImpDist 5 (f ⊃g) ⊃(¬g ⊃¬f) 3, 4,FLMP 6 (¬g ⊃¬f) ⊃f ⊃g FBoxContraPosImpDist 7 (X ⊃g) ⊃f ⊃g 5, 6,ImpChain

 ⊢ ¬f ⊃¬f FNextNotImpNotNext

Proof:

 1 f ⊃f 2 f ⊃¬¬f 1, def. of 3 ¬f ⊃¬f 2,Prop

Here is a proof of PTL Axiom A3:

 ⊢ (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 1–4,Prop 6 ¬f ⊃¬f FNextNotImpNotNext 7 (¬f ∨ g) ⊃¬f ∨g 5, 6,Prop 8 (f ⊃g) ⊃f ⊃g 7, def. of  ⊃

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 .

 ⊢ f ⊃g ⇒ ⊢ ⟨skip⟩f ⊃⟨skip⟩g FRightSkipChopImpSkipChopRule

Proof:

 1 f ⊃g Assump 2 (f ⊃g) FLBoxGen 3 (f ⊃g) ⊃⟨skip⟩f ⊃⟨skip⟩g 4 ⟨skip⟩f ⊃⟨skip⟩g 2, 3,MP

 ⊢ f ⊃g ⇒ f ⊃g FNextImpNextRule

Proof:

 1 f ⊃g Assump 2 ⟨skip⟩f ⊃⟨skip⟩g 3 f ≡⟨skip⟩f 4 g ≡⟨skip⟩g 5 f ⊃g 3, 4,Prop

 ⊢ f ≡ g ⇒ f ≡g FNextEqvNextRule

Proof:

 1 f ≡ g Assump 2 f ⊃g 1,Prop 3 f ⊃g 4 g ⊃f 1,Prop 5 g ⊃f 6 f ≡g 3, 5,Prop

 ⊢ f ≡ f ∨f FDiamondEqvNowOrNextDiamond

Proof:

 1 f ≡⟨skip∗⟩f 2 ⟨skip∗⟩f ≡ f ∨⟨skip ; skip∗⟩f 3 ⟨skip ; skip∗⟩f ≡⟨skip⟩⟨skip∗⟩f 4 ⟨skip∗⟩f ≡⟨skip⟩⟨skip∗⟩f 5 f ≡⟨skip∗⟩X 6 f ≡ f ∨f 1–5,Prop

 ⊢ f ⊃f FNowImpDiamond

Proof:

 1 f ≡ f ∨f FDiamondEqvNowOrNextDiamond 2 f ⊃f 1,Prop

 ⊢ f ⊃f FNextDiamondImpDiamond

Proof:

 1 f ≡ f ∨f FDiamondEqvNowOrNextDiamond 2 f ⊃f 1,Prop

 ⊢ f ⊃f BoxImpNow

Proof:

 1 ¬f ⊃¬f FNowImpDiamond 2 ¬¬f ⊃f 1,Prop 3 f ⊃f 2, def. of

 ⊢ f ⊃f FBoxImpWeakNextBox

Proof:

 1 ¬¬¬f ⊃¬f 2 ¬¬¬f ⊃¬f 3 ¬f ⊃¬f FNextDiamondImpDiamond 4 ¬¬¬f ⊃¬f 2, 3,ImpChain 5 ¬f ⊃¬f 4, def. of 6 ¬¬f ⊃¬¬f 5,Prop 7 f ⊃f 6, def. of ,

Below is a proof of PTL Axiom A4:

 ⊢ f ⊃f ∧f FBoxImpNowAndWeakNext

Proof:

 1 f ⊃f 2 f ⊃f FBoxImpWeakNextBox 3 f ⊃f ∧f 1, 2,Prop

 2018-02-26 Contact | Home | ITL home | Course | Proofs | Algebra | FL