Axiomatising first-order temporal logic: Until and since over linear time (Q2563451)

The author presents a complete axiomatisation for first-order temporal logic with the connectives \(U\) (Until) and \(S\) (Since) over all linear time flows. Adding two more axioms, he obtains also a complete axiomatisation over the rational numbers flow of time. The result extends the corresponding one of Burgess for propositional logic, as well as Scott's result for first-order temporal logic with the connectives \(F\) and \(P\), but the proof is by no means a straightforward generalization of them. In fact, he avoids ``datings'' for reducing \(U\), \(S\) to \(F\) and \(P\), and unnatural rules. For the construction of the model of a consistent set of formulas, he uses subtle and nice techniques in order to cope with completeness of quantified formulas (``omega completeness''). The model is constructed a the limit of finite pieces in countably many steps over a subset of the rationals.