We shall describe the set of strongly meet irreducible logics in the lattice ϵLin.t of normal tense logics of weak orderings. Based on this description it is shown that all logics in ϵLin.t are independently axiomatizable. Then the description is used in order to investigate tense logics with respect to decidability, finite axiomatizability, axiomatization problems and completeness with respect to Kripke semantics. The main tool for the investigation is a translation of bimodal formulas into a language talking about (...) partitions of general frames into intervals so that relative to both Kripke frames and descriptive frames the expressive power of both languages coincides. (shrink)

This monograph is designed to provide an introduction to the principal areas of tense logic. Many of the developments in this ever-growing field have been intentionally excluded to fulfill this aim. Length also dictated a choice between the alternative notations of A. N. Prior and Nicholas Rescher - two pioneers of the subject. I choose Prior's because of the syntactical parallels with the language it symbolizes and its close ties with other branches of logi cal theory, especially modal (...) logic. The first chapter presents a wider view of the material than later chapters. Several lines of development are consequently not followed through the remainder of the book, most notably metric systems. Although it is import ant to recognize that the unadorned Prior-symbolism can be enriched in vari ous ways it is an advanced subject as to how to actually carry off these enrichments. Readers desiring more information are referred to the appropri ate literature. Specialists will notice that only the first of several quantifi cational versions of tense logic is proven complete in the final chapter. Again constraints of space are partly to blame. The proof for the 'star' systems is wildly complex and at the time of this writing is not yet ready for publi cation. (shrink)

This work aims to make tense logic a more robust tool for ontologists, philosophers, knowledge engineers and programmers by outlining a fusion of tense logic and ontology of time. In order to make tense logic better understandable, the central formal primitives of standard tense logic are derived as theorems from an informal and intuitive ontology of time. In order to make formulation of temporal propositions easier, temporal operators that were introduced by Georg (...) Henrik von Wright are developed, and mapped to the ontology of time. (shrink)

This article surveys some of the key issues that arise when one tries to use tense logic as a metaphysical theory of the nature of time. Topics discussed include basic tense logic, tense logic and verb tense, the structure of the time series, instants of time, quantified tense logic, and the expressive resources of tense logic.

In an earlier paper by the author, Åqvist , I presented an approach to the logic of historical necessity, or inevitability, in the sense of a “two-dimensional” combination of tense and modal logic for worlds, or histories, with the same time order, known as T × W logic. Distinctive features of that approach were, apart from its two-dimensionality, its being based on discrete and finite time, and its use of so-called systematic frame constants in order to (...) enable us to indicate longitudes and latitudes of any points in the co-ordinate systems under consideration. This led us to study and axiomatize an infinite hierarchy HTWxy of two-dimensional modal tense logics with the characteristic operators for historical necessity and possibility added to the original basic vocabulary. The main purpose of the present paper is then twofold: to extend the logics HTWxy to the interesting branch of philosophical logic constituted by deontic logic as combined with tense logic; and to deal with a curious puzzle known as the so-called epistemic obligation paradox – a well known stumbling-block in this area of research in philosophical logic. We argue for a solution to both these problems, which appeals to a new infinite hierarchy DHTWxym of extensions of the HTWxy in the sense of logics combining dyadic deontic modalities with temporal ones such as those for historical necessity and other two-dimensional modalities. (shrink)

In this paper we examine Prior’s reconstruction of Master Argument [4] in some modal-tense logic. This logic consists of a purely tense part and Diodorean definitions of modal alethic operators. Next we study this tense logic in the pure tense language. It is the logic K t 4 plus a new axiom ( P ): ‘ p Λ G p ⊃ P G p ’. This formula was used by Prior in his (...) original analysis of Master Argument. ( P ) is usually added as an extra axiom to an axiomatization of the logic of linear time. In that case the set of moments is a total order and must be left-discrete without the least moment. However, the logic of Master Argument does not require linear time. We show what properties of the set of moments are exactly forced by ( P ) in the reconstruction of Prior. We make also some philosophical remarks on the analyzed reconstruction. (shrink)

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without (...) resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants. (shrink)

This paper deals with the historical and philosophical background of the introduction of the notion of branching time in philosophical logic as it is revealed in the hitherto unpublished mail-correspondence between Saul Kripke and A.N. Prior in the late 1950s. The paper reveals that the idea was first suggested by Saul Kripke in a letter to A.N. Prior, dated September 3, 1958, and it is shown how the elaboration of the idea in the course of the correspondence was intimately (...) intervowen with considerations of how to represent indeterminism and of the adequacy of tensed logic in light of special relativity. The correspondence underpins the point that Prior's later development of branching time may be understood as a crucial part of his attempt at the formulating a conceptual framework integrating basic human notions of time and free choice. (shrink)

