top

An approach to tense logic

R. Bull. An approach to tense logic. Theoria, 36:282–300, 1970.

Download: (unavailable)

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). Øne 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).

BibTeX: (download)

@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). }
}

Generated by bib2html.pl (written by Patrick Riley ) on Mon Aug 10, 2009 14:52:33