ITL
© 1996-2018







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 finite time is assumed. Recall that any valid implication of the form finite f is allowed and that we designate such a step by using PITLF. PITL Theorem BfFinStateEqvBox below illustrates this technique.

finite (f g) ⇒ ⊢ f g FiniteImpBfImpBfRule

Proof:

1
finite (f g)
Assump
2
(f g)
3
(f g) ( f g)
4
f g
2, 3,MP

qed

finite (f g) ⇒ ⊢ f g FiniteImpBfEqvBfRule

Proof:

1
finite (f g)
Assump
2
finite (f g)
1,Prop
3
f g
4
finite (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 finite time:

fin w w BfFinStateEqvBox

Proof:

1
fin w fin w
2
fin w fin w
1,Prop
3
finite (( fin w) w)
4
fin w w
5
w w
6
w w
7
w w
8
fin w w
2, 4, 5, 7,EqvChain

qed

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







2018-10-21
Contact | Home | ITL home | Course | Proofs | Algebra | FL