Algebraic semantics and model completeness for intuitionistic public announcement logic (Q393906)

The paper is based on the logic of public announcements (PAL), a propositional modal logic with formulas of the form \(\langle\psi\rangle\phi\) and \([\psi]\phi\) where \(\psi\) denotes an announcement which possibly changes the epistemic states of agents. The muddy children puzzle is provided for illustration purposes: \(k\) of \(n\) children have got mud on their foreheads and each child can only see the others' foreheads. After their father has said ``at least one of you is dirty'' and repeatedly asked them ``do you know whether your own forehead is dirty?'', all children, being truthful, answer ``no'' the first \(k-1\) times, and ``yes'' the \(k\)-th time. This can be formalised over the vocabulary \(\{D_i, C_i\mid 1\leq i\leq n\}\), the intended interpretations of \(D_i\) and \(C_i\) being ``child \(i\) is dirty'' and ``child \(i\) is clean'', respectively, in such a way that this line of reasoning corresponds to deriving the formula \( [\mathrm{father}][\mathrm{no}]^{k-1}\square_j D_j \) from the axiom scheme \(\square_i p\rightarrow p\) and \(\{\mathrm{aut},\mathrm{dirty}(J),E_k(\mathrm{vision})\}\) where: {\parindent=6mm \begin{itemize} \item[--] \(\mathrm{father}\) is \(\bigvee_{i=1}^n D_i\) (father's initial statement), \item [--] \(\mathrm{no}\) is \(\bigwedge_{i=1}^n(\diamond_i D_i\wedge\diamond_i C_i)\) (children's answer for each of the first \(k-1\) rounds), \item [--] \(\mathrm{aut}\) is \(\bigvee_{i=1}^n(C_i\rightarrow\bot)\leftrightarrow D_i\bigr)\) (each child has either a clean or a dirty forehead), \item [--] \(\mathrm{dirty}(J)\) is \(\bigwedge\bigl\{(D_i\rightarrow\square_j D_i)\wedge(C_i\rightarrow\square_j C_i)\mid 1\leq i,j\leq n, i\neq j\bigr\}\) (each child knows for each other child where it is clean or dirty), and \item [--] \(\mathrm{vision}\) is \(\bigwedge_{j\in J}D_j\wedge_{\bigwedge j\notin J}D_j\) and \(J\) is a subset of \(\{1,\dots,n\}\) of cardinality \(k\), \end{itemize}} in an intuitionistic version of PAL (IPAL), for which a completeness result is provided. Axiomatically, IPAL 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}\) \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 IPAL holding for both, using concepts and techniques from coalgebraic logic and duality theory. The proof techniques characterize the key logical constructions of IPAL 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.