This paper argues that the Einstein-Minkowski space-time of special relativity provides an adequate model for classical tense logic, including rigorous definitions of tensed becoming and of the logical priority of proper time. In addition, the extension of classical tense logic with an operator for predicate-term negation provides us with a framework for interpreting and defending the significance of future contingency in special relativity. The framework for future contingents developed here involves the dual falsehood of non-logical contraries, (...) only one of which becomes true. This has several methodological, metaphysical and physical advantages over the alternative traditional frameworks for handling future contingents. (shrink)

Prior has conjectured that the tense-logical system Gli obtained by adding to a complete basis for the classical propositional calculus the primitive symbolG, the definitionsDf. F:Fα=NGNαDf. L:Lα=KαGα,and the postulatesis complete for the logic of linear, infinite, transitive, discrete future time. In this paper it is demonstrated that that conjecture is correct and it is shown that Gli has the finite model property: see [4]. The techniques used are in part suggested by those used in Bull [2] and [3]:Gli (...) can be shown to be complete for the logic of linear, infinite, transitive, discrete future time in the sense that every formula of Gli which is true of such time can be proved as a theorem of Gli. For this purpose the notion of truth needs to be formalized. This formalization is effected by the construction of a model for linear, infinite, transitive, discrete future time. (shrink)

An interpretation in modal and tense logic is proposed for Boethius's reconciliation of God's foreknowledge with human freedom from The consolation of philosophy, Book V. The interpretation incorporates a suggestion by Paul Spade that God's special status in time be explained as a restriction of God's knowledge to eternal sentences. The argument proves valid, and the seeming restriction on omnipotence is mitigated by the very strong expressive power of eternal sentences.

This paper explains how to obtain quantification over times in a tense logic in which all temporal distinctions are ultimately spelled out in terms of the two simple tense operators “it was the case that” and “it will be the case that.” The account of times defended here is similar to what is known as “linguistic ersatzism” about possible worlds, but there are noteworthy differences between these two cases. For example, while linguistic ersatzism would support actualism, the (...) view of times defended here does not support presentism. (shrink)

In this paper we examine Prior's reconstruction of Master Argument [4] in some modal-tense logic. This logic consists of a purely tense part and Diodorean definitions of modal alethic operators. Next we study this tense logic in the pure tense language. It is the logic $K_t 4$ plus a new axiom $:p \wedge Gp \supset PGp'$. This formula was used by Prior in his original analysis of Master Argument. is usually added as (...) an extra axiom to an axiomatization of the logic of linear time. In that case the set of moments is a total order and must be left-discrete without the least moment. However, the logic of Master Argument does not require linear time. We show what properties of the set of moments are exactly forced by in the reconstruction of Prior. We make also some philosophical remarks on the analyzed reconstruction. (shrink)

In a number of publications A.N. Prior considered the use of what he called ‘metric tense logic’. This is a tense logic in which the past and future operators P and F have an index representing a temporal distance, so that Pnα means that α was true n -much ago, and Fn α means that α will be true n -much hence. The paper investigates the use of metric predicate tense logic in formalising phenomena (...) ormally treated by such devices as multiple indexing or quantification over times. (shrink)

We may distinguish between two ways of understanding tense-logical formulae, depending on whether we construe tense operators as operators on sentences or on predicates. Bearing this distinction in mind helps us formalise the premisses of Diodorus Cronus' Master Argument correctly, and give a formal reconstruction of the Argument itself.

According to Hans Kamp and Frank Vlach, the two-dimensional tense operators “now” and “then” are ineliminable in quantified tense logic. This is often adduced as an argument against tense logic, and in favor of an extensional account that makes use of explicit quantification over times. The aim of this paper is to defend tense logic against this attack. It shows that “now” and “then” are eliminable in quantified tense logic, provided we (...) endow it with enough quantificational structure. The operators might not be redundant in some other systems of tense logic, but this merely indicates a lack of quantificational resources and does not show any deep-seated inability of tense logic to express claims about time. The paper closes with a brief discussion of the modal analogue of this issue, which concerns the role of the actuality operator in quantified modal logic. (shrink)

