About cut elimination for logics of common knowledge (Q1772772): Difference between revisions

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.