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