Kamp's theorem

In mathematical logic and computer science, 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 $ℒ$ is expressive complete if every first-order formula with one free variable is equivalent to a formula in $ℒ$. 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 $𝐔$ and $𝐒$ operators to Prior's tense logic, increasing its expressive power and ensuring expressive completeness. Explicitly, Kamp shows that the $𝐗,𝐘,𝐅,𝐏$ operators cannot express $𝐔$.

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$:

$\phi ::=\mathrm{\top }\mid p\mid \mathrm{\neg }\phi \mid \phi \wedge \phi \mid 𝐗\phi \mid 𝐅\phi \mid \phi 𝐔\phi \mid 𝐘\phi \mid 𝐏\phi \mid \phi 𝐒\phi$

An LTL formula is interpreted over a timeline, which is a quadruple $𝒯=(T,<,s,ℐ)$ 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$ if $t_2$ is the successor of $t_1$, and an interpretation function $ℐ:T\to 2^P$. This syntax uses the usual $𝐗$ and $𝐔$ operators, and includes their past duals, $𝐘$ and $𝐒$, respectively. The satisfaction relation $\models$ is defined as follows, where $t\in T$:

• $𝒯,t\models p$ if $p\in ℐ(t)$
• $𝒯,t\models \mathrm{\neg }\phi$ if $𝒯,t\models ̸\phi$
• $𝒯,t\models \phi \wedge \psi$ if $𝒯,t\models \phi$ and $𝒯,t\models \psi$
• $𝒯,t\models 𝐗\phi$ if $s(t,t+1)$ and $𝒯,t+1\models \phi$
• $𝒯,t\models 𝐅\phi$ if there is $t^{\prime }\ge t$ such that $𝒯,t^{\prime }\models \phi$
• $𝒯,t\models \phi 𝐔\psi$ if there is $t^{\prime }\ge t$ such that $𝒯,t^{\prime }\models \psi$ and $𝒯,t^{″}\models \phi$ for all $t^{″}\in [t,t^{\prime })$
• $𝒯,t\models 𝐘\phi$ if $s(t-1,t)$ and $𝒯,t-1\models \phi$
• $𝒯,t\models 𝐏\phi$ if there is $t^{\prime }\le t$ such that $𝒯,t^{\prime }\models \phi$
• $𝒯,t\models \phi 𝐒\psi$ if there is $t^{\prime }\le t$ such that $𝒯,t^{\prime }\models \psi$ and $𝒯,t^{″}\models \phi$ for all $t^{″}\in (t^{\prime },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$:

$\phi ::=t<t\mid t=t\mid p(t)\mid \mathrm{\neg }\phi \mid \phi \wedge \phi \mid \mathrm{\exists }x\phi$

The standard satisfaction relation is used, where $𝒯,t\models \phi (x)$ denotes that $\phi (t)$ holds.

Let $𝒯$ 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 $𝒯$. That is, for all FOMLO formulas $\phi (x)$, there exists an LTL formula $\psi$ such that for all $t\in T$, $𝒯,t\models \phi (x)⟺𝒯,t\models \psi$. The converse direction is given by the standard translation.

Other Expressive Completeness Results

LTL is not expressively complete over the rationals. Stavi provides the connectives ${𝐔}^s$and ${𝐒}^s$such that the logic obtained by extending LTL with these connectives is expressively complete over all linear orders. This result is known as Stavi's theorem.

Unary temporal logic, which is LTL restricted to the operators $𝐗,𝐘,𝐅,𝐏$ 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.