We introduce a non-wellfounded proof system for intuitionistic logic extended with inductive and co-inductive definitions, based on a syntax in which fixpoint formulas are annotated with explicit variables for ordinals. We explore the computational content of this system, in particular we introduce a notion of computability and show that every valid proof is computable. As a consequence, we obtain a normalization result for proofs of what we call finitary formulas. A special case of this result is that every proof of a sequent of the appropriate form represents a unique function on natural numbers. Finally, we derive a categorical model from the proof system and show that least and greatest fixpoint formulas correspond to initial algebras and final coalgebras respectively.

Abstract We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations.

We introduce and study a natural extension of the Alternating time temporal logic ATL , called Temporal Logic of Coalitional Goal Assignments (TLCGA). It features one new and quite expressive coalitional strategic operator, called the coalitional goal assignment operator ⦉ γ ⦊, where γ is a mapping assigning to each set of players in the game its coalitional goal , formalised by a path formula of the language of TLCGA, i.e., a formula prefixed with a temporal operator X , U , or G , representing a temporalised objective for the respective coalition, describing the property of the plays on which that objective is satisfied. Then, the formula ⦉ γ ⦊ intuitively says that there is a strategy profile Σ for the grand coalition Agt such that for each coalition C , the restriction Σ | C of Σ to C is a collective strategy of C that enforces the satisfaction of its objective γ (C) in all outcome plays enabled by Σ | C . We establish fixpoint characterizations of the temporal goal assignments in a μ-calculus extension of TLCGA, discuss its expressiveness and illustrate it with some examples, prove bisimulation invariance and Hennessy–Milner property for it with respect to a suitably defined notion of bisimulation, construct a sound and complete axiomatic system for TLCGA, and obtain its decidability via finite model property.

Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open problem. In this paper, we introduce a cut-free sequent calculus for game logic, and two cut-free sequent calculi that manipulate annotated formulas, one for game logic and one for the monotone μ -calculus, the variant of the polymodal μ -calculus where the semantics is given by monotone neighbourhood models instead of Kripke structures. We show these systems are sound and complete, and that completeness of Parikh's axiomatization follows. Our approach builds on recent ideas and results by Afshari & Leigh (LICS 2017) in that we obtain completeness via a sequence of proof transformations between the systems. A crucial ingredient is a validity-preserving translation from game logic to the monotone μ -calculus.

We prove a generic completeness result for a class of modal fixpoint logics corresponding to flat fragments of the two-way mu-calculus, extending earlier work by Santocanale and Venema. We observe that Santocanale and Venema's proof that least fixpoints in the Lindenbaum-Tarski algebra of certain flat fixpoint logics are constructive, using finitary adjoints, no longer works when the converse modality is introduced. Instead, our completeness proof directly constructs a model for a consistent formula, using the induction rule in a way that is similar to the standard completeness proof for propositional dynamic logic. This approach is combined with the concept of a focus, which has previously been used in tableau based reasoning for modal fixpoint logics.

We introduce and study bisimulations for coalgebras on Stone spaces (Kupke et al., 2004, Theoretical Computer Science, 327, 109–134), motivated by previous work on ultrafilter extensions for coalgebras (Kupke et al., 2005, Algebra and Coalgebra in Computer Science, 263–277), bisimulations for the Vietoris functor (Bezhanishvili et al., 2010, Journal of Logic and Computation, 20, 1017–1040) and building on an idea of Gorín and Schröder (2013, Algebra and Coalgebra in Computer Science, 8089, 253–266). We provide a condition under which our notion of bisimulation gives a sound and complete proof method for behavioural equivalence, and show that it generalizes Vietoris bisimulations. Our main technical result proves that the topological closure of any bisimulation between Stone coalgebras in our sense is still a bisimulation. This answers a question raised in Bezhanishvili et al. (2010, Journal of Logic and Computation, 20, 1017–1040), and also leads to a simpler proof of the main theorem in that paper, that the topological closure of a Kripke bisimulation is a Vietoris bisimulation. As a second application of our general bisimulation concept, we study neighbourhood bisimulations on descriptive frames for monotone modal logic as they were introduced in Hansen et al. (2009, Logical Methods in Computer Science, 5, 1–38). From our general results we derive that these are sound and complete for behavioural equivalence and that the topological closure of a neighbourhood bisimulation is still a neighbourhood bisimulation, in analogy with the main result in Bezhanishvili et al. (2010, Journal of Logic and Computation, 20, 1017–1040). Finally, we apply our result to bisimulations for Stone companions of set functors as defined in Kupke et al. (2004, Theoretical Computer Science, 327, 109–134).

