A non-reified temporal logic (Q1190791)

The authors present a temporal logic BTK for propositions whose truth values might change as a function of time. The logic is based on a sorted first-order logic where predicates take additional temporal arguments. Temporal and non-temporal values are separated into two disjoint sorts. The semantics of formulae is defined using standard interpretation models for two-sorted predicate logics. The authors discuss issues of proof theory and axiomatization for their logic. The second part of the paper discusses the relation of the presented logic to Shoham's logic [\textit{Y. Shoham}, ibid. 33, 89-104 (1987; Zbl 0633.68014)]. In Shoham's logic temporal arguments are not added as parameters to arbitrary predicates. A special predicate TRUE (defining a so-called reifying context), having as parameters two temporal values and a predicate term, models temporal information. After a discussion of differences between both logics the subsumption of Shoham's logic by BTK is shown.