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)

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.

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)

To counter a general belief that all the paradoxes stem from a kind of circularity (or involve some self--reference, or use a diagonal argument) Stephen Yablo designed a paradox in 1993 that seemingly avoided self--reference. We turn Yablo's paradox, the most challenging paradox in the recent years, into a genuine mathematical theorem in Linear Temporal Logic (LTL). Indeed, Yablo's paradox comes in several varieties; and he showed in 2004 that there are other versions that are equally paradoxical. Formalizing (...) these versions of Yablo's paradox, we prove some theorems in LTL. This is the first time that Yablo's paradox(es) become new(ly discovered) theorems in mathematics and logic. (shrink)

‎A universal schema for diagonalization was popularized by N. S‎. ‎Yanofsky (2003)‎, ‎based on a pioneering work of F.W‎. ‎Lawvere (1969)‎, ‎in which the existence of a (diagonolized-out and contradictory) object implies the existence of a fixed-point for a certain function‎. ‎It was shown that many self-referential paradoxes and diagonally proved theorems can fit in that schema‎. ‎Here‎, ‎we fit more theorems in the universal‎ ‎schema of diagonalization‎, ‎such as Euclid's proof for the infinitude of the primes and new proofs (...) of G. Boolos (1997) for Cantor's theorem on the non-equinumerosity of a set with its powerset‎. ‎Then‎, ‎in Linear Temporal Logic‎, ‎we show the non-existence of a fixed-point in this logic whose proof resembles the argument of Yablo's paradox (1985‎, ‎1993)‎. ‎Thus‎, ‎Yablo's paradox turns for the first time into a genuine mathematico-logical theorem in the framework of Linear Temporal Logic‎. ‎Again the diagonal schema of the paper is used in this proof; and it is also shown that G. Priest's inclosure schema (1997) can fit in our universal diagonal / fixed-point schema‎. ‎We also show the existence of dominating (Ackermann-like) functions (which dominate a given countable set of functions‎, ‎such as primitive recursive functions) in the schema. (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)

The pandemic has been the most vivid agent of change that many of us have known. But it has not changed everything: plenty of the institutions, norms, and practices that sustain racial capitalism, settler colonialism, and cisheteropatriarchy have either weathered the storm of the crisis or been nourished by its effects. And yet enough has changed for us to see that the pandemic has profoundly recontextualised those structures and systems of violence, bringing us into a fresh negotiation with, for example, (...) the question of how we discuss and imagine freedom. Responding in part to this unexpected provocation, activist-scholars Robyn Maynard and Leanne Betasamosake Simpson forged a collaboration from the lockdown of 2020, corresponding by letter to create their forthcoming book, Rehearsals for Living, due to be published by Haymarket Books (US) and Knopf (Canada) in 2022. In this interview, we asked them to explain the epistolary form of the book and expand on the concept of “rehearsal”, before inviting them to reflect on a series of issues that animate our current crises: the politics of recognition; the notion of apocalypse; ways to disrupt linear temporalities; practises of reciprocity against proprietary logics; the gendered violence of state apparatuses; and worldbuilding as a method of resistance. In their expansive answers, Robyn and Leanne draw on their experiences as organisers and educators, commenting on anticolonial struggles, the Movement for Black Lives, and the rise of abolition discourse. Stressing the need to build a multiplicity of shared homespaces in the face of racial/colonial capitalism and organized abandonment, they challenge us to rethink the predicaments and possibilities of the present, enabling us to imagine futures liberated of extractivist, carceral governance – “planting more liberatory futures in the present”, as Robyn puts it. The task of sowing those seeds is a collective praxis of rewriting the narratives that constitute us, refusing to hear that nothing can change and insisting that everything must. (shrink)

Visual literacy has long been important as a way of reading images beyond mimetic illustration. It also allows the reader to tap into a logic of representation in order to create different representations and narratives. In this essay I argue that images provide crucial temporal complexity to the study of narrative, with particular resonances for narrative historiography. The complex temporality of the image, especially the graphic narrative or comic, points toward a historical time which may be neither linear (...) nor causal. Moreover, images demand interaction from the reader, but offer many avenues of interpretation, suggesting that the reader pay attention to their own constructions of meaning and practices of narrativizing. -/- La litéracie visuelle a longtemps été importante comme façon de lire les images hors de simple illustration mimétique. Elle permet aussi le lecteur d’entrer dans une logique de représentation pour créer des différentes représentations et des différentes narrations. Dans cet essai, je soutiens que les images fournissent une cruciale complexité temporale pour l’étude des narrations, avec valence particuliaire pour l’historiographie narrative. La temporalité complexe de l’image, surtout la narration graphique ou bande dessinée, indique une temporalité historique qui sera peut-être ni linéaire, ni causative. Par ailleurs, les images exigent l’intéraction du lecteur, et au même temps ils offrent plusieurs avenues d’interprétation, ce qui attire l’attention du lecteur à ses propres habitudes de lecture et à ses propres narrations construits. (shrink)