Cut-free common knowledge (Q2475436)

The following general schema is applied to the logic of knowledge. Let two connectives \(C,E\) in some propositional logic satisfy \(C\alpha=\&_m E^m\alpha.\) Then it is natural to postulate an infinitary inference rule \[ (\omega C)\;\text{From \(E^m\alpha,\Gamma\) for all \(m\) infer \(C\alpha,\Gamma\).} \] It isoften relatively easy to get completeness and cut elimination for such formulation. Suppose one also has the finite model property: if \(\alpha\) is satisfiable, then it is satisfiable in a model of size say \(2^{l(\alpha)}\). Then a finitary restriction of the rule \((\omega C)\) that is complete is also cut-free complete: \[ (\omega C)\;\text{From \(E^m\alpha,\Gamma\) for all \(m\leq \text{bd}(\alpha,\Gamma)\) infer \(C\alpha,\Gamma\),} \] where \(\text{bd}(\alpha,\Gamma)= 2^{l(C\alpha)}+2^{\gamma_1}+\ldots+ 2^{\gamma_n}\) for \(\Gamma=\{\gamma_1,\ldots,\gamma_n\}\). In the present paper \(C\) is common knowledge, \(E\) is joint knowledge. Open question mentioned at the end: find syntactic cut elimination procedures for the systems considered.