A cut-free labelled sequent calculus for dynamic epistemic logic

2020 ◽  
Vol 30 (1) ◽  
pp. 321-348
Author(s):  
Shoshin Nomura ◽  
Hiroakira Ono ◽  
Katsuhiko Sano
Keyword(s):  
Modal Logic ◽  
Epistemic Logic ◽  
Sequent Calculus ◽  
Dynamic Epistemic Logic ◽  
Kripke Semantics ◽  
Cut Rule ◽  
Public Announcement ◽  
Public Announcement Logic ◽  
Soundness And Completeness ◽  
Labelled Sequent Calculus

Abstract Dynamic epistemic logic is a logic that is aimed at formally expressing how a person’s knowledge changes. We provide a cut-free labelled sequent calculus ($\textbf{GDEL}$) on the background of existing studies of Hilbert-style axiomatization $\textbf{HDEL}$ of dynamic epistemic logic and labelled calculi for public announcement logic. We first show that the $cut$ rule is admissible in $\textbf{GDEL}$ and show that $\textbf{GDEL}$ is sound and complete for Kripke semantics. Moreover, we show that the basis of $\textbf{GDEL}$ is extended from modal logic K to other familiar modal logics including S5 with keeping the admissibility of cut, soundness and completeness.

scholarly journals EVERYONE KNOWS THAT SOMEONE KNOWS: QUANTIFIERS OVER EPISTEMIC AGENTS

2019 ◽  
Vol 12 (2) ◽  
pp. 255-270 ◽  
Author(s):  
PAVEL NAUMOV ◽  
JIA TAO
Keyword(s):  
Modal Logic ◽  
Epistemic Logic ◽  
Possible Worlds ◽  
Completeness Theorem ◽  
Kripke Semantics ◽  
Possible Worlds Semantics ◽  
Distributed Knowledge ◽  
First Order ◽  
Soundness And Completeness ◽  
First Order Modal Logic

AbstractModal logic S5 is commonly viewed as an epistemic logic that captures the most basic properties of knowledge. Kripke proved a completeness theorem for the first-order modal logic S5 with respect to a possible worlds semantics. A multiagent version of the propositional S5 as well as a version of the propositional S5 that describes properties of distributed knowledge in multiagent systems has also been previously studied. This article proposes a version of S5-like epistemic logic of distributed knowledge with quantifiers ranging over the set of agents, and proves its soundness and completeness with respect to a Kripke semantics.

scholarly journals POSITIVE LOGIC WITH ADJOINT MODALITIES: PROOF THEORY, SEMANTICS, AND REASONING ABOUT INFORMATION

2010 ◽  
Vol 3 (3) ◽  
pp. 351-373 ◽  
Author(s):  
MEHRNOOSH SADRZADEH ◽  
ROY DYCKHOFF
Keyword(s):  
Modal Logic ◽  
Multiagent Systems ◽  
Epistemic Logic ◽  
Proof Theory ◽  
Sequent Calculus ◽  
Dynamic Epistemic Logic ◽  
Algebraic Semantics ◽  
Sequent Calculi ◽  
Closure Operators ◽  
Positive Logic

We consider a simple modal logic whose nonmodal part has conjunction and disjunction as connectives and whose modalities come in adjoint pairs, but are not in general closure operators. Despite absence of negation and implication, and of axioms corresponding to the characteristic axioms of (e.g.) T, S4, and S5, such logics are useful, as shown in previous work by Baltag, Coecke, and the first author, for encoding and reasoning about information and misinformation in multiagent systems. For the propositional-only fragment of such a dynamic epistemic logic, we present an algebraic semantics, using lattices with agent-indexed families of adjoint pairs of operators, and a cut-free sequent calculus. The calculus exploits operators on sequents, in the style of “nested” or “tree-sequent” calculi; cut-admissibility is shown by constructive syntactic methods. The applicability of the logic is illustrated by reasoning about the muddy children puzzle, for which the calculus is augmented with extra rules to express the facts of the muddy children scenario.

A multi-labelled sequent calculus for Topo-Logic

2020 ◽  
Vol 30 (2) ◽  
pp. 663-696
Author(s):  
Ian Shillito
Keyword(s):  
Structural Properties ◽  
Epistemic Logic ◽  
Search Strategy ◽  
Sequent Calculus ◽  
Search Tree ◽  
Topological Spaces ◽  
Label Technique ◽  
Proof Search ◽  
Labelled Sequent Calculus

Abstract We present a labelled sequent calculus for a trimodal epistemic logic exhibitied in Baltag et al. (2017, Logic, Rationality, and Interaction, pp. 330–346), an extension of the so called ‘Topo-Logic’. To the best of our knowledge, our calculus is the first proof-calculus for this logic. This calculus is obtained via an adaptation of the label technique by internalizing a semantics over topological spaces. This internalization leads to the generation of two kinds of labels in our calculus and the labelling of formulae by pairs of labels. These novelties give tools to provide a simple calculus that is intuitively connected to the semantics. We prove that this calculus enjoys many structural properties such as admissibility of cut, admissibility of contraction and invertibility of its rules. Finally, we exhibit a proof search strategy for our calculus that allows us to prove completeness in a direct way by the extraction of a countermodel from a failure of proof. To define this strategy, we design a tool for controlling the generation of labels in the construction of a search tree, although the termination of this strategy is still open.

