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

We show how to apply a constructivization technique previously introduced in order to obtain constructive proofs of approximations of simple classical theorems.

In this paper we present a modal interpretation of negation as failure rule which is inspired from that introduced by Gabbay and which applies also to allowed predicate programs. In the last section it is related to Kunen's 3-valued interpretation.