Search

Abstract: For some modal fixed point logics, there are deductive systems that enjoy syntactic cut-elimination. An early example is the system in Pliuskevicius (1991) for LTL. More recent examples are the systems by the authors of this paper for the logic of common knowledge (Brünnler and Studer, 2009) and by Hill and Poggiolesi (2010) for PDL, which are based on a form of deep inference. These logics can be seen as fragments of the modal mu-calculus. Here we are interested in how far this approach can be pushed in general. To this end, we introduce a nested sequent system with syntactic cut-elimination which is incomplete for the modal mu-calculus, but complete with respect to a restricted language that allows only fixed points of a certain form. This restricted language includes the logic of common knowledge and PDL. There is also a traditional sequent system for the modal mu-calculus by Jäger et al. (2008) , without a syntactic cut-elimination procedure. We embed that system into ours and vice versa, thus establishing cut-elimination also for the shallow system, when only the restricted language is considered. [Copyright &y& Elsevier]

Abstract: We first look at an existing infinitary sequent system for common knowledge for which there is no known syntactic cut-elimination procedure and also no known non-trivial bound on the proof-depth. We then present another infinitary sequent system based on nested sequents that are essentially trees and with inference rules that apply deeply inside these trees. Thus we call this system “deep” while we call the former system “shallow”. In contrast to the shallow system, the deep system allows one to give a straightforward syntactic cut-elimination procedure. Since both systems can be embedded into each other, this also yields a syntactic cut-elimination procedure for the shallow system. For both systems we thus obtain an upper bound of on the depth of proofs, where is the Veblen function. [Copyright &y& Elsevier]

Abstract: Systems of explicit mathematics provide an axiomatic framework for representing programs and proving properties of them. We introduce such a system with a new form of power types using a monotone power type generator. These power types allow us to model impredicative overloading. This is a very general form of type dependent computation which occurs in the study of object-oriented programming languages. We also present a set-theoretic interpretation for monotone power types. Thus establishing the consistency our system of explicit mathematics. [Copyright &y& Elsevier]

In this paper we discuss extensions of Feferman''s theory T0 for explicit mathematics by the so-called limit and Mahlo axioms and present a novel approach to constructing natural recursion-theoretic models for (fairly strong) systems of explicit mathematics which is based on nonmonotone inductive definitions. [Copyright &y& Elsevier]

Simplicial complexes are a successful model for distributed computing. They have recently been observed to provide an interesting model for epistemic multi-agent logic where the agents' local states are the main building blocks (instead of the global states). A natural generalization is to study epistemic logic on semi-simplicial sets. However, finding the appropriate modal logic for semi-simplicial models has been an open question. We answer this by introducing the logic of synergistic knowledge and establishing its soundness and completeness. • Exploring simplicial semantics for modal logic based on semi-simplicial sets. • New form of distributed knowledge: Synergistic Knowledge. • Sound and complete system Syn for the language of synergistic knowledge. [ABSTRACT FROM AUTHOR]

Abstract: Modal public announcement logics study how beliefs change after public announcements. However, these logics cannot express the reason for a new belief. Justification logics fill this gap since they can formally represent evidence and justifications for an agent's belief. We present and , two alternative justification counterparts of Gerbrandy–Groeneveld's public announcement logic . We show that is the forgetful projection of both and . We also establish that partially realizes . The question whether a similar result holds for is still open. [Copyright &y& Elsevier]

We observe that removing contraction from a standard sequent calculus for first-order predicate logic preserves completeness for the modal fragment. (© 2008 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Abstract: This paper presents a new model construction for a natural cut-free infinitary version of the propositional modal -calculus. Based on that the completeness of and the related system can be established directly – no detour, for example through automata theory, is needed. As a side result we also obtain a finite, cut-free sound and complete system for the propositional modal -calculus. [Copyright &y& Elsevier]