We present the concept of a disjunctive basis as a generic framework for normal forms in modal logic based on coalgebra. Disjunctive bases were defined in previous work on completeness for modal fixpoint logics, where they played a central role in the proof of a generic completeness theorem for coalgebraic mu-calculi. Believing the concept has a much wider significance, here we investigate it more thoroughly in its own right. We show that the presence of a disjunctive basis at the "one-step" level entails a number of good properties for a coalgebraic mu-calculus, in particular, a simulation theorem showing that every alternating automaton can be transformed into an equivalent nondeterministic one. Based on this, we prove a Lyndon theorem for the full fixpoint logic, its fixpoint-free fragment and its one-step fragment, and a Uniform Interpolation result, for both the full mu-calculus and its fixpoint-free fragment. We also raise the questions, when a disjunctive basis exists, and how disjunctive bases are related to Moss' coalgebraic "nabla" modalities. Nabla formulas provide disjunctive bases for many coalgebraic modal logics, but there are cases where disjunctive bases give useful normal forms even when nabla formulas fail to do so, our prime example being graded modal logic. Finally, we consider the problem of giving a category-theoretic formulation of disjunctive bases, and provide a partial solution.

Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic interpreted over coalgebras for an arbitrary set functor. We then consider invariance under behavioral equivalence of MSO-formulas. More specifically, we investigate whether the coalgebraic mu-calculus is the bisimulation-invariant fragment of the monadic second-order language for a given functor. Using automatatheoretic techniques and building on recent results by the third author, we show that in order to provide such a characterization result it suffices to find what we call an adequate uniform construction for the coalgebraic type functor. As direct applications of this result we obtain a partly new proof of the Janin-Walukiewicz Theorem for the modal mu-calculus, avoiding the use of syntactic normal forms, and bisimulation invariance results for the bag functor (graded modal logic) and all exponential polynomial functors (including the "game functor"). As a more involved application, involving additional non-trivial ideas, we also derive a characterization theorem for the monotone modal mu-calculus, with respect to a natural monadic second-order language for monotone neighborhood models.

We introduce an axiomatization for the coalgebraic fixed point logic which was introduced by Venema as a generalization, based on Moss' coalgebraic modality, of the well-known modal mu-calculus. Our axiomatization can be seen as a generalization of Kozen's proof system for the modal mu-calculus to the coalgebraic level of generality. It consists of a complete axiomatization for Moss'modality, extended with Kozen's axiom and rule for the fixpoint operators. Our main result is a completeness theorem stating that, for functors that preserve weak pullbacks and restrict to finite sets, our axiomatization is sound and complete for the standard interpretation of the language in coalgebraic models. Our proof is based on automata-theoretic ideas: in particular, we introduce the notion of consequence game for modal automata, which plays a crucial role in the proof of our main result. The result generalizes the celebrated Kozen-Walukiewicz completeness theorem for the modal mu-calculus, and our automata-theoretic methods simplify parts of Walukiewicz' proof.

In a recent article, Alexander Kurz and Yde Venema establish a Lindström theorem for coalgebraic modal logic that is shown to imply a modal Lindström theorem by Maarten de Rijke. A later modal Lindström theorem has been established by Johan van Benthem, and this result still lacks a coalgebraic formulation. The main obstacle has so far been the lack of a suitable notion of ‘submodels’ in coalgebraic semantics, and the problem is left open by Kurz and Venema. In this article, we propose a solution to this problem and derive a general coalgebraic Lindström theorem along the lines of van Benthem's result. We provide several applications of the result.

Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic MSO(T) interpreted over co algebras for an arbitrary set functor T. Similar to well-known results for monadic second-order logic over trees, we provide a translation of this logic into a class of automata, relative to the class of T-co algebras that admit a tree-like supporting Kripke frame. We then consider invariance under behavioral equivalence of MSO(T)-formulas, more in particular, we investigate whether the co algebraic mu-calculus is the bisimulation-invariant fragment of MSO(T). Building on recent results by the third author we show that in order to provide such a co algebraic generalization of the Janin-Walukiewicz Theorem, it suffices to find what we call an adequate uniform construction for the functor T. As applications of this result we obtain a partly new proof of the Janin-Walukiewicz Theorem, and bisimulation invariance results for the bag functor (graded modal logic) and all exponential polynomial functors. Finally, we consider in some detail the monotone neighborhood functor M, which provides co algebraic semantics for monotone modal logic. It turns out that there is no adequate uniform construction for M, whence the automata-theoretic approach towards bisimulation invariance does not apply directly. This problem can be overcome if we consider global bisimulations between neighborhood models: one of our main results provides a characterization of the monotone modal mu-calculus extended with the global modalities, as the fragment of monadic second order logic for the monotone neighborhood functor that is invariant for global bisimulations.

Abstract in UndeterminedInterrogative belief revision is a relatively recent framework for belief revision theory, in which the epistemic state of an agent includes a representation of that agent's research agenda, i.e. the set of questions the agent wants to have answers to. This added structure opens new possibilites for various types of epistemic change that cannot be distinguished in traditional belief revision. In this article I use the so-called 'action model' approach known from the literature on dynamic epistemic logic to provide a unified framework in which we can reason about these various types of epistemic changes. I show how to model some natural examples of epistemic changes involving change of the research agenda in this framework. The action models give rise to a dynamic logic which is proven to be decidable.