@ARTICLE{bull70,
author = {R. Bull},
title = {An approach to tense logic},
journal = {Theoria},
year = {1970},
volume = {36},
pages = {282--300},
abstract = {
The author's motivation for constructing the calculi of this paper
is so that time and tense can be "discussed together in the same
language" (p. 282). Two types of enriched propositional caluli for
tense logic are considered, both containing ordinary propositional
variables for which any proposition may be substituted. One type
also contains "clock-propositional" variables, $a,b,c$, etc., for
which only clock-propositional variables may be substituted and that
correspond to instants or moments in the semantics. The other type
also contains "history-propositional" variables, $u,v,w$, etc., for
which only history-propositional variables may be substituted and
that correspond to maximally linearly ordered subsets of instants.
This second type is for tense logics in which time is not linear
and where at any moment there may exist alternative future courses
of events. Quantifiers are included in both types but only for clock-
and history-propositional variables.
However, these quantifiers are given an essentially substitutional
interpretation. In addition, besides each clock-propositional variable
being true at exactly one instant, the semantics requires that for
each instant there be at least one clock-propositional variable true
at that instant, which in effect amounts to having each instant of
the model "denoted" in the formalism by some clock-propositional
variable. Thus it is not surprising that quantification over clock-propositional
variables turns out to have a "well behaved first-order semantics"
(p. 284). \{One axiom relating history- with clock-propositions seems
to need revision: $CKTauTbuAUabUba$. Since the clock-propositional
variables might be true at the same instant the consequent should
include an alternative, namely, $LCab$.\}
Besides the standard truth-functional and tense operators $G,H,F,P$,
the author includes $L$ for "it is always the case that". The model-theoretic
earlier-than relation ordering instants and the semantic truth-at
(an instant) relation are formalized by $Uab$ and $Ta\alpha$ (for
$a$ wff $\alpha$) which are defined respectively as $LCbPa$ (whenever
the clock-proposition $b$ is the case the clock-proposition $a$ was
the case) and $LCa\alpha$ ($\alpha$ is the case whenever the clock-proposition
$a$ is the case).
Because the future tense operators are definable in terms of $U$ and
$T$ and the latter are definable in terms of $L$ and $P$, the dual
of $H$, the author notes that his completeness proofs can be restricted
to $L$ and $H$ as primitive and with the future tense operators used
for other interpretations, especially Prior, A.'s indeterminist "it
will be the case that", where time is not linear.
The author concludes with some rather technical observations showing
that "in ordinary tense logics the instants are nonstandard elements
of the models. This provides", according to the author, "a semantic
pressure to build the instants into tense logic, so that they will
appear as standard elements in the models" (p. 283). }
}