---
tag: CQ0QCQK5JT
kind: statement
role: proposition
name: Kamp's theorem
sources:
  - wikipedia: en:83795911@r1373516405
    locator: Kamp's theorem
    note: adopted
    mention: wikipedia://en/83795911
    sections: [Statement]
same_as:
  wikidata: Q141285148
  wikipedia: Kamp's theorem
inventory: [AB8THS9G4H]
---

## Statement

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|0MWKJ44V5A]] and the [[real numbers|08J2M1JYAG]]. 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. Explicitly, Kamp shows that the $\mathbf X, \mathbf Y, \mathbf F, \mathbf P$ operators cannot express $\mathbf U$.