Temporal Logic

In this article, I present a formal semantic framework that renders explicit how to reconcile the condition that a proposition about a contingent future event is true at a moment t0 with the idea that at t0, this proposition is ‘truth-maker indeterminate’: a state of affairs making it true will obtain later on, though no such state of affairs obtains at t0. The semantics I formulate employs ‘open temporal models’. They represent the passage of time by a specific component termed (...) time-resource, which acts on durations construed as model-external inputs. A model does not by itself specify which course of events gets actualized in a given duration depending on the latest moment that has already got actualized. A time-resource merely represents schematically the dependence between a moment t and a course of events that gets actualized in a time-span of a given length counted from t; until that much time has indeed passed, it is not fixed which course of events actually extends t. Further, I introduce evaluations as a fine-grained tool for studying truth-conditions of tensed formulas, and I use this tool to define the notion of truth-maker. I define what it means that a truth-maker will obtain but does not, and what it means for a truth-maker to be determinate. It is proven that my semantic analysis retains the desirable link between determinacy and historical necessity—namely, a truth-maker of a proposition being determinate entails that the proposition is historically necessary. (shrink)

I argue that the semantics of sentences expressing future contingent propositions is best viewed as being based on a clear distinction between a time at which a proposition is true and a time at which a state of affairs that makes it true gets actualized. That a prediction is true here and now means that its truth-maker gets actualized later. This is not to say that if a contingent proposition p concerning the future is true at t, it acquires the (...) truth-value true at t only retrospectively, at a later moment. Nor must this be seen as suggesting that it is a settled, unpreventable fact at t that p is true at t. It just means that the reason for its present truth is something that happens later on: the future happens to evolve in such a way as to make a truth-maker of p obtain. In this case, then, it can be said that at t, p is truth-maker indeterminate, or that it has an indeterminate truth-maker. I develop a formal semantics based on this analysis in the follow-up article ‘A Formal Framework for Future Contingents’. Here, I lay down the conceptual framework and indicate Boethius and Abelard as precursors of the view I wish to defend. (shrink)

This is a sequel article to [10] where a hypersequent calculus for some temporal logics of linear frames including Kt4.3 and its extensions for dense and serial flow of time was investigated in detail. A distinctive feature of this approach is that hypersequents are noncommutative, i.e., they are finite lists of sequents in contrast to other hypersequent approaches using sets or multisets. Such a system in [10] was proved to be cut-free HC formalization of respective logics by means of semantical (...) argument. In this article we present an equivalent variant of this calculus for which a constructive syntactical proof of cut elimination is provided. (shrink)

Ewald considered tense operators G, H, F and P on intuitionistic propositional calculus and constructed an intuitionistic tense logic system called IKt. In 2014, Figallo and Pelaitay introduced the variety IKt of IKt-algebras and proved that the IKt system has IKt-algebras as algebraic counterpart. In this paper, we introduce and study the variety of tense Nelson algebras. First, we give some examples and we prove some properties. Next, we associate an IKt-algebra to each tense Nelson algebras. This result allowed us (...) to determine the congruence of the tense Nelson algebras and also to characterize the subdirectly irreducible tense Nelson algebras and particularly the simple tense Nelson algebras. Finally, we prove that there exists an equivalence between the category of IKt-algebras and the category of tense centered Nelson algebras. (shrink)

Is a mathematical theorem proved because provable, or provable because proved? If Brouwer’s intuitionism is accepted, we’re committed, it seems, to the latter, which is highly problematic. Or so I will argue. This and other consequences of Brouwer’s attempt to found mathematics on the intuition of a move of time have heretofore been insufficiently appreciated. Whereas the mathematical anomalies of intuitionism have received enormous attention, too little time, I’ll try to show, has been devoted to some of the temporal anomalies (...) that Brouwer has invited us to introduce into mathematics. (shrink)

Temporaryism—the view that not always everything always exists—comes in two main versions: presentism and expansionism. Both versions of the view are commonly formulated using the notion of being present, which we, among others, find problematic. Expansionism is also sometimes accused of requiring extraordinary conceptual tools for its formulation. In this paper, we put forward systematic characterizations of presentism and expansionism which involve neither the notion of being present nor unfamiliar conceptual tools. These characterizations are full-blown logics, each logic comprising an (...) axiomatic proof system and an intuitive semantics with respect to which the system is both sound and complete. (shrink)

