Non-finitely axiomatisable modal product logics with infinite canonical axiomatisations (Q2304538)

The paper is concerned with modal products of a modal logic with the finitely axiomatizable logic \(\mathbf{Diff} \subseteq \mathbf{S5}\), where \(\mathbf{Diff}\) is a logic introduced by Von Wright as the set of unimodal formulas that are valid in all difference frames, that is, in frames \((W, \neq_W )\), where \(\neq_W \) is the non-equality relation on some non-empty set \(W\). It is known that \(\mathbf{Diff}\) can be axiomatized by the Sahlqvist formulas. In particular, the following theorems have been proven. Theorem 1. For any Kripke complete logic \(L\) with \(\mathbf{K} \subseteq L \subseteq \mathbf{S5}\), \(L \times \mathbf{Diff}\) is not axiomatizable using finitely many propositional variables. Thus, \(\mathbf{Diff} \times \mathbf{Diff}\) is not finitely axiomatizable. Theorem 2. \(\mathbf{Diff} \times^{\mathrm{sq}} \mathbf{Diff}\) is not axiomatizable over \(\mathbf{Diff} \times \mathbf{Diff}\) using finitely many propositional variables. Theorem 3. \begin{itemize} \item[(i)] There is an infinite axiomatization for \(\mathbf{Diff} \times \mathbf{Diff}\) consisting of Sahlqvist formulas. \item[(ii)] The class of all frames for \(\mathbf{Diff} \times \mathbf{Diff}\) is elementary. \item[(iii)] For every countable rooted frame \(\mathfrak{F}\), \(\mathfrak{F}\) is a frame for \(\mathbf{Diff} \times \mathbf{Diff}\) iff \(\mathfrak{F}\) is a p-morphic image of some product of two difference frames. \end{itemize} Theorem 4. \begin{itemize} \item[(i)] \(\mathbf{Diff}\times^{\mathrm{sq}} \mathbf{Diff}\) can be axiomatized by adding infinitely many generalized Sahlqvist formulas to \(\mathbf{Diff}\times \mathbf{Diff}\). \item[(ii)] The class of all frames for \(\mathbf{Diff}\times^{\mathrm{sq}} \mathbf{Diff}\) is elementary. \item[(iii)] For every countable rooted frame \(\mathfrak{F}\), \(\mathfrak{F}\) is a frame for \(\mathbf{Diff}\times^{sq} \mathbf{Diff}\) iff \(\mathfrak{F}\) is a p-morphic image of some product of two difference frames of the same size. \end{itemize}