Our PITL axiom system is given in Table 1. Recall that the symbol ⊃ is the logical operator implication used in formulas. In contrast, the metalogical symbol ⇒ denotes the ability to infer a new theorem from other previously deduced ones. The axiom system mainly deals with chop, and skip and operators derived from them. Only one axiom is needed for chop-star.
The axiom system contains some of the propositional axioms suggested by Rosner and Pnueli but also includes our own axioms and inference rule for the operators and chop-star. These assist in deducing theorems and derived inference rules for compositional reasoning. The Axiom Taut permits using properties of conventional nonmodal logic without proof (recall Definition 1 concerning tautologies). It is possible to omit it and achieve the same results by means of a few “lower-level” axioms and inference rules dealing primarily with nonmodal reasoning.
The axiom system gives nearly equal treatment to initial and terminal subintervals. For example, the Inference Rules BiGen and BoxGen respectively provide a means to obtain new theorems by embedding previously deduced PITL theorems in and . This is exceedingly important for the kinds of proofs we do since we naturally move formulas in and out of the left side of chop in many situations. The later embedding of the FL axiom system in the PITL axiom system and the reduction of PITL completeness to FL completeness both involve a lot of this kind of reasoning. The proof of the PITL Replacement Theorem is also a good example of how the analysis of the left side of chop is relevant. We additionally believe that axioms and inference rules concerning make the axiom system easier to understand since much of it consists simply of duals in this sense. In contrast, most temporal logics cannot readily handle initial subintervals since the conventional operators are point-based. Even other axiom systems for ITL largely neglect initial subintervals.
A formula f which is deducible (provable) from the axioms and inferences rules is called an PITL theorem, denoted ⊢ f. When doing proofs, we can observe that a PITL subset in which the only primitive temporal operator is chop and one side is always some fixed formula obeys the rules of the conventional normal modal system K . We now give two sample theorems and their proofs. The justification Prop in some steps refers to conventional propositional reasoning which can involve implicit uses of Axiom Taut and/or modus ponens MP.