Temporal Logic

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)

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)

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)

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 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)

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)

In this paper, we investigate the expressiveness of the variety of propositional interval neighborhood logics , we establish their decidability on linearly ordered domains and some important subclasses, and we prove the undecidability of a number of extensions of PNL with additional modalities over interval relations. All together, we show that PNL form a quite expressive and nearly maximal decidable fragment of Halpern–Shoham’s interval logic HS.

We survey main developments, results, and open problems on interval temporal logics and duration calculi. We present various formal systems studied in the literature and discuss their distinctive features, emphasizing on expressiveness, axiomatic systems, and (un)decidability results.

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)

(...) . (shrink)

لم يكن العلم يومًا غريبًا عن الفلسفة، بل لقد أدت العلاقة الجدلية المستمرة بينهما إلى مزيد من المصداقية والقبول لبعض النماذج التفسيرية، سواء منها ما كان في الأصل نموذجًا فلسفيًا ثم وجد دعمًا علميًا – كنموذج الذرات والفـراغ عند «ديمرقــريطس» وتبنى النظرية الذرية الحديثة لإطاره العام – أو ما كان منها نموذجًا علميًا تم تداوله فلسفيًا – كنموذج النقاط المادية المتجاذبة عند »نيوتن« وتبنى معظم فلاسفة الحقبة الحديثة له. وفي هذا المقال يهتم الدكتور صلاح عثمان بمناقشة نموذج شجرة الكون لفيلسوف (...) العلم الكندي المعاصر «ستورس مكال»، وأوجه الاختلاف بينه وبين النماذج التفسيرية المماثلة القائمة على فكرة متصل الزمان – مكان، ويُركز على ما يقترحه النموذج من حلٍ لواحدةٍ من أصعب مشكلات العلم والمنطق والفلسفة، ألا وهى مشكلة تحديد شروط الصدق للقضايا المنطقية الشرطية المناقضة للواقع؛ أعني تلك التي لا تُعبر عن حوادث وقعت بالفعل، بل كان من المفترض أن تقع، وبالتالي يصعب تحديد قيمة صدق (صادقة أو كاذبة) لها. هذا النوع من القضايا يرتبط ارتباطًا وثيقًا بتصور القانون العلمي، وتحفل به المقاربات التاريخية والخطط المستقبلية للأفراد والحكومات، لذا تعددت محاولات معالجته من قبل الفلاسفة، وهو ما تجلى مثلاً في النظرية الاستدلالية للقضايا الشرطية التي اقترحها «نيلسون جودمان», ونظرية العقول واعتقاداتها للفيلسوف الإنجليزي «فرانك رامزي», ونظرية العوالم الممكنة للفيلسوفين الأمريكيين المعاصـرين «روبرت ستالنيكر»، و«ديفيد لويس»، وأخيرًا نظرية النموذج الشجري لـ «ستورس مكال». وينتهي المقال إلى نتيجة مؤداها نجاح النموذج في معالجة المشكلة، وإن كان ذلك مرهونًا بالتأكيد على موضوعية قيم الصدق والاحتمال التي تحوزها القضايا الشرطية في مقابل الذات المُدركة، تلك التي تنتقل عبر غُرف انتظار متعددة تقترب رويدًا رويدًا من الحقيقة. . (shrink)

1) We will begin by offering a short introduction to Epistemic Logic and presenting Fitch’s paradox in an epistemic‑modal logic. (2) Then, we will proceed to presenting three Epistemic Temporal logical frameworks creat‑ ed by Hoshi (2009) : TPAL (Temporal Public Announcement Logic), TAPAL (Temporal Arbitrary Public Announcement Logic) and TPAL+P ! (Temporal Public Announcement Logic with Labeled Past Operators). We will show how Hoshi stated the Verificationist Thesis in the language of TAPAL and analyze his argument on why this (...) version of it is immune from paradox. (3) Edgington (1985) offered an interpretation of the Verificationist Thesis that blocks Fitch’s paradox and we will propose a way to formulate it in a TAPAL‑based lan‑ guage. The language we will use is a combination of TAPAL and TPAL+P ! with an Indefinite (Unlabeled) Past Operator (TAPAL+P !+P). Using indexed satisfi‑ ability relations (as introduced in (Wang 2010 ; 2011)) we will offer a prospec ‑ tive semantics for this language. We will investigate whether the tentative re‑ formulation of Edgington’s Verificationist Thesis in TAPAL+P !+P is free from paradox and adequate to Edgington’s ideas on how „all truths are knowable“ should be interpreted. (shrink)

