Temporal logic

The language of the logic first published in Podstawy Analizy Metodologicznej Kanonów Milla (The Foundations of a Methodological Analysis of Mill’s Methods) consisted of:[3]

• first-order logic operators ‘¬’, ‘∧’, ‘∨’, ‘→’, ‘≡’, ‘∀’ and ‘∃’
• realization operator U
• functional symbol δ
• propositional variables p₁,p₂,p₃,...
• variables denoting time moments t₁,t₂,t₃,...
• variables denoting time intervals n₁,n₂,n₃,...

The set of terms (denoted by S) is constructed as follows:

• variables denoting time moments or intervals are terms
• if ${\displaystyle \tau \in S}$ and ${\displaystyle \epsilon }$ is a time interval variable, then ${\displaystyle \delta (\tau ,\epsilon )\in S}$

The set of formulas (denoted by For) is constructed as follows:[10]

• all first-order logic formulas are valid
• if ${\displaystyle \tau \in S}$ and ${\displaystyle \phi }$ is a propositional variable, then ${\displaystyle U_{\tau }(\phi )\in For}$
• if ${\displaystyle \phi \in For}$, then ${\displaystyle \neg \phi \in For}$
• if ${\displaystyle \phi ,\psi \in For}$ and ${\displaystyle \circ \in \{\wedge ,\vee ,\rightarrow ,\equiv \}}$, then ${\displaystyle \phi \circ \psi \in For}$
• if ${\displaystyle \phi \in For}$ and ${\displaystyle Q\in \{\forall ,\exists \}}$ and υ is a propositional, moment or interval variable, then ${\displaystyle Q_{\upsilon }\phi \in For}$

1. ${\displaystyle U_{t_{1}}\neg p_{1}\equiv \neg U_{t_{1}}p_{1}}$
2. ${\displaystyle U_{t_{1}}(p_{1}\rightarrow p_{2})\rightarrow (U_{t_{1}}p_{1}\rightarrow U_{t_{1}}p_{2})}$
3. ${\displaystyle U_{t_{1}}((p_{1}\rightarrow p_{2})\rightarrow ((p_{2}\rightarrow p_{3})\rightarrow (p_{1}\rightarrow p_{3})))}$
4. ${\displaystyle U_{t_{1}}(p_{1}\rightarrow (\neg p_{1}\rightarrow p_{2}))}$
5. ${\displaystyle U_{t_{1}}((\neg p_{1}\rightarrow p_{1})\rightarrow p_{1})}$
6. ${\displaystyle \forall _{t_{1}}U_{t_{1}}p_{1}\rightarrow p_{1}}$
7. ${\displaystyle \forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{1},n_{1})}p_{1}\equiv U_{t_{2}}p_{1})}$
8. ${\displaystyle \forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{2},n_{1})}p_{1}\equiv U_{t_{1}}p_{1})}$
9. ${\displaystyle \forall _{t_{1}}\exists _{p_{1}}\forall _{t_{2}}(U_{t_{2}}p_{1}\equiv \forall _{p_{2}}(U_{t_{1}}p_{2}\equiv U_{t_{2}}p_{2}))}$

A minimal syntax for TL is specified with the following BNF grammar:

${\displaystyle \phi$ ::=a\;|\;\bot \;|\;\lnot \phi \;|\;\phi \lor \phi \;|\;G\phi \;|\;H\phi }

where a is some atomic formula.[13]

Kripke models are used to evaluate the truth of sentences in TL. A pair (T, <) of a set T and a binary relation < on T (called "precedence") is called a frame. A model is given by triple (T, <, V) of a frame and a function V called a valuation that assigns to each pair (a, u) of an atomic formula and a time value some truth value. The notion "ϕ is true in a model U=(T, <, V) at time u" is abbreviated U⊨ϕ[u]. With this notation,[14]

Given a class F of frames, a sentence ϕ of TL is

• valid with respect to F if for every model U=(T,<,V) with (T,<) in F and for every u in T, U⊨ϕ[u]
• satisfiable with respect to F if there is a model U=(T,<,V) with (T,<) in F such that for some u in T, U⊨ϕ[u]
• a consequence of a sentence ψ with respect to F if for every model U=(T,<,V) with (T,<) in F and for every u in T, if U⊨ψ[u], then U⊨ϕ[u]

Many sentences are only valid for a limited class of frames. It is common to restrict the class of frames to those with a relation < that is transitive, antisymmetric, reflexive, trichotomic, irreflexive, total, dense, or some combination of these.

Burgess outlines a logic that makes no assumptions on the relation <, but allows for meaningful deductions, based on the following axiom schema:[15]

1. A where A is a tautology of first-order logic
2. G(A→B)→(GA→GB)
3. H(A→B)→(HA→HB)
4. A→GPA
5. A→HFA

with the following rules of deduction:

1. given A→B and A, deduce B (modus ponens)
2. given a tautology A, infer GA
3. given a tautology A, infer HA

One can derive the following rules:

1. Becker's rule: given A→B, deduce TA→TB where T is a tense, any sequence made of G, H, F, and P.
2. Mirroring: given a theorem A, deduce its mirror statement A^§, which is obtained by replacing G by H (and so F by P) and vice versa.
3. Duality: given a theorem A, deduce its dual statement A*, which is obtained by interchanging ∧ with ∨, G with F, and H with P.

Burgess gives a Meredith translation from statements in TL into statements in first-order logic with one free variable x₀ (representing the present moment). This translation M is defined recursively as follows:[16]

${\displaystyle {\begin{aligned}&M(a)&&=a^{*}x_{0}\\&M(\lnot \phi )&&=\lnot M(\phi )\\&M(\phi \land \psi )&&=M(\phi )\land M(\psi )\\&M({\mathsf {G}}\phi )&&=\forall x_{1}(x_{0}<x_{1}\rightarrow M(A^{+}))\\&M({\mathsf {H}}\phi )&&=\forall x_{1}(x_{1}<x_{0}\rightarrow M(A^{+}))\end{aligned}}}$

where ${\displaystyle A^{+}}$ is the sentence ${\displaystyle A}$ with all variable indices incremented by 1 and ${\displaystyle a^{*}}$ is a one-place predicate defined by ${\displaystyle x\mapsto V(a,x)}$.