#### 8.8 Some Properties Involving a Reduction to PITL with Finite Time

We now present some derived inference rules which come in useful when completeness for PITL with ﬁnite time is assumed. Recall that any valid implication of the form ﬁnite f is allowed and that we designate such a step by using PITLF. PITL Theorem BfFinStateEqvBox below illustrates this technique.

 ⊢ ﬁnite ⊃(f ⊃g) ⇒ ⊢ f ⊃g FiniteImpBfImpBfRule

Proof:

 1 ﬁnite ⊃(f ⊃g) Assump 2 (f ⊃g) 1,BfFGen 3 (f ⊃g) ⊃( f ⊃g) BfImpDist 4 f ⊃g 2, 3,MP

qed

 ⊢ ﬁnite ⊃(f ≡ g) ⇒ ⊢ f ≡g FiniteImpBfEqvBfRule

Proof:

 1 ﬁnite ⊃(f ≡ g) Assump 2 ﬁnite ⊃(f ⊃g) 1,Prop 3 f ⊃g 4 ﬁnite ⊃(g ⊃f) 1,Prop 5 g ⊃f 6 f ≡g 3, 5,Prop

qed

The next theorem’s proof involves the application of the previous derived inference rule together with completeness for PITL with just ﬁnite time:

 ⊢ ﬁn w ≡w BfFinStateEqvBox

Proof:

 1 ﬁn w ≡ ﬁn w 2 ﬁn w ≡ ﬁn w 1,Prop 3 ﬁnite ⊃(( ﬁn w) ≡w) 4 ﬁn w ≡w 5 w ≡w 6 w ≡ w 7 w ≡w 8 ﬁn w ≡w 2, 4, 5, 7,EqvChain

qed

An alternative proof of Theorem BfFinStateEqvBox can be given without PITLF by ﬁrst deducing the dual equivalence ( (empty w)) w, for any state formula w.

 2019-01-03 Contact | Home | ITL home | Course | Proofs | Algebra | FL