Scopo del volume è offrire un’introduzione accessibile e rigorosa ai più recenti sviluppi di una fondamentale branca della filosofia del tempo: la filosofia del futuro. Vengono presentate e discusse alcune delle domande chiave del dibattito contemporaneo, ad esempio: il futuro è già scritto o esistono molti cammini alternativi che il tempo è in grado di imboccare? "Esistere" significa semplicemente essere presenti o ci sono veri e propri oggetti futuri? Siamo davvero liberi di scegliere quali azioni compiere e di modificare il (...) corso degli eventi? Il dibattito intorno alle risposte di volta in volta offerte in filosofia esplora un’intrigante zona d’intersezione tra metafisica, logica ed etica, e interessa discipline diverse, come la fisica, la psicologia e l’economia. Non sorprende dunque che la discussione contemporanea sia oramai tanto intricata da risultare ostica ai non addetti ai lavori. Il volume offre gli strumenti necessari per inquadrare le domande sul futuro nella loro reale complessità concettuale, introducendo tutte le indispensabili nozioni tecniche in un linguaggio chiaro e intuitivo. (shrink)

La logica modale è nata per studiare i ragionamenti su ciò che è possibile e ciò che è necessario. Negli ultimi decenni, a partire dal lavoro di logici e filosofi quali Rudolf Carnap, Saul Kripke e David Lewis, la sua applicazione è stata progressivamente estesa ad altri ambiti, quali il ragionamento sul tempo, sulla conoscenza e sui sistemi di norme. Queste ricerche hanno condotto a un complesso e intrigante dialogo con alcune fondamentali branche della filosofia: la metafisica, l’epistemologia, la filosofia (...) del linguaggio. Lo scopo del volume è offrire una panoramica di questo dialogo al contempo accessibile e rigorosa, pensata sia per gli studenti di un corso universitario, sia per il lettore non specialista. Se da un lato tutte le necessarie nozioni tecniche sono rese accessibili ai non addetti ai lavori, dall'altro si restituisce un'immagine fedele delle sfide concettuali che la ricerca in questi settori è oggi chiamata ad affrontare. (shrink)

In this work we answer a long standing request for temporal embeddings of deontic STIT logics by introducing the multi-agent STIT logic TDS . The logic is based upon atemporal utilitarian STIT logic. Yet, the logic presented here will be neutral: instead of committing ourselves to utilitarian theories, we prove the logic TDS sound and complete with respect to relational frames not employing any utilitarian function. We demonstrate how these neutral frames can be transformed into utilitarian temporal frames, while preserving (...) validity. Last, we discuss problems that arise from employing binary utility functions in a temporal setting. (shrink)

We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.

We critically review two extant paradigms for understanding the systematic interaction between modality and tense, as well as their respective modifications designed to do justice to the contingency of time’s structure and composition. We show that on either type of theory, as well as their respective modifications, some principles prove logically valid whose truth might sensibly be questioned on metaphysical grounds. These considerations lead us to devise a more general logical framework that allows accommodation of those metaphysical views that its (...) predecessors rule out by fiat. (shrink)

The purpose of the paper is to rethink the role of actuality in the branching model of possibilities. We investigate the idea that the model should be enriched with an additional factor—the so-called Thin Red Line—which is supposed to represent the single possible course of events that gets actualized in time. We believe that this idea was often misconceived which prompted some unfortunate reactions. On the one hand, it suggested problematic semantic models of future tense and and on the other, (...) it provoked questionable lines of criticism. We reassess the debate and point to potential pitfalls, focusing on the semantic dimension of the Thin Red Line theory. Our agenda transcends the semantics, however. We conclude that semantic considerations do not threaten the Thin Red Line theory and that the proper debate should be carried in the domain of metaphysics. (shrink)

In a recently published paper, Patrick Todd (2016, 'Future contingents are all false! On behalf of a Russellian open future') advocates a novel treatment of future contingents. On his view, all statements concerning the contingent future are false. He motivates his semantic postulates by considerations in philosophy of time and modality, in particular by the claim that there is no actual future. I present a number of highly controversial consequences of Todd’s theory. Inadequacy of his semantics might indirectly serve as (...) an argument against the philosophical view underpinning his proposal. (shrink)

I argue that, for all we know, there are perfectly ordinary actual entities that are temporal in the usual sense and yet never present, past, or future. This epistemic fact requires us to modify the theses of presentism and eternalism. More importantly, it generates three new and quite serious objections to presentism, which I formulate and partially evaluate in this paper.

