I would like to know if it is possible to transform simple LTL logic formula i.e.: $G a$ or $F a$ (where $G$ - globally, $F$ - finally) to First Order Logic formula.
I was wondering if the below statements are true under some conditions: $$ Ga = \forall a \\ Fa = \exists a $$
My aim is to use SPASS theorem prover (https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/) to prove simple LTL formulas, but the SPASS is the First Order Logic prover. If it is possible how to present in SPASS syntax statements like: $Ga$ or $Fa$.
A first order formula $T(\varphi)$ equivalent to the LTL formula $\varphi$ can be computed as follows (see these slides): \begin{align} T(a) &= a(x)\\ T(X\varphi) &= ∃y\ (y=x+1)∧T(\varphi)[y/x] \\ T(\varphi \mathop{U} \psi) &= ∃y\ (x \leqslant y) \wedge T(\psi)[y/x] \wedge ∀z\ \bigl((x \leqslant z < y) \rightarrow T(\varphi)[z/x]\bigr) \end{align} For $F$ and $G$, you can use the formulas $F\varphi = \textbf{True} \mathop{U} \varphi$ and $G\varphi = \neg F \neg \varphi$. For instance, $$ Fa = T(\textbf{True} \mathop{U} a) = ∃y\ (x \leqslant y) \wedge a(y) \wedge ∀z\ \bigl((x \leqslant z < y) \rightarrow \textbf{True}(z)\bigr) $$ Note that the opposite conversion (FO to LTL) would be much harder. Indeed, also Propositional LTL over the naturals has the expressive power of FO (Gabbay, Pnueli, Shelah & Stavi, 1980), LTL satisfiability is is PSPACE-complete (Halpern&Reif, 1981, Sistla&Clarke, 1982) while satisfiability of FO over finite words is nonelementary (no bounded-height tower) [Stockmeyer, 1974]. Thus there is no elementary conversion from FO to LTL.