scholarly journals Towards a Logic for Reasoning About Learning in a Changing World

10.29007/8g5j ◽  
2018 ◽  
Author(s):  
Prakash Panangaden ◽  
Mehrnoosh Sadrzadeh
Keyword(s):  
Modal Logic ◽  
Epistemic Logic ◽  
Information Acquisition ◽  
Robot Navigation ◽  
Dynamic Epistemic Logic ◽  
The State ◽  
Changing World

We develop an algebraic modal logic that combines epistemic and dynamic modalities with a view to modelling information acquisition (learning) by automated agents in a changing world. Unlike most treatments of dynamic epistemic logic, we have transitions that ``change the state'' of the underlying system and not just the state of knowledge of the agents. The key novel feature that emerges is the need to have a way of ``inverting transitions'' and distinguishing between transitions that ``really happen'' and transitions that are possible.Our approach is algebraic, rather than being based on a Kripke-style semantics. The semantics are given in terms of quantales. We introduce a class of quantales with the appropriate inverse operations and use it to model toy robot-navigation problems, which illustrate how an agent learns information by taking actions. We discuss how a sound and complete logic of the algebra may be obtained from the positive fragment of PDL with converse.

scholarly journals Logics for Knowability

2021 ◽  
pp. 1-42
Author(s):  
Mo Liu ◽  
Jie Fan ◽  
Hans Van Ditmarsch ◽  
Louwe B. Kuijer
Keyword(s):  
Propositional Logic ◽  
Single Agent ◽  
Classical Propositional Logic ◽  
Public Announcement ◽  
Public Announcement Logic ◽  
Multi Agent ◽  
Soundness And Completeness

In this paper, we propose three knowability logics LK, LK−, and LK=. In the single-agent case, LK is equally expressive as arbitrary public announcement logic APAL and public announcement logic PAL, whereas in the multi-agent case, LK is more expressive than PAL. In contrast, both LK− and LK= are equally expressive as classical propositional logic PL. We present the axiomatizations of the three knowability logics and show their soundness and completeness. We show that all three knowability logics possess the properties of Church-Rosser and McKinsey. Although LK is undecidable when at least three agents are involved, LK− and LK= are both decidable.

scholarly journals ‘KNOWABLE’ AS ‘KNOWN AFTER AN ANNOUNCEMENT’

2008 ◽  
Vol 1 (3) ◽  
pp. 305-334 ◽  
Author(s):  
PHILIPPE BALBIANI ◽  
ALEXANDRU BALTAG ◽  
HANS VAN DITMARSCH ◽  
ANDREAS HERZIG ◽  
TOMOHIRO HOSHI ◽  
...  
Keyword(s):  
Epistemic Logic ◽  
Natural Generalization ◽  
Entire Group ◽  
Modal Operator ◽  
Public Announcement ◽  
Public Announcement Logic

Public announcement logic is an extension of multiagent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. We propose an extension of public announcement logic with a dynamic modal operator that expresses what is true after any announcement: ⋄φ expresses that there is a truthful announcement ψ after which φ is true. This logic gives a perspective on Fitch's knowability issues: For which formulas φ, does it hold that φ → ⋄Kφ? We give various semantic results and show completeness for a Hilbert-style axiomatization of this logic. There is a natural generalization to a logic for arbitrary events.

scholarly journals A Modified Subformula Property for the Modal Logic S4.2

2019 ◽  
Vol 48 (1) ◽  
Author(s):  
Mitio Takano
Keyword(s):  
Modal Logic ◽  
Sequent Calculus ◽  
Interpolation Property ◽  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Cut Rule ◽  
Finite Model Property ◽  
Axiom A ◽  
Subformula Property

The modal logic S4.2 is S4 with the additional axiom ◊□A ⊃ □◊A. In this article, the sequent calculus GS4.2 for this logic is presented, and by imposing an appropriate restriction on the application of the cut-rule, it is shown that, every GS4.2-provable sequent S has a GS4.2-proof such that every formula occurring in it is either a subformula of some formula in S, or the formula □¬□B or ¬□B, where □B occurs in the scope of some occurrence of □ in some formula of S. These are just the K5-subformulas of some formula in S which were introduced by us to show the modied subformula property for the modal logics K5 and K5D (Bull Sect Logic 30(2): 115–122, 2001). Some corollaries including the interpolation property for S4.2 follow from this. By slightly modifying the proof, the finite model property also follows.

Sign in / Sign up

Export Citation Format

Share Document