Citations of:
Add citations
You must login to add citations.


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

The transition semantics presented in Rumberg (J Log Lang Inf 25(1):77–108, 2016a) constitutes a finegrained 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 firstorder definable Kripke structures that preserves L_tvalidity w.r.t. transition structures. As a consequence, for a certain fragment of L_t, validity (...) 

There is a longstanding disagreement among BranchingTime theorists. Even though they all believe that the branching representation accurately grasps the idea that the future, contrary to the past, is open, they argue whether this representation is compatible with the claim that one among many possible futures is distinguished—the single future that will come to be. This disagreement is paralleled in an argument about the bivalence of future contingents. The single, privileged future is often called the Thin Red Line. I reconstruct (...) 

In recent years combinations of tense and modality have moved intothe focus of logical research. From a philosophical point of view, logical systems combining tense and modality are of interest because these logics have a wide field of application in original philosophical issues, for example in the theory of causation, of action, etc. But until now only methods yielding completeness results for propositional languages have been developed. In view of philosophical applications, analogous results with respect to languages of predicate logic (...) 

This paper follows Part I of our essay on caseintensional firstorder logic (CIFOL; Belnap and Müller (2013)). We introduce a framework of branching histories to take account of indeterminism. Our system BHCIFOL adds structure to the cases, which in Part I formed just a set: a case in BHCIFOL is a moment/history pair, specifying both an element of a partial ordering of moments and one of the total courses of events (extending all the way into the future) that that moment (...) 

This paper investigates the semantic treatment of conditional obligation, explicit permission (often called positive permission), and prohibition based on models with agents and branched time. In such models branches (rather than moments) are taken as basic, and the branching provides a way to represent the indeterminism which is normally presupposed by talk of free will, responsibility, action and ability. Careful treatment of the relation between ability and responsibility avoids many common problems with accounts of conditional obligation. Recognition of the generality (...) 

I present a variant of with time, called, interpreted in standard Kripke semantics. On the syntactic level, is nothing but the extension of atemporal individual by: the future tense and past tense operators, and the operator of group agency for the grand coalition. A sound and complete axiomatisation for is given. Moreover, it is shown that supports reasoning about interesting normative concepts such as the concepts of achievement obligation and commitment. 

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

This paper follows Part I of our essay on caseintensional ﬁrstorder logic. We introduce a framework of branching histories to take account of indeterminism. Our system BHCIFOL adds structure to the cases, which in Part I formed just a set: a case in BHCIFOL is a moment/history pair, specifying both an element of a partial ordering of moments and one of the total courses of events that that moment is part of. This framework allows us to deﬁne the familiar Ockhamist (...) 

unified treatment of both (families of) interpretations is based on a revised notion of settledness. The main features of this approach are the following: (i) in branching structures, a world can be represented not by a single course of events, but by a node u in the tree, where u itself is seen as the cluster of courses of events passing through it; (ii) the utterance time is uniquely fixed; (iii) the utterance world is not uniquely fixed; (iv) because of (...) 

This paper is predicated on the idea that some modal operators are better understood as quantificational expressions over worlds that determine not only firstorder facts but modal facts also. In what follows, we will present a framework in which these two types of facts are brought closer together. Structural features will be located in the worlds themselves. This result will be achieved by decomposing worlds into parts, where some of these parts will have “modal import” in the sense that they (...) 

This paper deals with structures ${\langle{\bf T}, I\rangle}$ in which T is a tree and I is a function assigning each moment a partition of the set of histories passing through it. The function I is called indistinguishability and generalizes the notion of undividedness. Belnap’s choices are particular indistinguishability functions. Structures ${\langle{\bf T}, I\rangle}$ provide a semantics for a language ${\mathcal{L}}$ with tense and modal operators. The first part of the paper investigates the settheoretical properties of the set of indistinguishability (...) 

The basic notions in Prior’s Ockhamist and Peircean logics of branchingtime are the notion of moment and that of history (or course of events). In the tree semantics, histories are defined as maximal linearly ordered sets of moments. In the geometrical approach, both moments and histories are primitive entities and there is no set theoretical (and ontological) dependency of the latter on the former. In the topological approach, moments can be defined as the elements of a rank 1 base of (...) 

Temporal logic is one of the many areas in which a possible world semantics is adopted. Prior's Ockhamist and Peircean semantics for branchingtime, though, depart from the genuine Kripke semantics in that they involve a quantification over histories, which is a secondorder quantification over sets of possible worlds. In the paper, variants of the original Prior's semantics will be considered and it will be shown that all of them can be viewed as firstorder counterparts of the original semantics. 



Fictional truth, or truth in fiction/pretense, has been the object of extended scrutiny among philosophers and logicians in recent decades. Comparatively little attention, however, has been paid to its inferential relationships with time and with certain deliberate and contingent human activities, namely, the creation of fictional works. The aim of the paper is to contribute to filling the gap. Toward this goal, a formal framework is outlined that is consistent with a variety of conceptions of fictional truth and based upon (...) 

This paper presents two general results of decidability concerning logics based on an indeterministic metric tense logic, which can be applied to, among others, logics combining knowledge, time and agency. We provide a general Kripke semantics based on a variation of the notion of synchronized Ockhamist frames. Our proof of the decidability is by way of the finite frame property, applying subframe transformations and a variant of the filtration technique. 

The thin red line ( TRL ) is a theory about the semantics of futurecontingents. The central idea is that there is such a thing as the ‘actual future’, even in the presence of indeterminism. It is inspired by a famous solution to the problem of divine foreknowledge associated with William of Ockham, in which the freedom of agents is argued to be compatible with God’s omniscience. In the modern branching time setting, the theory of the TRL is widely regarded (...) 

In this paper we propose a method for modeling social influence within the STIT approach to action. Our proposal consists in extending the STIT language with special operators that allow us to represent the consequences of an agent’s choices over the rational choices of another agent. 

The basic notions in Prior's Ockhamist and Peircean logics of branchingtime are the notion of moment and that of history. In the tree semantics, histories are defined as maximal linearly ordered sets of moments. In the geometrical approach, both moments and histories are primitive entities and there is no set theoretical dependency of the latter on the former. In the topological approach, moments can be defined as the elements of a rank 1 base of a nonArchimedean topology on the set (...) 

The semantical structures called T x W frames were introduced in (Thomason, 1984) for the Ockhamist temporalmodal language, $[Unrepresented Character]_{o}$ , which consists of the usual propositional language augmented with the Priorean operators P and F and with a possibility operator ◇. However, these structures are also suitable for interpreting an extended language, $[Unrepresented Character]_{so}$ , containing a further possibility operator $\lozenge^{s}$ which expresses synchronism among possibly incompatible histories and which can thus be thought of as a crosshistory 'simultaneity' operator. (...) 

We present an extension of the mosaic method aimed at capturing manydimensional modal logics. As a proofofconcept, we define the method for logics arising from the combination of linear tense operators with an “orthogonal” S5like modality. We show that the existence of a model for a given set of formulas is equivalent to the existence of a suitable set of partial models, called mosaics, and apply the technique not only in obtaining a proof of decidability and a proof of completeness (...) 