Dynamic epistemic logic (DEL) is a multi-modal logic for reasoning about the change of knowledge in multi-agent systems. It extends epistemic logic by a modal operator for actions which announce logical formulas to other agents. In Hilbert-style proof calculi for DEL, modal action formulas are reduced to epistemic logic, whereas current sequent calculi for DEL are labelled systems which internalize the semantic accessibility relation of the modal operators, as well as the accessibility relation underlying the semantics of the actions. We (...) present a novel cut-free ordinary sequent calculus, called |$ \textbf{G4}_{P,A}[] $|⁠, for propositional DEL. In contrast to the known sequent calculi, our calculus does not internalize the accessibility relations, but—similar to Hilbert style proof calculi—action formulas are reduced to epistemic formulas. Since no ordinary sequent calculus for full S5 modal logic is known, the proof rules for the knowledge operator and the Boolean operators are those of an underlying S4 modal calculus. We show the soundness and completeness of |$ \textbf{G4}_{P,A}[] $| and prove also the admissibility of the cut-rule and of several other rules for introducing the action modality. (shrink)

We present a cut-admissible system for the modal logic S5 in a formalism that makes explicit and intensive use of deep inference. Deep inference is induced by the methods applied so far in conceptually pure systems for this logic. The system enjoys systematicity and modularity, two important properties that should be satisfied by modal systems. Furthermore, it enjoys a simple and direct design: the rules are few and the modal rules are in exact correspondence to the modal axioms.

In classically based modal logic, there are three common conceptions of necessity, the universal conception, the equivalence relation conception, and the axiomatic conception. They provide distinct presentations of the modal logic S5, all of which coincide in the basic modal language. We explore these different conceptions in the context of the relevant logic R, demonstrating where they come apart. This reveals that there are many options for being an S5-ish extension of R. It further reveals a divide between the universal (...) conception of necessity on the one hand, and the axiomatic conception on the other: The latter is consistent with motivations for relevant logics while the former is not. For the committed relevant logician, necessity cannot be the truth in all possible worlds. (shrink)

In this paper, we present a simple sequent calculus for the modal propositional logic S5. We prove that this sequent calculus is theoremwise equivalent to the Hilbert-style system S5, that it is contraction-free and cut-free, and finally that it is decidable. All results are proved in a purely syntactic way.

Decidability of monadic first-order classical logic was established by Löwenheim in 1915. The proof made use of a semantic argument, but a purely syntactic proof has never been provided. In the present paper we introduce a syntactic proof of decidability of monadic first-order logic in innex normal form which exploits G3-style sequent calculi. In particular, we introduce a cut- and contraction-free calculus having a (complexity optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the (...) modal logic T. (shrink)

The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.

We present a rooted hypersequent calculus for modal propositional logic S5. We show that all rules of this calculus are invertible and that the rules of weakening, contraction, and cut are admissible. Soundness and completeness are established as well.

Natural deduction systems for classical, intuitionistic and modal logics were deeply investigated by Prawitz [D. Prawitz, Natural Deduction: A Proof-theoretical Study, in: Stockholm Studies in Philosophy, vol. 3, Almqvist and Wiksell, Stockholm, 1965. Reprinted at: Dover Publications, Dover Books on Mathematics, 2006] from a proof-theoretical perspective. Prawitz proved weak normalization for classical logic only for a language without logical or, there exists and with a restricted application of reduction ad absurdum. Reduction steps related to logical or, there exists and classical (...) negation bring about many problems solved only rather recently. For classical S5 modal logic, Prawitz defined a normalizable system, but for a language without logical or, there exists, ◊ and, for a propositional language without ◊, Medeiros [M.da P.N. Medeiros, A new S4 classical modal logic in natural deduction, Journal of Symbolic Logic 71 799–809] presented a normalizable system for classical S4. We can mention many cut-free Gentzen systems for S4, S5 and K45/K45D, some normalizable natural deduction systems for intuitionistic modal logics and one more for full classical S4, but not for full classical S5. Here our focus is on the definition of a classical and normalizable natural deduction system for S5, taking not only □ and ◊ as primitive symbols, but also all connectives and quantifiers, including classical negation, disjunction and the existential quantifier. The normalization procedure is based on the strategy proposed by Massi [C.D.B. Massi, Provas de normalizaçaõ para a lógica clássica, Ph.D. Thesis, Departamento de Filosofia, UNICAMP, Campinas, 1990] and Pereira and Massi [L.C. Pereira, C.D.B. Massi, Normalização para a lógica clássica, in: O que nos faz pensar, Cadernos de Filosofia da PUC-RJ, vol. 2, 1990, pp. 49–53] for first-order classical logic to cope with the combined use of classical negation, disjunction and the existential quantifier. Here we extend such results to deal with □ and ◊ too. The elimination rule for ◊ uses the notions of connection and of essentially modal formulas already proposed by Prawitz for the introduction of □. Beyond weak normalization, we also prove the subformula property for full S5. (shrink)

We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill’s calculi, and focus on their fragments including multiplicative connectives, additive conjunction and disjunction, brackets and bracket modalities, and the! subexponential modality. For both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut. We also prove algorithmic undecidability for both (...) calculi, and show that categorial grammars based on them can generate arbitrary recursively enumerable languages. (shrink)

We investigate a recent proposal for modal hypersequent calculi. The interpretation of relational hypersequents incorporates an accessibility relation along the hypersequent. These systems give the same interpretation of hypersequents as Lellman's linear nested sequents, but were developed independently by Restall for S5 and extended to other normal modal logics by Parisi. The resulting systems obey Došen's principle: the modal rules are the same across different modal logics. Different modal systems only differ in the presence or absence of external structural rules. (...) With the exception of S5, the systems are modular in the sense that different structural rules capture different properties of the accessibility relation. We provide the first direct semantical cut-free completeness proofs for K, T, and D, and show how this method fails in the case of B and S4. (shrink)

This is primarily a conceptual paper. The goal of the paper is to put into perspective the proof-theory of hybrid logic and in particular, try to give an answer to the following question: Why does the proof-theory of hybrid logic work so well compared to the proof-theory of ordinary modal logic?Roughly, there are two different kinds of proof systems for modal logic: Systems where the formulas involved in the rules are formulas of the object language, that is, ordinary modal-logical formulas, (...) and systems where the formulas involved in the rules are metalingustic formulas obtained by attaching labels representing possible worlds to ordinary modal-logical formulas. Systems of the second kind often also involve an explicit representation of the accessibility relation. From a proof-theoretic point of view, modal-logical systems of the first kind are less well-behaved than systems of the second kind.It turns out that this can be remedied by hybridization, that is, hybridization of modal logics enables the formulation of well-behaved proof systems without involving metalinguistic machinery. What has happened is that the metalinguistic machinery has been internalized in the object language. This gives an answer to the initial question, which is that the proof-theory of hybrid logic works so well because the metalinguistic semantic machinery has been internalized in the object language. (shrink)

A hybrid logic is obtained by adding to an ordinary modal logic further expressive power in the form of a second sort of propositional symbols called nominals and by adding so-called satisfaction operators. In this paper we consider hybridized versions of S5 (“the logic of everywhere”) and the modal logic of inequality (“the logic of elsewhere”). We give natural deduction systems for the logics and we prove functional completeness results.