The paper introduces a first-order theory in the language of predicate tense logic which contains a single simple axiom. It is shewn that this theory enables times to be referred to and sentences involving ‘now’ and ‘then’ to be formalised. The paper then compares this way of increasing the expressive capacity of predicate tense logic with other mechanisms, and indicates how to generalise the results to other modal and tense systems.

Based on the results of [11] this paper delivers uniform algorithms for deciding whether a finitely axiomatizable tense logic has the finite model property, is complete with respect to Kripke semantics, is strongly complete with respect to Kripke semantics, is d-persistent, is r-persistent.It is also proved that a tense logic is strongly complete iff the corresponding variety of bimodal algebras is complex, and that a tense logic is d-persistent iff it is complete and its (...) Kripke frames form a first order definable class. From this we obtain many natural non-d-persistent tense logics whose corresponding varieties of bimodal algebras are complex. (shrink)

Although we believe the results reported below to have direct philosophical import, we shall for the most part confine our remarks to the realm of mathematics. The reader is referred to [4] for a philosophically oriented discussion, comprehensible to mathematicians, of tense logic.The “minimal” tense logicT0is the system having connectives ∼, →,F(“at some future time”), andP(“at some past time”); the following axioms:(whereGandHabbreviate ∼F∼ and ∼P∼ respectively); and the following rules:(8) fromαandα → β, inferβ,(9) fromα, infer any substitution (...) instance ofα,(10) fromα, inferGα,(11) fromα, inferHα.A tense logic is a systemTwhose language is that ofT0and whose axioms and rules include (1)–(11). The axioms and rules ofTother than (1)–(11) are calledproperaxioms and rules.We shall investigate three systems of semantics for tense logics, i.e. three notions ofstructureand three relations ⊧ which stand between structures and formulas. One reads⊧αas “αis valid in.” A structureis amodelof a tense logicTif every formula provable inTis valid in. A semantics isadequateforTif the set of models ofTin the semantics is characteristic forT, i.e. if wheneverT ∀ αthen there is a modelofTin the semantics such that∀ α. Two structuresand, possibly from different semantics, are calledequivalent(∼) if exactly the same formulas are valid inas in. (shrink)

The author's motivation for constructing the calculi of this paper\nis so that time and tense can be "discussed together in the same\nlanguage" (p. 282). Two types of enriched propositional caluli for\ntense logic are considered, both containing ordinary propositional\nvariables for which any proposition may be substituted. One type\nalso contains "clock-propositional" variables, a,b,c, etc., for\nwhich only clock-propositional variables may be substituted and that\ncorrespond to instants or moments in the semantics. The other type\nalso contains "history-propositional" variables, u,v,w, etc., for\nwhich only history-propositional (...) variables may be substituted and\nthat correspond to maximally linearly ordered subsets of instants.\nThis second type is for tense logics in which time is not linear\nand where at any moment there may exist alternative future courses\nof events. Quantifiers are included in both types but only for clock-\nand history-propositional variables. However, these quantifiers are\ngiven an essentially substitutional interpretation. In addition,\nbesides each clock-propositional variable being true at exactly one\ninstant, the semantics requires that for each instant there be at\nleast one clock-propositional variable true at that instant, which\nin effect amounts to having each instant of the model "denoted" in\nthe formalism by some clock-propositional variable. Thus it is not\nsurprising that quantification over clock-propositional variables\nturns out to have a "well behaved first-order semantics" (p. 284).\n{One axiom relating history- with clock-propositions seems to need\nrevision: CKTauTbuAUabUba. Since the clock-propositional variables\nmight be true at the same instant the consequent should include an\nalternative, namely, LCab.} Besides the standard truth-functional\nand tense operators G,H,F,P, the author includes L for "it is\nalways the case that". The model-theoretic earlier-than relation\nordering instants and the semantic truth-at (an instant) relation\nare formalized by Uab and Taα (for a wff α) which\nare defined respectively as LCbPa (whenever the clock-proposition\nb is the case the clock-proposition a was the case) and LCaα\n(α is the case whenever the clock-proposition a is the case).\nBecause the future tense operators are definable in terms of U\nand T and the latter are definable in terms of L and P, the\ndual of H, the author notes that his completeness proofs can be\nrestricted to L and H as primitive and with the future tense\noperators used for other interpretations, especially Prior, A.'s\nindeterminist "it will be the case that", where time is not linear.\nThe author concludes with some rather technical observations showing\nthat "in ordinary tense logics the instants are nonstandard elements\nof the models. This provides", according to the author, "a semantic\npressure to build the instants into tense logic, so that they will\nappear as standard elements in the models" (p. 283). (shrink)