It is shown that the infinite-valued first-order Gödel logic G° based on the set of truth values {1/k: k ε w {0}} U {0} is not r.e. The logic G° is the same as that obtained from the Kripke semantics for first-order intuitionistic logic with constant domains and where the order structure of the model is linear. From this, the unaxiomatizability of Kröger's temporal logic of programs (even of the fragment without the nexttime operator O) and of the authors' temporal (...) logic of linear discrete time with gaps follows. (shrink)

The first-order temporal logics with □ and ○ of time structures isomorphic to ω (discrete linear time) and trees of ω-segments (linear time with branching gaps) and some of its fragments are compared: the first is not recursively axiomatizable. For the second, a cut-free complete sequent calculus is given, and from this, a resolution system is derived by the method of Maslov.

At least since Aristotle’s famous 'sea-battle' passages in On Interpretation 9, some substantial minority of philosophers has been attracted to the doctrine of the open future--the doctrine that future contingent statements are not true. But, prima facie, such views seem inconsistent with the following intuition: if something has happened, then (looking back) it was the case that it would happen. How can it be that, looking forwards, it isn’t true that there will be a sea battle, while also being true (...) that, looking backwards, it was the case that there would be a sea battle? This tension forms, in large part, what might be called the problem of future contingents. A dominant trend in temporal logic and semantic theorizing about future contingents seeks to validate both intuitions. Theorists in this tradition--including some interpretations of Aristotle, but paradigmatically, Thomason (1970), as well as more recent developments in Belnap, et. al (2001) and MacFarlane (2003, 2014)--have argued that the apparent tension between the intuitions is in fact merely apparent. In short, such theorists seek to maintain both of the following two theses: (i) the open future: Future contingents are not true, and (ii) retro-closure: From the fact that something is true, it follows that it was the case that it would be true. It is well-known that reflection on the problem of future contingents has in many ways been inspired by importantly parallel issues regarding divine foreknowledge and indeterminism. In this paper, we take up this perspective, and ask what accepting both the open future and retro-closure predicts about omniscience. When we theorize about a perfect knower, we are theorizing about what an ideal agent ought to believe. Our contention is that there isn’t an acceptable view of ideally rational belief given the assumptions of the open future and retro-closure, and thus this casts doubt on the conjunction of those assumptions. (shrink)

Everyone agrees that we can’t change the past. But what about the future? Though the thought that we can change the future is familiar from popular discourse, it enjoys virtually no support from philosophers, contemporary or otherwise. In this paper, I argue that the thesis that the future is mutable has far more going for it than anyone has yet realized. The view, I hope to show, gains support from the nature of prevention, can provide a new way of responding (...) to arguments for fatalism, can account for the utility of total knowledge of the future, and can help in providing an account of the semantics of the English progressive. On the view developed, the future is mutable in the following sense: perhaps, once, it was true that you would never come to read a paper defending the mutability of the future. And then the future changed. And now you will. (shrink)

An examination of McTaggart’s [1908] argument for the unreality of time.

Os presentistas nos dizem que os únicos objetos percorridos pelos quantificadoresde escopo mais amplo são aqueles que existem no presente, o que leva seus críticos aperguntarem o que torna verdadeiros os enunciados sobre o passado, como “Sócrates foi umfilósofo”. Em defesa do presentismo, e seguindo a proposta de Fiocco (2007), argumentamosque o que torna verdadeiro um enunciado sobre o passado é uma proposição, que proposiçõesnão existem no tempo, e que nada na teoria presentista compromete seus defensores com atese de que (...) o que não existe no tempo não existe. (shrink)

