Sain investigates soundness and completeness issues in first-order temporal logics. The focus of the paper is on nonstandard characterizations of the power of temporal proof systems. (In a nonstandard result, time is not necessarily assumed to be isomorphic to the natural numbers; transfinite times are possible.)

Some time ago, I had obtained soundness and completeness results that relied on the definition and use of a formal notion of “clocks.” Roughly, those results assume the existence of a variable that keeps changing values, like a clock. This paper proves that these clocks are in fact needed for completeness. It also addresses other difficult open problems in the area and corrects an unfortunate mistake I had made. The proofs are clever and puzzling at times, as is often the case in nonstandard studies. Therefore, the paper is challenging, but it should be of interest to researchers in the foundations of verification methods.