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
   BfChopImpChop
   BoxChopImpChop
   BoxChopEqvChop
   BfGen
   LeftChopImpChop
   LeftChopEqvChop
   DfImpDf
   DfEqvDf
   RightChopImpChop
   RightChopEqvChop
   DiamondEqvDiamond
   BoxEqvBox
   BoxImpInferBoxImpBox
   AndChopA
   AndChopB
   AndChopImpChopAndChop
   AndChopCommute
   OrChopEqv
   ChopImpDf
   DfEmpty
   ChopImpDiamond
  8.2 Some Properties of involving the Modal System K and Axiom D
   Mdef
   BfImpDfImpDf
   BfContraPosImpDist
   BfImpDist
   BfImpBfRule
   BfEqvBfRule
   BfAndEqv
   BfEqvSplit
   BfChopEqvChop
   BfImpDfEqvDf
   FiniteImpDfEqvDfRule
   BfImpDf
   DfOrEqv
   BfAndChopImport
  8.3 Some Properties of Chop, and with State Formulas
   DfState
   BfState
   StateChop
   StateChopExportA
   StateAndChopImport
   StateAndChop
   StateAndEmptyChop
   EmptyAndStateChop
   StateAndDf
   StateImpBfGen
   ChopAndNotChopImp
  8.4 Some Properties of involving the Modal System K4
   DfDfEqvDf
   DfNotEqvNotBf
   DfDfNotEqvNotBfBf
   BfBfEqvBf
   BfImpBfBf
  8.5 Properties Involving the PTL Operator
   NextChop
   StateAndNextChop
   DfStateAndNextEqv
  8.6 Some Properties of Together with
   DiamondNotEqvNotBox
   DfDiamondEqvDiamondDf
   DfDiamondNotEqvNotBfBox
   DiamondDfNotEqvNotBoxBf
   BfBoxEqvBoxBf
  8.7 Some Properties of Chop-Star
   ImpMoreChopStarEqvRule
   ImpMoreChopStarChopEqvRule
   SChopStarEqvSChopstarChopEmptyOrChopOmega
  8.8 Some Properties Involving a Reduction to PITL with Finite Time
   FiniteImpBfImpBfRule
   FiniteImpBfEqvBfRule
   BfFinStateEqvBox
  8.9 Some Properties of Skip, Next And Until
   BfMoreImpNLoneEqvMoreImpNLone
   MoreAndNLoneImpBfMoreImpNLone
   BfSkipImpAndNextImpAndSkipAndChop
   BfMoreImpImpBfSkipImp
   BfMoreImpAndNextImpAndSkipAndChop
   DfSkipAndNLoneEqvMoreAndNLone
   DfSkipAndNLoneImpBfSkipImpNLone
   NLoneAndSkipChopEqvNLoneAndNext
   UntilEqv
   UntilImpDiamond

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