The aim of this paper is to argue that the adoption of an unrestricted principle of bivalence is compatible with a metaphysics that (i) denies that the future is real, (ii) adopts nomological indeterminism, and (iii) exploits a branching structure to provide a semantics for future contingent claims. To this end, we elaborate what we call Flow Fragmentalism, a view inspired by Kit Fine (2005)’s non-standard tense realism, according to which reality is divided up into maximally coherent collections of tensed (...) facts. In this way, we show how to reconcile a genuinely A-theoretic branching-time model with the idea that there is a branch corresponding to the thin red line, that is, the branch that will turn out to be the actual future history of the world. (shrink)

In this research I will focus on a basis for a formal model based on an alternative kind of logic invented by Hans Götzsche: Occurrence Logic (Occ Log), which is not based on truth values and truth functionality. Also, I have taken into account tense logic developed and elaborated by A. N. Prior. In this article I will provide a conceptual and logical foundation for formal Occurrence Logic based on symbolic logic and will illustrate the most important relations between symbolic (...) logic and Occurrence Logic. There will be a special need to focus on arguments based on symbolic occurrence logic. The interrelationships and dependencies between symbolic logic and Occ Log could be conducive to an approach that can express and analyse ‘the occurrences of the world’s descriptions based on various logical principles at different moments’. Symbolic Occ Log checks the occurrence conditioning and the priority of occurrences by employing occurrence values. I shall conclude that the desired approach could gradually support me in providing a truth-functional independent first-order predicate calculus that could work on semantic analysis of different propositions within world descriptions. (shrink)

A complete axiomatic system CTL$_{rp}$ is introduced for a temporal logic for finitely branching $\omega^+$-trees in a temporal language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL* into CTL$_{rp}$. In particular, that yields a complete axiomatization for the translations of all valid CTL*-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a way more expressive medium for reasoning (...) about branching time. (shrink)

The so-called theory of karma is one of the distinguishing aspects of Hinduism and other non-Hindu south-Asian traditions. At the same time that the theory can be seen as closely connected with the freedom of will and action that we humans supposedly have, it has many times been said to be determinist and fatalist. The purpose of this paper is to analyze in some deepness the relations that are between the theory of karma on one side and determinism, fatalism and (...) free-will on the other side. In order to do that, I shall use what has been described as the best formal approach we have to indeterminism: branching time theory. More specifically, I shall introduce a branching time semantic framework in which, among other things, statements such as “state of affairs e is a karmic effect of agent a”, “a wills it to be the case that e” and “e is inevitable” could be properly represented. (shrink)

We present a logic of agency called LAE whose language includes propositional constants for actions and expectations. The logic is based on Von Wright’s theory of agency in general and his analysis of instrumentality in particular. An axiomatization of the logic, including an independence of agents axiom, is provided and soundness and completeness are shown with respect to its intended class of frames. The framework of LAE will allow us to formally define a manifold of concepts involved in agency theories, (...) including Von Wright’s four elementary forms of action, the notion of forbearance and notions of instrumentality that make reference to an agent’s expectations. (shrink)

In this article, we tell a story about incompleteness in modal logic. The story weaves together an article of van Benthem, “Syntactic aspects of modal incompleteness theorems,” and a longstanding open question: whether every normal modal logic can be characterized by a class of completely additive modal algebras, or as we call them, ${\cal V}$-baos. Using a first-order reformulation of the property of complete additivity, we prove that the modal logic that starred in van Benthem’s article resolves the open question (...) in the negative. In addition, for the case of bimodal logic, we show that there is a naturally occurring logic that is incomplete with respect to ${\cal V}$-baos, namely the provability logic $GLB$. We also show that even logics that are unsound with respect to such algebras do not have to be more complex than the classical propositional calculus. On the other hand, we observe that it is undecidable whether a syntactically defined logic is ${\cal V}$-complete. After these results, we generalize the Blok Dichotomy to degrees of ${\cal V}$-incompleteness. In the end, we return to van Benthem’s theme of syntactic aspects of modal incompleteness. (shrink)

We investigate axiomatizability of various fragments of first order computational tree logic showing that the fragments with the modal operator F are non axiomatizable. These results shows that the only axiomatizable fragment is the one with the modal operator next only.

Despite its brevity, McArthur’s monograph offers a helpful introduction to tense logic to readers who have already been introduced to the syntactical and semantical metatheory of classical logic. Familiarity with substitutional quantification, free-logic, and modal logic will help readers appreciate techniques used and the directions in which topics are developed.

The most popular method of incorporating time into a formal logic is based on the work of Arthur Prior. It treats tenses as operators on sentences. In this essay I show a serious problem with that approach, a confusion of scheme versus proposition, which makes any system built in that way incoherent. I will compare how other formal logics deal with the scheme versus proposition distinction and find that only for formal modal logics does the same problem arise. I then (...) compare Prior’s approach to other ways of taking time into account in formal logics. (shrink)

