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

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

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

A general proof certification framework for modal logic

Mathematical Structures in Computer Science ◽

10.1017/s0960129518000440 ◽

2019 ◽

Vol 29 (8) ◽

pp. 1344-1378

Author(s):

TOMER LIBAL ◽

MARCO VOLPE

Keyword(s):

Modal Logic ◽

General Framework ◽

Sequent Calculus ◽

Specification Language ◽

Sequent Calculi ◽

General Proof ◽

Theorem Provers ◽

Different Sources

One of the main issues in proof certification is that different theorem provers, even when designed for the same logic, tend to use different proof formalisms and produce outputs in different formats. The project ProofCert promotes the usage of a common specification language and of a small and trusted kernel in order to check proofs coming from different sources and for different logics. By relying on that idea and by using a classical focused sequent calculus as a kernel, we propose here a general framework for checking modal proofs. We present the implementation of the framework in a Prolog-like language and show how it is possible to specialize it in a simple and modular way in order to cover different proof formalisms, such as labelled systems, tableaux, sequent calculi and nested sequent calculi. We illustrate the method for the logic K by providing several examples and discuss how to further extend the approach.

Download Full-text

De Finettian Logics of Indicative Conditionals Part II: Proof Theory and Algebraic Semantics

Journal of Philosophical Logic ◽

10.1007/s10992-020-09572-7 ◽

2021 ◽

Author(s):

Paul Égré ◽

Lorenzo Rossi ◽

Jan Sprenger

Keyword(s):

Proof Theory ◽

Future Research ◽

Algebraic Semantics ◽

Sequent Calculi ◽

Truth Conditions ◽

Indicative Conditionals ◽

Tarski Algebra ◽

Soundness And Completeness ◽

Tableau Calculi ◽

The One

AbstractIn Part I of this paper, we identified and compared various schemes for trivalent truth conditions for indicative conditionals, most notably the proposals by de Finetti (1936) and Reichenbach (1935, 1944) on the one hand, and by Cooper (Inquiry, 11, 295–320, 1968) and Cantwell (Notre Dame Journal of Formal Logic, 49, 245–260, 2008) on the other. Here we provide the proof theory for the resulting logics and , using tableau calculi and sequent calculi, and proving soundness and completeness results. Then we turn to the algebraic semantics, where both logics have substantive limitations: allows for algebraic completeness, but not for the construction of a canonical model, while fails the construction of a Lindenbaum-Tarski algebra. With these results in mind, we draw up the balance and sketch future research projects.

Download Full-text

Sequent calculus for logic of correlated knowledge

Lietuvos matematikos rinkinys ◽

10.15388/lmr.2011.ml04 ◽

2011 ◽

Vol 52 ◽

Author(s):

Haroldas Giedra ◽

Jūratė Sakalauskaitė

Keyword(s):

Epistemic Logic ◽

Sequent Calculus ◽

Sequent Calculi

Sound and complete sequent calculi for general epistemic logic and logic of correlated knowledge are presented in this paper.

Download Full-text

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.

Download Full-text

A Cut-Free Labelled Sequent Calculus for Dynamic Epistemic Logic

Logical Foundations of Computer Science - Lecture Notes in Computer Science ◽

10.1007/978-3-319-27683-0_20 ◽

2015 ◽

pp. 283-298 ◽

Cited By ~ 1

Author(s):

Shoshin Nomura ◽

Hiroakira Ono ◽

Katsuhiko Sano

Keyword(s):

Epistemic Logic ◽

Sequent Calculus ◽

Dynamic Epistemic Logic ◽

Labelled Sequent Calculus

Download Full-text

A contribution to automated-oriented reasoning about permutability of sequent calculi rules

Computer Science and Information Systems ◽

10.2298/csis120820043l ◽

2013 ◽

Vol 10 (3) ◽

pp. 1185-1210 ◽

Cited By ~ 1

Author(s):

Tatjana Lutovac ◽

James Harland

Keyword(s):

Proof Theory ◽

Sequent Calculus ◽

Sufficient Conditions ◽

General Treatment ◽

Cut Elimination ◽

Sequent Calculi ◽

Special Cases ◽

Necessary And Sufficient ◽

Different Parts ◽

Sequence Rules

Many important results in proof theory for sequent calculus (cut-elimination, completeness and other properties of search strategies, etc) are proved using permutations of sequent rules. The focus of this paper is on the development of systematic and automated-oriented techniques for the analysis of permutability in some sequent calculi. A representation of sequent calculi rules is discussed, which involves greater precision than previous approaches, and allows for correspondingly more precise and more general treatment of permutations. We define necessary and sufficient conditions for the permutation of sequence rules. These conditions are specified as constraints between the multisets that constitute different parts of the sequent rules. The authors extend their previous work in this direction to include some special cases of permutations.

Download Full-text

A representation of proper BC domains based on conjunctive sequent calculi

Mathematical Structures in Computer Science ◽

10.1017/s096012951900015x ◽

2019 ◽

Vol 30 (1) ◽

pp. 1-13 ◽

Cited By ~ 3

Author(s):

Longchun Wang ◽

Qingguo Li

Keyword(s):

Proof Theory ◽

Sequent Calculus ◽

Continuous Functions ◽

Logical System ◽

Consequence Relations ◽

Sequent Calculi ◽

Syntactic Form ◽

Scott Continuous ◽

Continuous Domain

AbstractWe build a logical system named a conjunctive sequent calculus which is a conjunctive fragment of the classical propositional sequent calculus in the sense of proof theory. We prove that a special class of formulae of a consistent conjunctive sequent calculus forms a bounded complete continuous domain without greatest element (for short, a proper BC domain), and each proper BC domain can be obtained in this way. More generally, we present conjunctive consequence relations as morphisms between consistent conjunctive sequent calculi and build a category which is equivalent to that of proper BC domains with Scott-continuous functions. A logical characterization of purely syntactic form for proper BC domains is obtained.

Download Full-text