Epistemic updates on algebras (Q2871469)

The paper is based on a logic of epistemic actions and knowledge (EAK), a propositional modal logic with formulas of the form \(\langle\alpha\rangle\phi\) and \([\alpha]\phi\) where \(\alpha\) denotes an action, constrained by some preconditions before it can be applied and change the epistemic states of agents. A scenario is provided for illustration purposes: An agent \(a\) holds a green card and two agents \(b\) and \(c\) each hold a white card. It is common knowledge among the three of them that there are two white cards and one green one. Then \(a\) shows its card only to \(b\) (action \(\alpha\)), who announces in the presence of \(c\) that \(a\) knows what the actual distribution of cards is (action \(\beta\)), after what \(c\) knows what the actual distribution is. This can be formalised on the vocabulary \(\bigl\{G_i, W_i\mid i\in\{a,b,c\}\bigr\}\), in such a way that this line of reasoning corresponds to deriving the formula \( [\alpha][\beta]\square_cG_a \) (after actions \(\alpha\) and \(\beta\) have been performed, agent \(c\) knows knows that \(a\) holds the Green card) from {\parindent=6mm \begin{itemize} \item[--] \(\bigvee_{i\in\{a,b,c\}}(G_i\wedge\bigwedge_{j\in\{a,b,c\}\setminus\{i\}}W_j)\) (there are one green card and two white ones), \item [--] \(\bigwedge_{i\in\{a,b,c\}}\bigl((W_i\rightarrow\bot)\leftrightarrow G_i\bigr)\) (each agent holds either a white or a green card and not both), and \item [--] \(\bigwedge_{i\in\{a,b,c\}}\square_i\phi\) where \(\phi\) is the formula \(\bigwedge_{i\in\{a,b,c\}}\bigl(W_i\rightarrow\bigwedge_{j\in\{a,b,c\}\setminus\{i\}}\diamond_i G_j\bigr)\) (the three agents know that for each one of them \(i\), if \(i\) holds the white card then from \(i\)'s perspective, any of the other two agents may hold the green card) NEWLINENEWLINE\end{itemize}}NEWLINENEWLINEin an intuitionistic version of EAK (IEAK), for which a completeness result is provided. Axiomatically, IEAK is an extension of IK [\textit{G. Fischer Servi}, Rend. Semin. Mat., Torino 42, No. 3, 179--194 (1984; Zbl 0592.03011)], an intuitionistic analogue of the modal logic K, whose semantics is defined on the basis of models of the form \(M=((W, \leq, R),V)\) where \((W,\leq)\) is a nonempty poset, \(R\) is a binary equivalence relation such that \((R\circ\geq)\subseteq(\geq\circ R)\), \((\leq\circ R)\subseteq(R\circ\leq)\), and \(R=(\geq\circ R)\cap(R\circ\leq)\), and \(V\) is a valuation over \(W\), the key clauses for the interpretation \([[\phi]]_M\) of a formula \(\phi\) in \(M\) being: {\parindent=6mm \begin{itemize} \item[--] \([[\diamond\phi]]_M=R^{-1}\langle[[\phi]]_M\rangle\) \item [--] \([[\square\phi]]_M=\overline{(\geq\circ R)^{-1}\langle\overline{[[\phi]]_M}\rangle}\) NEWLINENEWLINE\end{itemize}} The crux of the paper is to generalise these models to a notion of IK-model and a notion of relational IK-model, the completeness result for IEAK holding for both, using concepts and techniques from coalgebraic logic and duality theory. The proof techniques characterize the key logical constructions of EAK in terms which are general enough to be applicable to many classes of algebras, including Boolean algebras with operators and modal expansions of Heyting algebras.