Editing Temporal logic (section)

=== Translation to predicate logic ===
Burgess gives a ''Meredith translation'' from statements in TL into statements in [[first-order logic]] with one free variable {{Var|x}}<sub>0</sub> (representing the present moment). This translation {{Var|M}} is defined recursively as follows:<ref>{{Cite book|title=Philosophical logic|last=Burgess|first=John P.|publisher=Princeton University Press|year=2009|isbn=9781400830497|location=Princeton, New Jersey|page=17|oclc=777375659|author-link=John P. Burgess}}</ref>

:<math>\begin{align}
  & 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{align}</math>

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