4 PITL Axiom System

We now present an axiom system for PITL. Our experience in rigorously developing hundreds of proofs has helped us refine the axioms and convinced us of their utility for a wide range of purposes.

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

  4.1 Axioms and Inference Rules for PITL

Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023