Completeness results for memory logics (Q408552)

This paper studies memory logics, a particular kind of propositional modal logics where a relational structure \(\mathcal M=\langle D,(R_r)_{r\in\mathrm{Rel}},L\rangle\), with \(\mathrm{Rel}\) denoting a set of accessibility relations over the domain \(D\) and \(L\) an interpretation of all propositional symbols in the language at each member of \(D\), is extended with a set of nominal symbols meant to denote members of \(D\) and a memory \(S\), that is, a subset of \(D\) meant to represent the set of members of \(D\) which have been ``explored'' and ''remembered''. The modal operators considered include the classical operators \(\langle r\rangle\), \(r\in\mathrm{Rel}\), and some of the unary operators \({\mathtt r}\mkern-14mu\bigcirc\), \({\mathtt f}\mkern-14mu\bigcirc\), \({\mathtt e}\mkern-14mu\bigcirc\) and \({{\mathtt a}\mkern-14mu\bigcirc}_{i}\) for all nominals \(i\) and the nullary operator \({\mathtt k}\mkern-14mu\bigcirc\), with the following interpretation in \(\langle\mathcal M,S\rangle\) at \(w\in D\) with \(I\) extended to map the nominals to members of \(D\): {\parindent=5mm \begin{itemize}\item[1)] Given \(s\in\mathrm{Rel}\), \(\langle\mathcal M,S\rangle,w\models\langle s\rangle\varphi\) iff there exists \(w'\in D\) with \(R_s(w,w')\) and \(\langle\mathcal M,S\rangle,w'\models\varphi\). \item[2)] Given a nominal \(i\), \(\langle\mathcal M,S\rangle,w\models {{\mathtt a}\mkern-14mu\bigcirc}_{i}\varphi\) iff \(\langle\mathcal M,S\rangle,L(i)\models\varphi\). \item[3)] \(\langle\mathcal M,S\rangle,w\models {\mathtt r}\mkern-14mu\bigcirc\varphi\) iff \(\langle\mathcal M,S\cup\{w\}\rangle,w\models\varphi\). \item[4)] \(\langle\mathcal M,S\rangle,w\models{\mathtt k}\mkern-14mu\bigcirc\) iff \(w\in S\). \item[5)] \(\langle\mathcal M,S\rangle,w\models {\mathtt f}\mkern-14mu\bigcirc\varphi\) iff \(\langle\mathcal M,S\setminus\{w\}\rangle,w\models\varphi\). \item[6)] \(\langle\mathcal M,S\rangle,w\models {\mathtt e}\mkern-14mu\bigcirc\varphi\) iff \(\langle\mathcal M,\emptyset\rangle,w\models\varphi\). \end{itemize}} So \({\mathtt r}\mkern-14mu\bigcirc\) remembers the current state, \({\mathtt f}\mkern-14mu\bigcirc\) forgets the current state, \({\mathtt e}\mkern-14mu\bigcirc\) forgets (erases) all states, and \({\mathtt k}\mkern-14mu\bigcirc\) checks whether the current state has been remembered (is ``known''). For instance, the formula \({\mathtt e}\mkern-14mu\bigcirc\;{\mathtt r}\mkern-14mu\bigcirc\langle r\rangle\;{\mathtt k}\mkern-14mu\bigcirc\) expresses that \(R_{r}\) is reflexive (the memory is cleared, the current state is memorised and it is verified that \(r\) has a loop at this state), which demonstrates that the proposed language is more expressive than basic modal logic. The authors provide complete axiomatisations for some memory logics. The first result proves completeness of the memory logic with the extra modal operators \({\mathtt r}\mkern-14mu\bigcirc\), \({\mathtt k}\mkern-14mu\bigcirc\) and \({{\mathtt a}\mkern-14mu\bigcirc}_{i}\). A key axiom is \({{\mathtt a}\mkern-14mu\bigcirc}_{i}({\mathtt r}\mkern-14mu\bigcirc\varphi\leftrightarrow\varphi[{\mathtt k}\mkern-14mu\bigcirc/{\mathtt k}\mkern-14mu\bigcirc\vee i])\) which states that when being in a state named by \(i\), remembering that state is equivalent to increase the extension of \({\mathtt k}\mkern-14mu\bigcirc\) with \(i\) throughout the formula. The proof follows the classical proof of building a Henkin model using \textit{named} maximal consistent sets. Extensions of this result are provided for the logic where \(S\) is empty, and for the class of pure formulas which contain no proposition letters (hence whose atoms are only nominals and \({\mathtt k}\mkern-14mu\bigcirc\)). Then complete axiomatisations are given for (1) the memory logic with the extra modal operators \({\mathtt r}\mkern-14mu\bigcirc\), \({\mathtt e}\mkern-14mu\bigcirc\), \({\mathtt k}\mkern-14mu\bigcirc\) and \({{\mathtt a}\mkern-14mu\bigcirc}_{i}\), (2) the memory logic with the extra modal operators \({\mathtt r}\mkern-14mu\bigcirc\), \({\mathtt f}\mkern-14mu\bigcirc\), \({\mathtt k}\mkern-14mu\bigcirc\) and \({{\mathtt a}\mkern-14mu\bigcirc}_{i}\), and (3) the memory logic with the extra modal operators \({\mathtt r}\mkern-14mu\bigcirc\), \({\mathtt e}\mkern-14mu\bigcirc\), \({\mathtt f}\mkern-14mu\bigcirc\), \({\mathtt k}\mkern-14mu\bigcirc\) and \({{\mathtt a}\mkern-14mu\bigcirc}_{i}\). Finally, the semantics of the accessibility operators is changed to: Given \(s\in\mathrm{Rel}\), \(\langle\mathcal M,S\rangle,w\models\langle s\rangle\varphi\) iff there exists \(w'\in D\) with \(R_s(w,w')\) and \(\langle\mathcal M,S\cup\{w\}\rangle,w'\models\varphi\) to remember the state being left when moving to a successor state and a complete axiomatisation is given for the memory logic with the extra modal operators \({\mathtt r}\mkern-14mu\bigcirc\) and \({\mathtt k}\mkern-14mu\bigcirc\), hence a logic which avoids the use of nominals, and which turns out to have the tree model property.