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 Deﬁnition 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 ﬁxed formula obeys the rules of the conventional
normal modal system K . We now give two sample theorems and their proofs. The justiﬁcation Prop in
some steps refers to conventional propositional reasoning which can involve implicit uses of Axiom Taut
and/or modus ponens MP.