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.

Deﬁnition 1 (Tautology)A tautology is any formula which is a substitution instance of some
valid nonmodal propositional formula.

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 h_{0}∨ h_{1}⊃ h_{1}. 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.