9 Tense Logic
Arthur Prior introduced tense operators in order to articulate an approach to tense on which it is not to be analyzed in terms of covert quantification over times but rather in terms of propositional operators, which operate on one and the same proposition. Compare, for example, the statements:
There has been an asteroid impact on Earth.
There will be an asteroid impact on Earth.
One approach is to take the statements to involve covert quantification over times:
a. There is a time \(t\) earlier than the time of utterance at which there is an asteroid impact on Earth.
a. There is a time \(t\) later than the time of utterance at which there is an asteroid impact on Earth.
On the other hand, Prior suggested, we may take the statements to involve two tense operators, which act on one and the same proposition:
- b. It has been the case that there is an asteroid impact on Earth
- b. It will be the case that there is an asteroid impact on Earth
These operators act on the proposition expressed by first statement below:
- c. There is an asteroid impact on Earth.
The proposition may change truth value when evaluated relative to one time or another. That proposition has been true, but it is now false.
9.1 Syntax
The language of tense logic \(\mathcal{L}^{\textsf{F}, \textsf{P}}\) includes two primitive tense operators:
\[ \begin{array}{lll} \mathsf{F} \varphi & & \text{It will be the case that} \ \varphi \ \text{at least once in the Future}\\ \mathsf{P} \varphi & & \text{It has been the case that} \ \varphi \ \text{at least once in the Past}\\ \end{array} \]
We begin with stock of propositional variables or atoms:
\[ AT := p, q, r, \cdots \]
We define the formulas of a propositional tense language \(\mathcal{L}^{\textsf{F}, \textsf{P}}\) recursively:
\[ \varphi ::= AT \ | \ \neg \varphi \ | \ (\varphi \to \psi) \ | \ \textsf{F} \varphi \ | \ \textsf{P} \varphi \]
We now define two additional tense operators:
\[ \begin{array}{lll} \textsf{G} \varphi & & \text{It is always Going to the case that} \ \varphi \ \text{in the future}\\ \textsf{H} \varphi & & \text{It Has always been the case that} \ \varphi \ \text{in the past}\\ \end{array} \]
Definition 9.1 (Derived Tenses) \[ \begin{array}{lll} \textsf{G} \varphi & := & \neg \textsf{F} \neg \varphi \\ \textsf{H} \varphi & := & \neg \textsf{P} \neg \varphi \\ \end{array} \]
These operators may be combined into more complex tense expressions:
\[ \begin{array}{lll} \textsf{GF} \varphi & & \text{It is always Going to the case that} \ \varphi \ \\ & & \text{will be the case at least once in the future}\\ \textsf{HP} \varphi & & \text{It has been the case at least once in the past that} \ \varphi \ \\ & & \text{has always been the case in the past}\\ \end{array} \]
9.2 Flow of Time Models
We model the language with the help of what we may call flow of time models:
A flow of time model \(M\) for \(\mathcal{L}^{\textsf{F}, \textsf{P}}\) is a structure \((T, \prec, V)\) where:
\(T\) is a non-empty set of times or temporary states of the world.
\(\prec\) is an earlier than relation on \(T\).
\(V\) maps each propositional variable \(p\) to a set of times \(V(t) \subseteq T\).
We now explain what is for a formula to be true at a time in a flow of time model:
A formula \(\varphi\) is true at a time \(t\) in a flow of time model \(M\), which we write: \(M, t \Vdash \varphi\): \[ \begin{array}{lll} M, t \Vdash p & \text{iff} & t \in V(p)\\ M, t \Vdash \neg \varphi & \text{iff} & M, t \nVdash \varphi\\ M, t \Vdash (\varphi \to \psi) & \text{iff} & M, t \nVdash \varphi \ \text{or} \ M, w \Vdash \psi\\ M, t \Vdash \textsf{F} \varphi & \text{iff} & \text{for some} \ u \in T \ \text{such that} \ t < u, \ M, u \Vdash \varphi\\ M, t \Vdash \textsf{P} \varphi & \text{iff} & \text{for some} \ u \in T \ \text{such that} \ u < t, \ M, u \Vdash \varphi\\ \end{array} \]
Given the definitions of \(\textsf{G}\) and \(\textsf{H}\) in terms of \(\textsf{F}\) and \(\textsf{P}\), we find that \[ \begin{array}{lll} M, t \Vdash \textsf{G} \varphi & \text{iff} & \text{for all} \ u \in W \ \text{such that} \ t < u, \ M, u \Vdash \varphi\\ M, t \Vdash \textsf{H} \varphi & \text{iff} & \text{for all} \ u \in W \ \text{such that} \ u < t, \ M, u \Vdash \varphi\\ \end{array} \]
We finally define what is for a formula to be true at a model.
A formula \(\varphi\) to be true in a flow of time model \(M\), which we write \(M \Vdash \varphi\) if, and only if, for all \(t\in T\), \(M, t \Vdash \varphi\).
Much like in modal propositional logic, flow of time models are based on flow of time frames:
A frame \(F\) for \(\mathcal{L}^{\textsf{F}, \textsf{P}}\) is an ordered pair \((T, \prec)\) where:
\(T\) is a non-empty set of times, and
\(\prec\) is a binary earlier than relation on \(T\)
A model \(M\) is based on a frame \(F = (T, \prec)\) if, and only if, there is an assignment \(V\) such that \(M = (F, V)\). That is, \(M = (V, \prec, V)\).
For a formula \(\varphi\) of \(\mathcal{L}^{\textsf{F},\textsf{P}}\) to be valid in a frame is to be true in every model based on that frame, that is, to be true at every world of every model based on that frame.
A formula \(\varphi\) is valid in a frame \((T, \prec)\), written \((T, \prec) \models \varphi\), if, and only if, \(\varphi\) is true in every model \((T, \prec, V)\) based on the frame \((T, \prec)\).
That is, the formula remains true across assignments no matter what sets of worlds we assign to what propositional variables.
A formula \(\varphi\) is valid in a class of frames \(\mathcal{C}\), written \(\models_{\mathcal{C}} \varphi\) if, and only if, \(\varphi\) is valid in every frame \((T, \prec)\) in the class \(\mathcal{C}\).
We may, however, want to rule out some frames on the grounds that they fail to satisfy plausible constraints on a physical time order. Some of these constraints are listed below along with formulas of tense logic we may use to characterize flow of time frames in which the relevant condition is satisfied.
\[ \begin{array}{lllll} \text{Transitivity} & & u \prec t \wedge t \prec v \to u \prec v & &\textsf{FF} p \to \textsf{F}p \\ & & & & \textsf{G} p \to \textsf{GG}p \\ & & & & \textsf{PP} p \to \textsf{P}p \\ & & & & \textsf{H} p \to \textsf{HH}p \\ & & & & \\ \text{R-Totality} & & u \prec t \wedge u \prec v \to & & (\textsf{F}p \wedge \textsf{F} q) \to \\ & & (t \prec v \vee t = v \vee v \prec t) & & ( \textsf{F}(p \wedge \textsf{F} q) \vee \textsf{F}(p \wedge q) \vee \\ & & & & \textsf{F}(\textsf{F}p \wedge q)) \\ & & & & \\ \text{L-Totality} & & t \prec u \wedge v \prec u \to & & (\textsf{P}p \wedge \textsf{P} q) \to \\ & & (t \prec v \vee t = v \vee v \prec t) & & ( \textsf{P}(p \wedge \textsf{P} q) \vee \textsf{P}(p \wedge q) \vee \\ & & & & \textsf{P}(\textsf{P}p \wedge q))\\ & & & & \\ \text{R-Extendibility} & & \exists t \ u \prec t & & \textsf{G}p \to \textsf{F} p\\ & & & & \\ \text{L-Extendibility} & & \exists t \ t \prec u & & \textsf{H}p \to \textsf{P} p \\ & & & & \\ \text{Density} & & u \prec v \to \exists t \ (u \prec t \wedge t \prec v) & & \textsf{F} p \to \textsf{FF}p \\ & & & & \textsf{GG} p \to \textsf{G}p \\ & & & & \textsf{P} p \to \textsf{PP}p \\ & & & & \textsf{HH} p \to \textsf{H}p \\ \end{array} \]
Consider the case of \(R\)-Totality, for example:
Proposition 9.1 The condition of \(R\)-Totality is modally defined by the axiom
\[ (\textsf{F}p \wedge \textsf{F} q) \to ( \textsf{F}(p \wedge \textsf{F} q) \vee \textsf{F}(p \wedge q) \vee \textsf{F}(\textsf{F}p \wedge q)) \]
Proof. We argue that for every frame \((T, \prec)\),
\[ \begin{array}{lcl} & (T, \prec) \models (\textsf{F}p \wedge \textsf{F} q) \to ( \textsf{F}(p \wedge \textsf{F} q) \vee \textsf{F}(p \wedge q) \vee \textsf{F}(\textsf{F}p \wedge q)) & \\ & \text{iff} & \\ & \forall u \in T \ \forall v \in T \ \forall t \in T \ (u \prec t \wedge u \prec v \to (t \prec v \vee t = v \vee v \prec t)) &\\ \end{array} \]
(\(\Rightarrow\)) Suppose \(\prec\) is not \(R\)-total. Then there are times \(u, v, t\in T\) such that
\[ u \prec t \wedge u \prec v \wedge (t \nprec v \wedge t \neq v \wedge v \nprec t) \]
Consider a valuation \(V\) for which \(V(p) = \{t\}\) and \(V(q) = \{v\}\). Since \(u \prec t\) and \(u \prec v\), \((T, \prec, V), u \Vdash \textsf{F}p \wedge \textsf{F}q\). We now argue that \(u\) falsifies every disjunct in the consequent of the axiom in the model.
Since \(p\) is only true at \(t\) and \(q\) is only true at \(v\), and, furthermore, \(t \nprec v\), \(p \wedge \textsf{F}q\) is false at all times in the model, much less times later than \(u\). It follows that \((T, \prec, V), u \nVdash \textsf{F}(p \wedge \textsf{F}q)\).
Since no time in the model verifies \(p \wedge q\), \((T, \prec, V), u \nVdash \textsf{F}(p \wedge q)\).
Finally, since \(p\) is only true at \(t\) and \(q\) is only true at \(v\), and, furthermore, \(v \nprec t\), \(Fp \wedge q\) is false at all times in the model, much less times later than \(u\). It follows that \((T, \prec, V), u \nVdash \textsf{F}(\textsf{F}p \wedge q)\).
(\(\Leftarrow\)) Suppose \(\prec\) is \(R\)-total. Consider a flow of time model \((T, \prec, V)\) based on a valuation \(V\), and let \(u \in T\) be such that
\[ (T, \prec, V), u \Vdash \textsf{F}p \wedge \textsf{F}q \]
That means that \((T, \prec, V), u \Vdash \textsf{F}p\) and \((T, \prec, V), u \Vdash \textsf{F}q\). That is, there is a time \(v\in T\) such that \(u \prec v\) and \((T, \prec, V), v \Vdash p\) and there is a time \(t\in T\) such that \(u \prec t\) and \((T, \prec, V), t \Vdash q\). Since \(\prec\) is \(R\)-total, we have:
\[ t \prec v \vee t = v \vee v \prec t. \]
We now reason by cases. If \(t \prec v\), then \((T, \prec, V), t \Vdash p \wedge \textsf{F}q\) and \((T, \prec, V), u \Vdash \textsf{F}(p \wedge \textsf{F}q)\). If, on the other hand, \(t = v\), then \((T, \prec, V), t \Vdash p \wedge q\) and \((T, \prec, V), u \Vdash \textsf{F}(p \wedge q)\). Finally, if \(v \prec t\), then \((T, \prec, V), v \Vdash \textsf{F}p \wedge q\) and \((T, \prec, V), u \Vdash \textsf{F}(\textsf{F}p \wedge q)\). Either way:
\[ (T, \prec, V), u \Vdash \textsf{F}(p \wedge \textsf{F}q) \vee \textsf{F}(p \wedge q) \vee \textsf{F}(\textsf{F}p \wedge q). \]
Generalizing,
\[ (T, \prec, V) \Vdash (\textsf{F}p \wedge \textsf{F} q) \to ( \textsf{F}(p \wedge \textsf{F} q) \vee \textsf{F}(p \wedge q) \vee \textsf{F}(\textsf{F}p \wedge q)). \]
Similar arguments are available for other conditions on flow of time frames.
9.3 Axiomatic Derivations
We first introduce the minimal tense logic, which is designed to capture validity in all flow of time frames, and explain how to supplement it with further axioms aimed to place further constraints on temporal order.
9.3.1 The Minimal Tense Logic
The minimal tense logic is sound and complete with respect to the class of all frames.
The minimal tense logic \(\textsf{K}_t\) consists of an infinite set of axioms and two rules of inference.
The axioms of \(\textsf{L}_0\) include:
substitution instances of tautologies of propositional logic
substitution instances of the axioms: \[ \tag{$\textsf{K}_{\textsf{G}}$} \textsf{G}(p \to q) \to (\textsf{G} p \to \textsf{G} q) \] \[ \tag{$\textsf{K}_{\textsf{H}}$} \textsf{H}(p \to q) \to (\textsf{H} p \to \textsf{H} q) \]
substitution instances of the axioms:
\[ \tag{$\textsf{GP}$} p \to \textsf{GP} p \] \[ \tag{$\textsf{HF}$} p \to \textsf{HF} p \]
The rules of inference of \(\textsf{K}\) include:
- Modus Ponens:
\[\tag{$\textsf{MP}$} \varphi, (\varphi \to \psi)/\psi \]
- Temporal Generalization:
\[\tag{$\textsf{TG}_\textsf{G}$} \varphi/\textsf{G} \varphi \]
\[\tag{$\textsf{TG}_{\textsf{H}}$} \varphi/\textsf{H} \varphi \]
The mirror image \(\varphi^M\) of a formula \(\varphi\) is the formula that results from \(\varphi\) when we replace every occurrence of \(\textsf{F}\) in \(\varphi\) with an occurrence of \(\textsf{P}\) in \(\varphi\) and vice versa. That means that every occurrence of \(\textsf{G}\) or \(\neg \textsf{F} \neg\) is replaced by an occurrence of \(\textsf{H}\) and vice versa.
Proposition 9.2 The minimal tense logic is closed under a derived rule of mirror images:
\[ \tag{Mirror} \varphi/\varphi^M \]
Proof. The mirror image of every axiom is itself an axiom, and similarly for the rules of inference. When the mirror image transformation is applied to every line of a proof whose last line is \(\varphi\), the result is still a proof, though now a derivation of \(\varphi^M\),
Proposition 9.3 The minimal tense logic \({\textsf{K}}_t\) is complete with respect to the class of all flow of time frames.
The proof proceeds via the canonical model method. That is, we set out to argue that if \(\varphi\) is not a theorem of \(\textsf{K}_t\), then \(\varphi\) is true at some world \(\Gamma\) of the canonical model \((T_{\textsf{K}_t}, <_{\textsf{K}_t}, V_{\textsf{K}_t})\).
9.3.2 Extensions of the Minimal Tense Logic
Different extensions of the minimal tense logic aim to capture different structural constraints on temporal order. One may, for example, attempt to capture the view that temporal order exemplifies the structure of the rational line. That, in turn, would require one to supplement \(\textsf{L}_0\) with axioms designed to make sure the order is total and extendible in both directions as well as dense.
The complete tense logic for the rational number line \((\mathbb{Q}, <)\) is \(\textsf{K}_t\) supplemented with the axioms:
\[ \begin{array}{lll} & (\textsf{F}p \wedge \textsf{F} q) \to ( \textsf{F}(p \wedge \textsf{F} q) \vee \textsf{F}(p \wedge q) \vee \textsf{F}(\textsf{F}p \wedge q)) & R\text{-Totality}\\ & (\textsf{P}p \wedge \textsf{P} q) \to ( \textsf{P}(p \wedge \textsf{P} q) \vee \textsf{P}(p \wedge q) \vee \textsf{P}(\textsf{P}p \wedge q)) & L\text{-Totality}\\ & \textsf{G}p \to \textsf{F} p & R\text{-Extendibility}\\ & \textsf{H}p \to \textsf{P} p & L\text{-Extendibility}\\ & \textsf{F} p \to \textsf{FF}p & \text{Density} \\ \end{array} \]
The complete tense logic for the real line line \((\mathbb{R}, <)\) supplements the axioms above with a principle designed to make sure the frame is Dedekind-complete:
\[ (\textsf{P}\textsf{F} p \wedge \textsf{F} \textsf{G} \neg p) \to \textsf{P}\textsf{F}(\textsf{G}\neg p \wedge \textsf{H}\textsf{F} p) \]
A flow of time frame \((T, <)\) is Dedekind-complete if, and. only if, every set of time points that has an upper \(R\)-bound has a least upper \(R\)-bound.