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

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024