We now present an axiom system for PITL. Our experience in rigorously developing hundreds of proofs has helped us reﬁne the axioms and convinced us of their utility for a wide range of purposes.
For example, any PITL formula of the form f ∨ g ⊃ g is a tautology since it is a substitution instance of the valid nonmodal formula h0 ∨ h1 ⊃ h1. It is not hard to show that all tautologies are themselves valid. Intuitively, a formula is a tautology if it does not require any modal reasoning to justify its truth.