© 1996-2018

| | | ||||||||||

| ## 17 Some PITL theorems and Their ProofsThis 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 ﬁnite and inﬁnite time. We have partially organised the material, particularly in Section 17.2, along the lines of some standard modal logic systems. The PITL theorems and derived rules have a shared index sequence (e.g., BfChopImpChop–BoxChopEqvChop are followed by BfGen rather than DR1). We believe that this convention simpliﬁes locating material in this appendix. Proof steps can refer to axioms, inference rules, previously deduced theorems, derived inference rules and also the following: - Assumptions which are regarded as being previously deduced.
- Prop: Conventional nonmodal propositional reasoning (by restricted application of Axiom VPTL) and Modus Ponens.
- ImpChain: A chain of implications.
- EqvChain: A chain of equivalences.
- In principle, ImpChain and EqvChain are subsumed by Prop but are used here to make the reasoning more explicit.
17.1 Some Basic Properties of Chop
17.2 Some Properties of involving the Modal System K and Axiom D 17.3 Some Properties of Chop, and with State Formulas 17.4 Some Properties of involving the Modal System K4 17.5 Properties Involving the PTL Operator 17.6 Some Properties of Together with 17.7 Some Properties of Chop-Star 17.8 Some Properties Involving a Reduction to PITL with Finite Time 17.9 Some Properties of Skip, Next And Until | | ||||||||||

| |