Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom (Q1042695)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom |
scientific article |
Statements
Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom (English)
0 references
15 December 2009
0 references
Multimodal logic S4\(_n\) has \(n\) modalities \(K_c\) (for the central agent), \(K_1,\ldots,K_{n-1}\), with S4-axioms for each of the modalities plus interaction axioms : \(K_c\rightarrow K_i\) for all \(i\). The corresponding Gentzen-type system admitting cut elimination has the familiar S4-rules plus the interaction rule: from \(K\Gamma\rightarrow A\) infer \(K\Gamma,\Gamma_1\rightarrow \Delta,K_cA\), where \(K\Gamma\) consists of formulas of the form \(K_iB\).
0 references
modal logic
0 references
logic of knowledge
0 references
central agent
0 references
interaction axiom
0 references
cut elimination
0 references