Tense logics formulated in the bimodal propositional language are investigated with respect to Kripke-completeness (completeness) and decidability. It is proved that all minimal tense extensions of modal logics of finite width (in the sense of K. Kine) as well as all minimal tense extensions of cofinal subframe logics (in the sense of M. Zakharyaschev) are complete. The decidability of all finitely axiomatizable minimal tense extensions of cofinal subframe logics is shown. A number of variations and extensions (...) of these results are also presented. (shrink)

We prove that all finitely axiomatizable tense logics with temporal operators for ‘always in the future’ and ‘always in the past’ and determined by linear fows time are coNP-complete. It follows, for example, that all tense logics containing a density axiom of the form ■n+1F p → nF p, for some n ≥ 0, are coNP-complete. Additionally, we prove coNP-completeness of all ∩-irreducible tense logics. As these classes of tense logics contain many Kripke incomplete bimodal logics, (...) we obtain many natural examples of Kripke incomplete normal bimodal logics which are nevertheless coNP-complete. (shrink)

Prior's project of tense logic has both a formal-logical and a philosophical side. Both aspects were important for Prior. The paper suggests viewing Prior's philosophical project as a continuation of the tradition of "logic as language", or "universalism", identified by van Heijenoort and Hintikka, respectively. The label "tense-logical universalism" is chosen in order to stress Prior's emphasis on the foundational role of natural language for the three fields of logic, semantics, and philosophy of science. The (...) paper draws on Prior's works in all three mentioned areas. In particular, we comment on Prior's universalist approach to model theory, which has recently given rise to hybrid logic, and on the interesting perspective on relativity theory offered through his writings. (shrink)

In this paper we argue that Prior and Reichenbach are best viewed as allies, not antagonists. We do so by combining the central insights of Prior and Reichenbach in the framework of hybrid tense logic. This overcomes a well-known defect of Reichenbach’s tense schema, namely that it gives multiple representations to sentences in the future perfect and the future-in-the-past. It also makes it easy to define an iterative schema for tense that allows for multiple points of (...) reference, a possibility noted by Prior and demanded by Comrie, and we sketch how this schema can be generalized to a shift-and-restrict pattern in which special propositional symbols act as restrictors on the range of tense operators. (shrink)

Tense logics formulated in the bimodal propositional language are investigated with respect to Kripke-completeness and decidability. It is proved that all minimal tense extensions of modal logics of finite width as well as all minimal tense extensions of cofinal subframe logics are complete. The decidability of all finitely axiomatizable minimal tense extensions of cofinal subframe logics is shown. A number of variations and extensions of these results are also presented.

We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi’s two interaction conditions relating the intuitionistic pre-order with the modal accessibility relation generalize to the requirement that the relation and its inverse be lower semi-continuous with respect to the topology. We then investigate the notion of topological bisimulation relations between topological Kripke frames, as introduced by Aiello and van Benthem, and show that (...) their topology-preserving conditions are equivalent to the properties that the inverse relation and the relation are lower semi-continuous with respect to the topologies on the two models. The first main result is that this notion of topological bisimulation yields semantic preservation w.r.t. topological Kripke models for both intuitionistic tense logics, and for their classical companion multi-modal logics in the setting of the Gödel translation. After giving canonical topological Kripke models for the Hilbert-style axiomatizations of the Fischer Servi logic and its classical companion logic, we use the canonical model in a second main result to characterize a Hennessy–Milner class of topological models between any pair of which there is a maximal topological bisimulation that preserve the intuitionistic semantics. (shrink)

The paper deals with the problem of axiomatizing a system T1 of discrete tense logic, where one thinks of time as the set Z of all the integers together with the operations +1 ("immediate successor") and-1 ("immediate predecessor"). T1 is like the Segerberg-Sundholm system WI in working with so-called infinitary inference ruldes; on the other hand, it differs from W I with respect to (i) proof-theoretical setting, (ii) presence of past tense operators and a "now" operator, and, (...) most importantly, with respect to (iii) the presence in T1 of so-called systematic frame constants, which are meant to hold at exactly one point in a temporal structure and to enable us to express the irreflexivity of such structures. Those frame constants will be seen to play a paramount role in our axiomatization of T1. (shrink)

Review of Tense Logic, ed. by Lennart Åqvist and Frans Guenthner,.