Completeness Theorem for a First Order Linear-time Logic


Zoran Ognjanović


We describe a first order temporal logic over the natural numbers time. It is well known that the corresponding set of all valid formulas is not recursively enumerable, and that there is no finitistic axiomatization. We present an infinitary axiomatization which is sound and complete with respect to the considered logic.