Sequent Calculus for Intuitionistic Epistemic Logic IEL

Cut elimination and complexity bounds for intuitionistic epistemic logic

Journal of Logic and Computation ◽

10.1093/logcom/exaa012 ◽

2020 ◽

Vol 30 (1) ◽

pp. 281-294

Author(s):

Vladimir N Krupski

Keyword(s):

Epistemic Logic ◽

Sequent Calculus ◽

Formal System ◽

Point Of View ◽

Cut Elimination ◽

Polynomial Space ◽

Complexity Bounds ◽

Proof Search

Abstract The formal system of intuitionistic epistemic logic (IEL) was proposed by S. Artemov and T. Protopopescu. It provides the formal foundation for the study of knowledge from an intuitionistic point of view based on Brouwer–Heyting–Kolmogorov semantics of intuitionism. We construct a cut-free sequent calculus for IEL and establish that polynomial space is sufficient for the proof search in it. We prove that IEL is PSPACE-complete.

Download Full-text

A multi-labelled sequent calculus for Topo-Logic

Journal of Logic and Computation ◽

10.1093/logcom/exaa021 ◽

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.

Download Full-text

A cut-free labelled sequent calculus for dynamic epistemic logic

Journal of Logic and Computation ◽

10.1093/logcom/exaa014 ◽

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.

Download Full-text

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

The Review of Symbolic Logic ◽

10.1017/s1755020310000134 ◽

2010 ◽

Vol 3 (3) ◽

pp. 351-373 ◽

Cited By ~ 5

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.

Download Full-text