Syntactic cut-elimination for common knowledge

DOI10.1016/J.APAL.2009.01.014MaRDI QIDQ1024553zbMATH OpenOpenAlexFDO

Authors Kai Brünnler, Thomas Studer

Publication date 17 June 2009

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2009.01.014

zbMATH Keywords

cut eliminationinfinitary sequent systemlogic of common belieflogic of common kowledgenested sequentsproof-depthVeblen function

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42) Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Review text

The logic of common knowledge has been formulated by Alberucci and Jäger in a sequential system with a rule of infinite premises so as to enjoy completeness, from which then follows the cut-elimination theorem indirectly. There are also several variations of the logic formulated in cut-free sequential systems but a syntactical cut-elimination proof has not been shown for any of them. In this paper, the authors formulate the logic in a system on nested sequents (i.e., trees of sequents), featuring inference rules to apply inside of such trees like a Schütte-type formulation, and show that the system allows a straightforward syntactical cut-elimination procedure establishing at the same time a non-trivial bound on the proof-depth charaterized by the Veblen function. The co-embeddability between the system and that of Alberucci and Jäger is also proved, which therefore gives rise to a syntactical proof of cut-elimination for the system of Alberucci and Jäger as well as a non-trivial bound of the proof-depth characterized similarly. It is also noted that the method works for many variations of the logic.

Recommendations

• Syntactic cut-elimination for common knowledge
• Cut-free common knowledge
• Deep sequent systems for modal logic
• Common knowledge: a finitary calculus with a syntactic cut-elimination procedure
• The proof theory of common knowledge

Cites work

• A system of interaction and structure
• A systematic proof theory for several modal logics
• About cut elimination for logics of common knowledge
• Cut-free common knowledge
• Cut-free sequent calculi for some tense logics
• Deduction chains for common knowledge
• Deep sequent systems for modal logic
• scientific article; zbMATH DE number 4210108 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (Why is no real title available?)
• scientific article; zbMATH DE number 1215496 (Why is no real title available?)
• scientific article; zbMATH DE number 2068679 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 824735 (Why is no real title available?)
• Justified and Common Knowledge: Limited Conservativity
• Justified common knowledge
• Knowledge and common knowledge in a distributed environment
• One-Pass Tableaux for Computation Tree Logic
• Proof theory. An introduction
• Schlussweisen-Kalküle der Prädikatenlogik
• Syntactic cut-elimination for common knowledge

Cited in

(13)

• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• On the proof theory of infinitary modal logic
• Cut-free common knowledge
• Justifications for common knowledge
• Common knowledge: a finitary calculus with a syntactic cut-elimination procedure
• The proof theory of common knowledge
• scientific article; zbMATH DE number 2068679 (Why is no real title available?)
• Effective cut-elimination for a fragment of modal mu-calculus
• Syntactic cut-elimination for common knowledge
• Pairing traditional and generic common knowledge
• Nested sequents or tree-hypersequents -- a survey
• Syntactic cut-elimination for a fragment of the modal mu-calculus
• Common knowledge does not have the Beth property

This page was built for publication: Syntactic cut-elimination for common knowledge

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1024553)