Medieval analyses of molecular propositions include many non-truthfunctional connectives in addition to the standard modern binary connectives (conjunction, disjunction, and conditional). Two types of non-truthfunctional molecular propositions considered by a number of 13th- and 14th-century authors are temporal and local propositions, which combine atomic propositions with `while' and `where'. Despite modern interest in the historical roots of temporal and tense logic, medieval analyses of `while' propositions are rarely discussed in modern literature, and analyses of `where' propositions are almost completely overlooked. (...) In this paper we introduce 13th- and 14th-century views on temporal and local propositions, and connect the medieval theories with modern temporal and spatial counterparts. (shrink)

Shows that a certain temporal logic has infinitely many non-equivalent formulae in a single variable.

The transition semantics presented in Rumberg (J Log Lang Inf 25(1):77–108, 2016a) constitutes a fine-grained framework for modeling the interrelation of modality and time in branching time structures. In that framework, sentences of the transition language L_t are evaluated on transition structures at pairs consisting of a moment and a set of transitions. In this paper, we provide a class of first-order definable Kripke structures that preserves L_t-validity w.r.t. transition structures. As a consequence, for a certain fragment of L_t, validity (...) w.r.t. transition structures turns out to be axiomatizable. The result is then extended to the entire language L_t by means of a quite natural ‘Henkin move’, i.e. by relaxing the notion of validity to bundled structures. (shrink)

In this paper we develop a novel propositional semantics based on the framework of branching time. The basic idea is to replace the moment-history pairs employed as parameters of truth in the standard Ockhamist semantics by pairs consisting of a moment and a consistent, downward closed set of so-called transitions. Whereas histories represent complete possible courses of events, sets of transitions can represent incomplete parts thereof as well. Each transition captures one of the alternative immediate future possibilities open at a (...) branching point. The transition semantics exploits the structural resources a branching time structure has to offer and provides a fine-grained picture of the interrelation of modality and time. In addition to temporal and modal operators, a so-called stability operator becomes interpretable as a universal quantifier over the possible future extensions of a given transition set. The stability operator allows us to specify how and how far time has to unfold for the truth value of a sentence at a moment to become settled and enables a perspicuous treatment of future contingents. We show that the semantics developed along those lines generalizes and extends extant approaches: both Peirceanism and Ockhamism can be viewed as limiting cases of the transition approach that build on restricted resources only, and on both accounts, stability collapses into truth. (shrink)

In this paper we will put forward a novel semantics for future contingents. The idea behind the semantics is to be a compromise position between the ‘Ockhamist’ semantics, first put forward by Prior [1966], Thomason [1970] etc., and a version of the Thin Red Line semantics recently proposed by Malpass and Wawer [2012]. The new position is able to represent alternative possibilities in two different ways, as actual or counterfactual, which corresponds to a similar distinction in two-dimensional semantics between the (...) primary and secondary intension. We prove a theorem about the notion of validity that results from the new definition, which in the context of the literature about TRL-theories and Ockhamism has some significance. (shrink)

In this paper I address issues related to the problem of future contingents and the metaphysical doctrine of fatalism. Two classical responses to the problem of future contingents are the third truth value view and the all-false view. According to the former, future contingents take a third truth value which goes beyond truth and falsity. According to the latter, they are all false. I here illustrate and discuss two ways to respectively argue for those two views. Both ways are similar (...) in spirit and intimately connected with fatalism, in the sense that they engage with the doctrine of fatalism and accept a large part of a standard fatalistic machinery. (shrink)

We define a multi-modal version of Computation Tree Logic (ctl) by extending the language with path quantifiers E δ and A δ where δ denotes one of finitely many dimensions, interpreted over Kripke structures with one total relation for each dimension. As expected, the logic is axiomatised by taking a copy of a ctl axiomatisation for each dimension. Completeness is proved by employing the completeness result for ctl to obtain a model along each dimension in turn. We also show that (...) the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for ctl. We then demonstrate how Normative Systems can be conceived as a natural interpretation of such a multi-dimensional ctl logic. (shrink)

In this paper, we study the introduction of modal past temporal operators in Temporal Equilibrium Logic, an hybrid formalism that mixes linear-time modalities and logic programs interpreted under stable models and their characterisation in terms of Equilibrium Logic. We show that Kamp’s translation can also be used to translate the new extension of TEL with past operators into Quantified Equilibrium Logic. Additionally, we provide a method for removing past operators that consists in replacing past-time subformulas by fresh auxiliary atoms, obtaining (...) an equivalent formula, modulo the original alphabet. (shrink)

We define a multi-modal version of Computation Tree Logic (CTL) by extending the language with path quantifiers $E^\delta $ and $E^\delta $ where δ denotes one of finitely many dimensions, interpreted over Kripke structures with one total relation for each dimension. As expected, the logic is axiomatised by taking a copy of a CTL axiomatisation for each dimension. Completeness is proved by employing the completeness result for CTL to obtain a model along each dimension in turn. We also show that (...) the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for CTL. We then demonstrate how Normative Systems can be conceived as a natural interpretation of such a multi-dimensional CTL logic. (shrink)

Validity of dynamic temporal reasoning is semantically characterized for English and Dutch aspectual adverbs in Discourse Representation Theory. This dynamic perspective determines how the content needs to be revised and what information is preserved across updates, when the order of premises is considered relevant. Resetting contextual parameters relies on modelling the basic aspectual polarity transitions and temporal reasoning extensionally. For intensional aspectual adverbials the speaker’s attitudes regarding past alternatives to and possible continuations of the current state come into play. Additional (...) considerations are offered for generalizing this system to the full logical space for linguistic universals, lexicalized quite differently in Dutch and English. (shrink)

We defend the thesis that every necessarily true proposition is always true. Since not every proposition that is always true is necessarily true, our thesis is at odds with theories of modality and time, such as those of Kit Fine and David Kaplan, which posit a fundamental symmetry between modal and tense operators. According to such theories, just as it is a contingent matter what is true at a given time, it is likewise a temporary matter what is true at (...) a given possible world; so a proposition that is now true at all worlds, and thus necessarily true, may yet at some past or future time be false in the actual world, and thus not always true. We reconstruct and criticize several lines of argument in favor of this picture, and then argue against the picture on the grounds that it is inconsistent with certain sorts of contingency in the structure of time. (shrink)

The various conclusions reached in this paper can be drawn together and briefly summarised in the following thesis: It is necessary to use variables ranging over times explicitly in the object language in the logical analysis of temporal reference in English. A discussion of Arthur Prior ideas, which are in direct opposition to those encompassed here, focuses on the principle that the point of view of the speaker dominates all subordinate clauses, which I maintain and Prior rejects. This leads me (...) to oppose the Priorean approach of considering tenses along the lines of propositional modal operators and in particular to criticise the notion of a proposition with variable truth value. My discussion concerns not only tenses, but also dates, and seeks to provide an account of tenses and dates together in a unified framework. (shrink)

This paper outlines a formal account of tensed sentences that is consistent with Ockhamism, a view according to which future contingents are either true or false. The account outlined substantively differs from the attempts that have been made so far to provide a formal apparatus for such a view in terms of some expressly modified version of branching time semantics. The system on which it is based is the simplest quantified modal logic.

This paper investigates logical aspects of combining linear orders as semantics for modal and temporal logics, with modalities for possible paths, resulting in a variety of branching time logics over classes of trees. Here we adopt a unified approach to the Priorean, Peircean and Ockhamist semantics for branching time logics, by considering them all as fragments of the latter, obtained as combinations, in various degrees, of languages and semantics for linear time with a modality for possible paths. We then consider (...) a hierarchy of natural classes of trees and bundled trees arising from a given class of linear orders and show that in general they provide different semantics. We also discuss transfer of definability from linear orders to trees and introduce a uniform translation from Priorean to Peircean formulae which transfers definability of properties of linear orders to definability of properties of all paths in trees. (shrink)

In this paper we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema's \cdt\ logic interpreted over partial orders (\nsbcdt\ for short). It combines (...) features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management, and it can be easily tailored to most propositional interval temporal logics proposed in the literature. We prove its soundness and completeness, and we show how it has been implemented. (shrink)

We introduce and study hierarchies of extensions of the propositional modal and temporal languages with pairs of new syntactic devices: point of reference-reference pointer which enable semantic references to be made within a formula. We propose three different but equivalent semantics for the extended languages, discuss and compare their expressiveness. The languages with reference pointers are shown to have great expressive power (especially when their frugal syntax is taken into account), perspicuous semantics, and simple deductive systems. For instance, Kamp's and (...) Stavi's temporal operators, as well as nominals (names, clock variables), are definable in them. Universal validity in these languages is proved undecidable. The basic modal and temporal logics with reference pointers are uniformly axiomatized and a strong completeness theorem is proved for them and extended to some classes of their extensions. (shrink)

This paper concerns model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing translation of (...) the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above. (shrink)