8 Some PITL theorems and Their Proofs

This appendix gives a representative set of PITL theorems and derived inference rules together with their proofs. Many are used either directly or indirectly in the completeness proof for PITL with both finite and infinite time. We have partially organised the material, particularly in Section 8.2, along the lines of some standard modal logic systems.

The PITL theorems and derived rules have a shared index sequence (e.g., BfChopImpChopBoxChopEqvChop are followed by BfGen rather than DR1). We believe that this convention simplifies locating material in this appendix.

Proof steps can refer to axioms, inference rules, previously deduced theorems, derived inference rules and also the following:

Our assumption of axiomatic completeness for PITL with just finite time PITLF
permits any valid implication of the form finite f.

  8.1 Some Basic Properties of Chop
  8.2 Some Properties of involving the Modal System K and Axiom D
  8.3 Some Properties of Chop, and with State Formulas
  8.4 Some Properties of involving the Modal System K4
  8.5 Properties Involving the PTL Operator
  8.6 Some Properties of Together with
  8.7 Some Properties of Chop-Star
  8.8 Some Properties Involving a Reduction to PITL with Finite Time
  8.9 Some Properties of Skip, Next And Until

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