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 somevalid 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.