Ryo Murai

We develop intuitionistic public announcement logic over intuitionistic \({\textbf{K}}\), \({{\textbf{K}}}{{\textbf{T}}}\), \({{\textbf{K}}}{{\textbf{4}}}\), and \({{\textbf{S}}}{{\textbf{4}}}\) with distributed knowledge. We reveal that a recursion axiom for the distributed knowledge is _not_ valid for a frame class discussed in [ 12 ] but valid for the restricted frame class introduced in [ 20, 26 ]. The semantic completeness of the static logics for this restricted frame class is established via the concept of pseudo-model.

Artemov and Protopopescu introduced a Brouwer-Heyting-Kolmogorov interpretation of knowledge operator to define the intuitionistic epistemic logic IEL, where the axiom $$A\supset KA$$ is accepted but the axiom $$KA\supset A$$ is refused. This paper studies the notion of distributed knowledge on an expansion of the multi agent variant of IEL. We provide a BHK interpretation of distributed knowledge operator to define the intuitionistic epistemic logic with distributed knowledge DIEL. We construct Hilbert system and cut-free sequent calculus for $$\mathbf {DIEL}$$ and show that they are sound and complete for the intended Kripke semantics.