Those inclined to positions in the philosophy of time that take tense seriously have typically assumed that not all regions of space-time are equal: one special region of space-time corresponds to what is presently happening. When combined with assumptions from modern physics this has the unsettling consequence that the shape of this favored region distinguishes people in certain places or people traveling at certain velocities. In this paper I shall attempt to avoid this result by developing a tensed picture of (...) reality that is nonetheless consistent with ‘hypersurface egalitarianism’—the view that all hypersurfaces are equal. (shrink)

It is surprisingly hard to define presentism. Traditional definitions of the view, in terms of tensed existence statements, have turned out not to to be capable of convincingly distinguishing presentism from eternalism. Picking up on a recent proposal by Tallant, I suggest that we need to locate the break between eternalism and presentism on a much more fundamental level. The problem is that presentists have tried to express their view within a framework that is inherently eternalist. I call that framework (...) the Fregean nexus, as it is defined by Frege’s atemporal understanding of predication. In particular, I show that the tense-logical understanding of tense which is treated as common ground in the debate rests on this very same Fregean nexus, and is thus inadequate for a proper definition of presentism. I contrast the Fregean nexus with what I call the original temporal nexus, which is based on an alternative, inherently temporal form of predication. Finally, I propose to define presentism in terms of the original temporal nexus, yielding original presentism. According to original presentism, temporal propositions are distinguished from atemporal ones not by aspects of their content, as they are on views based on the Fregean nexus, but by their form—in particular, by their form of predication. (shrink)

Todd (2016) proposes an analysis of future-directed sentences, in particular sentences of the form 'will(φ)', that is based on the classic Russellian analysis of definite descriptions. Todd's analysis is supposed to vindicate the claim that the future is metaphysically open while retaining a simple Ockhamist semantics of future contingents and the principles of classical logic, i.e. bivalence and the law of excluded middle. Consequently, an open futurist can straightforwardly retain classical logic without appeal to supervaluations, determinacy operators, or any further (...) controversial semantical or metaphysical complication. In this paper, we will show that this quasi-Russellian analysis of 'will' both lacks linguistic motivation and faces a variety of significant problems. In particular, we show that the standard arguments for Russell's treatment of definite descriptions fail to apply to statements of the form 'will(φ)'. (shrink)

We investigate the semantics of historical counterfactuals in indeterministic contexts. We claim that "plain" and "necessitated" counterfactuals differ in meaning. To substantiate this claim, we propose a new semantic treatment of historical counterfactuals in the Branching Time framework. We supplement our semantics with supervaluationist postsemantics, thanks to which we can explain away the intuitions which seem to talk in favor of the identification of "would" with "would necessarily".

This paper presents the proof of the apparent nature of relative simultaneity originally derived from Einstein’s Special Theory of Relativity (STR). The proof does not challenge the validity of the STR but uncovers fundamental and widespread error in understanding of practical implications of Lorentz transformations. It is demonstrated that more than a century long debates generally miss the point. This results in counterintuitive claims of coexisting multiple time realities by mere equivalence of equal clock indications and simultaneity. Such claims have (...) little empirical significance but they are substantial in education and philosophy which has become utterly confused after universal acceptance of the STR and rejections of Henri Bergson’s challenge. There is nothing more to “relative simultaneity” other than the effect of identical clocks being shifted by an offset which depends on synchronisation method. (shrink)

Temporal epistemic logics are known, from results of Halpern and Vardi, to have a wide range of complexities of the satisfiability problem: from PSPACE, through non-elementary, to highly undecidable. These complexities depend on the choice of some key parameters specifying, inter alia, possible interactions between time and knowledge, such as synchrony and agents' abilities for learning and recall. In this work we develop practically implementable tableau-based decision procedures for deciding satisfiability in single-agent synchronous temporal-epistemic logics with interactions between time and (...) knowledge. We discuss some complications that occur, even in the single-agent case, when interactions between time and knowledge are assumed and show how the method of incremental tableaux can be adapted to work in EXPSPACE, respectively 2EXPTIME, for these logics, thereby also matching the upper bounds obtained for them by Halpern and Vardi. (shrink)

