Cut-free common knowledge
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.
- A guide to completeness and complexity for modal logics of knowledge and belief
- About cut elimination for logics of common knowledge
- scientific article; zbMATH DE number 4154410 (Why is no real title available?)
- scientific article; zbMATH DE number 42737 (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?)
- On the proof theory of the modal mu-calculus
- Syntactic cut-elimination for common knowledge
- Deduction chains for common knowledge
- Two complete finitary sequent calculi for reflexive common knowledge
- 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
- One-Pass Tableaux for Computation Tree Logic
- scientific article; zbMATH DE number 2068679 (Why is no real title available?)
- An on-the-fly tableau-based decision procedure for PDL-satisfiability
- Syntactic cut-elimination for common knowledge
- Geometric Rules in Infinitary Logic
- Pairing traditional and generic common knowledge
- Model existence in non-compact modal logic
- Cut-free sequent systems for temporal logic
- 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: Cut-free common knowledge
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2475436)
