The two pairs of operators and and and obey various standard properties of modal logics. Axiom VPTL helps streamline reasoning involving and . The situation with and is quite diﬀerent since they lack a comparable axiom. Therefore, it is especially beneﬁcial to review some conventional modal systems which assist in organising various useful deductions involving and .

Table 4 summarises some relevant modal systems, various associated axioms and inference rules.

System | Axiom or inference rule | Axiom or rule name
| |

K: | M f ≜¬L¬f | M-def | |

plus | ⊢ L(f ⊃ g) ⊃ (Lf ⊃ Lg) | K | |

plus | ⊢ f ⇒ ⊢ Lf | N | |

T: | K plus | ⊢ Lf ⊃ f | T |

S4: | T plus | ⊢ Lf ⊃ LLf | 4 |

KD4: | K plus 4 and | ⊢ Lf ⊃ M f | D |

Within PITL, as in PTL, the operator can be regarded as the conventional unary necessity modality L and the operator as the dual possibility operator M. The two operators together fulﬁl the requirements of the modal system S4. We do not need to explicitly prove versions of the S4 axioms in Table 4 for and . Rather, any PITL formula which is a substitution instance of a valid S4 formula involving and can be readily deduced using the PITL proof system’s Axiom VPTL. Similarly, inference rules based on S4 can be obtained with Axiom VPTL, Inference Rule BoxGen (which corresponds to the inference rule N of S4) and modus ponens. Moreover, the PITL proof system’s Axiom VPTL permits using any PITL formula which is a substitution instance of some valid PTL formula which can also contain the PTL operator . In view of all this, we do not give much further consideration to aspects of S4 with and .

In contrast to , the PITL operator does not have a comprehensive axiom analogous to VPTL. Therefore, we need to explicitly prove in the PITL axiom system various modal properties of and its dual . If only ﬁnite time is allowed, then and act as an S4 system. However, with inﬁnite time permitted does not fulﬁl the requirements of S4, or even those of the weaker modal system T, because Axiom T fails. Instead, with inﬁnite time fulﬁls the requirements of the modal system KD4 which is strictly weaker than S4.

Here is a list of KD4’s axioms and inference rules and related PITL proofs for :

If only ﬁnite time is allowed, then the implication D does not need to be regarded as an explicit axiom since it can be inferred from any proof system for S4.

It is also worth noting that the related operators and obey the modal system S4 even when inﬁnite time is permitted. However, we prefer to work with and since the use of strong chop simpliﬁes the overall PITL completeness proof.

Conventional model logics usually take L, not M, to be primitive. When we deduce standard modal properties for and in our PITL axiom system, we let M, which corresponds to , be primitive and deﬁne L to be M’s dual (i.e., LA ≜¬M ¬f). This M-based approach goes well with the PITL axioms for chop. Chellas discusses some alternative axiomatisations of modal systems with M as the primitive although none correspond directly to ours. For the system K, we can deduce implication LImpMImpM below for and (see Theorem BfImpDfImpDf later on) and then obtain from it together some other reasoning the more standard axiom K just presented which only mentions L:

⊢ L(f ⊃ g) ⊃ (Mf ⊃ Mg) | LImpMImpM |

The operators and together yield a multi-modal logic with two necessity constructs L and L′ which are commutative:

⊢ LL′f ≡ L′Lf |

This corresponds to our Theorem BfBoxEqvBoxBf given later on.

Below are various theorems and derived inference rules about and for obtaining the axioms M-def (Theorem Mdef) and K (Theorem BfImpDist) found in the modal system K. The associated inference rule N was already proved above as Derived Inference Rule BfGen. We also prove the modal axiom D (Theorem BfImpDf).

In the next proof’s ﬁnal step, recall that EqvChain indicates a chain of equivalences:

Mdef

BfImpDfImpDf

BfContraPosImpDist

BfImpDist

BfImpBfRule

BfEqvBfRule

BfAndEqv

BfEqvSplit

BfChopEqvChop

BfImpDfEqvDf

FiniteImpDfEqvDfRule

BfImpDf

DfOrEqv

BfAndChopImport

BfImpDfImpDf

BfContraPosImpDist

BfImpDist

BfImpBfRule

BfEqvBfRule

BfAndEqv

BfEqvSplit

BfChopEqvChop

BfImpDfEqvDf

FiniteImpDfEqvDfRule

BfImpDf

DfOrEqv

BfAndChopImport