Draft:Kamp's theorem

Kamp's theorem states that linear temporal logic is equivalent to the monadic first-order logic of order over the non-negative integers and the real numbers. It is the oldest result in expressive completeness, the study of determining if a given logic can express a desired subject matter. In temporal logic, a logic ${\mathcal {L}}$ is expressive complete if every first-order formula with one free variable is equivalent to a formula in ${\mathcal {L}}$. The theorem was proven by Hans Kamp in his doctoral thesis, Tense Logic and the Theory of Linear Order (1968). In this thesis, Kamp introduces the $\mathbf {U}$ and $\mathbf {S}$ operators to Prior's tense logic, increasing its expressive power and ensuring expressive completeness.

Formal Statement

A formal statement and proof of Kamp's theorem is provided by Rabinovich. The following is based on his definitions. Let $P$ be a set of atomic predicates.

The syntax for linear temporal logic (LTL) over $P$ is given by the following grammar, where $p\in P$:

${\displaystyle \varphi$ ::=\top \mid p\mid \neg \varphi \mid \varphi \land \varphi \mid \mathbf {X} \varphi \mid \mathbf {F} \varphi \mid \varphi \mathrel {\mathbf {U} } \varphi \mid \mathbf {Y} \varphi \mid \mathbf {P} \varphi \mid \varphi \mathrel {\mathbf {S} } \varphi }

An LTL formula is interpreted over a timeline, which is a quadruple ${\mathcal {T}}=(T,<,s,{\mathcal {I}})$ given by a set of times $T$, a linear order relation $<$ on $T$, a successor relation $s$ such that $(t_{1},t_{2})\in s{\text{ if }}t_{2}{\text{ is the successor of }}t_{1}$, and an interpretation function ${\mathcal {I}}:T\to 2^{P}$. This syntax uses the usual $\mathbf {X} {\text{ and }}\mathbf {U}$ operators, and includes their past duals, $\mathbf {Y} {\text{ and }}\mathbf {S}$, respectively. The satisfaction relation $\models$ is defined as follows, where $t\in T$:

• ${\mathcal {T}},t\models p{\text{ if }}p\in {\mathcal {I}}(t)$
• ${\mathcal {T}},t\models \neg \varphi {\text{ if }}{\mathcal {T}},t\not \models \varphi$
• ${\mathcal {T}},t\models \varphi \land \psi {\text{ if }}{\mathcal {T}},t\models \varphi {\text{ and }}{\mathcal {T}},t\models \psi$
• ${\mathcal {T}},t\models \mathbf {X} \varphi {\text{ if }}s(t,t+1){\text{ and }}{\mathcal {T}},t+1\models \varphi$
• ${\mathcal {T}},t\models \mathbf {F} \varphi {\text{ if there is }}t'\geq t{\text{ such that }}{\mathcal {T}},t'\models \varphi$
• ${\mathcal {T}},t\models \varphi \mathrel {\mathbf {U} } \psi {\text{ if there is }}t'\geq t{\text{ such that }}{\mathcal {T}},t'\models \psi {\text{ and }}{\mathcal {T}},t''\models \varphi {\text{ for all }}t''\in [t,t')$
• ${\mathcal {T}},t\models \mathbf {Y} \varphi {\text{ if }}s(t-1,t){\text{ and }}{\mathcal {T}},t-1\models \varphi$
• ${\mathcal {T}},t\models \mathbf {P} \varphi {\text{ if there is }}t'\leq t{\text{ such that }}{\mathcal {T}},t'\models \varphi$
• ${\mathcal {T}},t\models \varphi \mathrel {\mathbf {S} } \psi {\text{ if there is }}t'\leq t{\text{ such that }}{\mathcal {T}},t'\models \psi {\text{ and }}{\mathcal {T}},t''\models \varphi {\text{ for all }}t''\in (t',t]$

The syntax for monadic first-order logic of order (FOMLO) over $P$ is given by the following grammar, where $p\in P$ and first-order variables are denoted by $t$:

${\displaystyle \varphi$ ::=t<t\mid t=t\mid p(t)\mid \neg \varphi \mid \varphi \land \varphi \mid \exists x\varphi }

The standard satisfaction relation is used, where ${\mathcal {T}},t\models \varphi (x)$ denotes that $\varphi (t)$ holds.

Let ${\mathcal {T}}$ be a timeline such that $T$ is the natural numbers or the real numbers. Kamp's theorem states that every formula in FOMLO is equivalent to a formula in LTL over ${\mathcal {T}}$. That is, for all FOMLO formulas $\varphi (x)$, there exists an LTL formula $\psi$ such that for all $t\in T$, ${\mathcal {T}},t\models \varphi (x)\iff {\mathcal {T}},t\models \psi$. The converse direction is given by the standard translation.

Other Expressive Completeness Results

Unary temporal logic, which is LTL restricted to the operators $\mathbf {X} ,\mathbf {Y} ,\mathbf {F} ,\mathbf {P}$ is equivalent to 2-variable FOMLO.

Metric temporal logic is equivalent to the first-order monadic logic of order and metric, $FO(<,+\mathbb {Q} )$.

Gabbay's separation theorem states the separation property is a necessary and sufficient condition for expressive completeness. Kamp's theorem has been proven through pure syntactic, separation and game arguments.