Kamp's theorem

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 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. Explicitly, Kamp shows that the $\mathbf X, \mathbf Y, \mathbf F, \mathbf P$ operators cannot express $\mathbf U$.