An axiomatization of the temporal logic with until and since over the real numbers. (English) Zbl 0744.03018

A Hilbert style axiomatization of the temporal logic with connectives \(F\) (in the future) and \(P\) (in the past) and a stronger logic with binary connectives \(U\) (until) and \(S\) (since) for the (flow of time based on) real numbers is presented. The main interest of the paper is devoted to the second logic (US). The completeness result for FP is a familiar one, but in the paper a slightly stronger theorem than standard is proven. In the case of the logic US the situation is more complicated. The compactness theorem fails in this logic (for real numbers). A consequence of this result is that a standard completeness theorem does not hold. A weaker completeness result is proven. First a model of a (consistent) formula with flow of time isomorphic to the rationals is built. Thereafter the model is used as a guide when constructing a model with the flow of time based on the real numbers. It is proven that the axiomatization given is finitely complete for the class of flows of time based on the real numbers. (A set of axiom schemas is finitely complete for a class \(K\) of flows of time, if for all formulas \(A\), \(A\) is consisten iff there is a structure \(N\) with flow of time in \(K\) such that \(N\) is a model of \(A\)).


03B45 Modal logic (including the logic of norms)
Full Text: DOI