On the weak completeness of a fragment of linear temporal logic

The main contribution of this work is an expanded and detailed version of a rather sketchy proof, which first appeared in Finger and Gabbay (1992, J. Logic Lang. Inf., 1, 203–233), of a weak completeness theorem for the until-free fragment LTL of linear temporal logic. More precisely we show that LTL is determined by the linearly ordered frame of the natural numbers. As a minor contribution, we also show that, under an ad hoc semantics and with a significant restriction on the admissible valuation maps, LTL can be regarded as a logic for the discrete first quadrant.