Temporal reference in linear tense logic (Q965860)

This detailed paper presents a first-order theory, ET, within predicate linear tense logic (K4.\(3_t\)) which enables reference to individual times and in which `now' and `then' can be formalized. This theory contains a single short axiom in addition to those for first-order linear tense logic. That axiom is \(\exists x(\phi_N x\wedge G\sim\phi_N x)\), or simply \(\exists xNx\), where `\(Nx\)' abbreviates `\(\phi_Nx\wedge G\sim\phi_N x\)', for a single designated predicate \(\phi_N\). It is noteworthy that the reference to times does not require a special class of singular terms; all the work is done by regular individual variables and quantifiers and the predicate \(\phi_N\). The bulk of the paper establishes the expressive adequacy of ET and various properties of models in which the axiom is valid. This demonstrates that \(N\) itself possesses appropriate properties. This approach is then contrasted with other methods of extending the expressive capacity of predicate tense logic, and briefly generalized to other forms of modal and tense logics.