Simple partial logic (=SPL) is, broadly speaking, an extensional logic which allows for the truth-value gap. First I give a system of propositional SPL by partializing classical logic, as well as extending it with several non-classical truth-functional operators. Second I show a way based on SPL to construct a system of tensed ontology, by representing tensed statements as two kinds of necessary statements in a linear model that consists of the present and future worlds. Finally I compare that way with (...) other two ways based on Łukasiewicz’s three-valued logic and branching temporal logic. (shrink)

There is a familiar debate between Russell and Strawson concerning bivalence and ‘the present King of France’. According to the Strawsonian view, ‘The present King of France is bald’ is neither true nor false, whereas, on the Russellian view, that proposition is simply false. In this paper, I develop what I take to be a crucial connection between this debate and a different domain where bivalence has been at stake: future contingents. On the familiar ‘Aristotelian’ view, future contingent propositions are (...) neither true nor false. However, I argue that, just as there is a Russellian alternative to the Strawsonian view concerning ‘the present King of France’, according to which the relevant class of propositions all turn out false, so there is a Russellian alternative to the Aristotelian view, according to which future contingents all turn out false, not neither true nor false. The result: contrary to millennia of philosophical tradition, we can be open futurists without denying bivalence. (shrink)

The paper argues for the applicability of the notion of collective truth as opposed to distributive truth, that is, truth at times or possibilia taken in groups rather than individually. The underlying reasoning is that there are transtemporal and transworld relationships, e.g., those involving the relations of <being a descendant of> and <thinking about>. Relationships are (one type of) truth-makers. Hence, there are transtemporal and transworld truth-makers. Therefore, there is transtemporal and transworld truth, i.e., collective truth. A semantics is developed (...) (formalized in the appendix) which embodies the notion of collective truth, and which thereby, it is argued, has various advantages over standard intensional semantics. For example, it avoids a commitment to certain impossible entities. (shrink)

Growing-Block theorists hold that past and present things are real, while future things do not yet exist. This generates a puzzle: how can Growing-Block theorists explain the fact that some sentences about the future appear to be true? Briggs and Forbes develop a modal ersatzist framework, on which the concrete actual world is associated with a branching-time structure of ersatz possible worlds. They then show how this branching structure might be used to determine the truth values of future contingents. They (...) point out three different ways of interpreting the logical connectives, which give rise to three different logics of the open future: one supervaluationist, one corresponding to Lukasiewicz's strong Kleene logic, and one intuitionist. (shrink)

ABSTRACT: The modal systems of the Stoic logician Chrysippus and the two Hellenistic logicians Philo and Diodorus Cronus have survived in a fragmentary state in several sources. From these it is clear that Chrysippus was acquainted with Philo’s and Diodorus’ modal notions, and also that he developed his own in contrast of Diodorus’ and in some way incorporated Philo’s. The goal of this paper is to reconstruct the three modal systems, including their modal definitions and modal theorems, and to make (...) clear the exact relations between them; moreover, to elucidate the philosophical reasons that may have led Chrysippus to modify his predessors’ modal concept in the way he did. It becomes apparent that Chrysippus skillfully combined Philo’s and Diodorus’ modal notions, with making only a minimal change to Diodorus’ concept of possibility; and that he thus obtained a modal system of modalities (logical and physical) which fit perfectly fit into Stoic philosophy. (shrink)

This paper assesses branching spacetime theories in light of metaphysical considerations concerning time. I present the A, B, and C series in terms of the temporal structure they impose on sets of events, and raise problems for two elements of extant branching spacetime theories—McCall’s ‘branch attrition’, and the ‘no backward branching’ feature of Belnap’s ‘branching space-time’—in terms of their respective A- and B-theoretic nature. I argue that McCall’s presentation of branch attrition can only be coherently formulated on a model with (...) at least two temporal dimensions, and that this results in severing the link between branch attrition and the flow of time. I argue that ‘no backward branching’ prohibits Belnap’s theory from capturing the modal content of indeterministic physical theories, and results in it ascribing to the world a time-asymmetric modal structure that lacks physical justification. (shrink)