About cut elimination for logics of common knowledge

DOI10.1016/J.APAL.2004.10.004MaRDI QIDQ1772772zbMATH OpenOpenAlexFDO

Authors Luca Alberucci, Gerhard Jäger

Publication date 21 April 2005

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.2004.10.004

zbMATH Keywords

cut eliminationKripke modelslogic of common knowledge

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

Propositional logic of common knowledge has monadic connectives \(K_1,...,K_n\) for knowing agents and \(C\) for common knowledge. \(E(\alpha)\) means \(K_1(\alpha)\&...\& K_n(\alpha)\), and \(C(\alpha)\) is interpreted as the conjunction of all \(E^m(\alpha)\). The results are presented in detail for the case when the modal logic of \(K_i\) is K, but admit extension to other popular logics. The Hilbert-style calculus \(K_n(C)\) has the standard modal axioms and inference rules for \(K_i\) plus the additional axiom \(C(\alpha) \rightarrow (E(\alpha)\&E(C(\alpha)))\) and the induction rule: from \(\beta\rightarrow E(\alpha\& E(\beta))\) infer \(\beta\to E(\alpha)\). Kripke models are defined in a standard way with \(n\) binary accessibility relations, one for every \(K_i\). A partial cut-elimination theorem is obtained via the finite model property: a canonical Kripke model is constructed from sequents with components in the Fisher-Ladner closure. Cut is needed only for the Boolean combinations of the formulas in this closure. To get complete cut elimination (by a non-effective proof) a semi-formal system with the \(\omega\)-rule for \(C\) is considered: \(C(\alpha),\Gamma\) is derived from \(E^m(\alpha),\Gamma\) for all \(m\). The subformula property for the resulting system implies that valid formulas without positive occurrences of \(C\) have finite derivations, and valid formulas without negative occurrences of \(C\) have derivations of finite height bounded by the K-depth of the given formula. This prompts the following restriction of the \(\omega\) rule for positive formulas: \(C(\alpha),\Gamma\) is derived from \(E^m(\alpha),\Gamma\) for all \(m\) from 1 to the \(\text{K-depth}+1\). This rule is admissible, but not derivable.

Recommendations

• Cut-elimination for knowledge logics with interaction
• Common knowledge: a finitary calculus with a syntactic cut-elimination procedure
• Cut elimination and complexity bounds for intuitionistic epistemic logic
• Cut elimination and realization for epistemic logics with justification
• A note on cut-elimination for classical propositional logic
• Bounds for cut elimination in intuitionistic propositional logic
• scientific article; zbMATH DE number 48659
• A cut-elimination proof in intuitionistic predicate logic
• Cut elimination for shallow modal logics
• Cut elimination in coalgebraic logics

Cites work

• About cut elimination for logics of common knowledge
• Common knowledge logic and game logic
• Common knowledge: Relating anti-founded situation semantics to modal logic neighbourhood semantics
• Game logic and its applications. II
• scientific article; zbMATH DE number 42737 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (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?)
• Knowledge and common knowledge in a distributed environment
• Propositional dynamic logic of regular programs
• Strictness of the Modal μ-Calculus Hierarchy
• Three views of common knowledge

Cited in

(28)

• Syntactic cut-elimination for common knowledge
• Refined common knowledge logics or logics of common information
• About cut elimination for logics of common knowledge
• Craig interpolation of epistemic logics with distributed knowledge
• Cut-free common knowledge
• Justified common knowledge
• Deduction chains for common knowledge
• Mechanizing common knowledge logic using COQ
• A specialization of definitions in common knowledge logic
• Cut-elimination for knowledge logics with interaction
• Justifications for common knowledge
• Common knowledge: a finitary calculus with a syntactic cut-elimination procedure
• Two ways to common knowledge
• The proof theory of common knowledge
• Intuitionistic common knowledge or belief
• Explicit generic common knowledge
• One-Pass Tableaux for Computation Tree Logic
• An on-the-fly tableau-based decision procedure for PDL-satisfiability
• Syntactic cut-elimination for common knowledge
• Frame definability, canonicity and cut elimination in common sense modal predicate logics
• scientific article; zbMATH DE number 7117799 (Why is no real title available?)
• Pairing traditional and generic common knowledge
• Gentzen-type sequent calculus for modal logic S5
• Nested sequents or tree-hypersequents -- a survey
• A logical framework for convention
• Canonical completeness of infinitary \(\mu \)
• A contraction-free and cut-free sequent calculus for propositional dynamic logic
• Common knowledge does not have the Beth property

This page was built for publication: About cut elimination for logics of common knowledge

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