 Like every formal logical system, temporal logic has two major aspects: a semantic and a deductive one. In this section, we present a deductive system for validity in TL, viz. the minimal temporal logic \(\mathbf{K}_{t}\). The logic \(\mathbf{K}_{t}\) is an axiomatic system, i.e., it is given by a list of axioms and inference rules. The system was first studied by Lemmon, following earlier axiomatizations proposed by Hamblin and Prior (see Rescher and Urquhart 1971, Chapter VI). 