All normal extensions of S5-squared are finitely axiomatizable (Q1770622)

The modal logic \(\mathbf{S5^2}\) is an extension of \(\mathbf{S5}\) which includes two commuting different modal operators both satisfying the axioms for \(\mathbf{S5}\). The logic \(\mathbf{S5^2}\) is known to have the exponential size model property and its satisfiability problem to be NEXPTIME-complete. In contrast, every proper normal extension is known to have the poly-size model property. In Stud. Log. 73, No. 3, 367--382 (2003; Zbl 1027.03015), \textit{N. Bezhanishvili} and \textit{M. Marx} conjectured that every proper modal extension of \(\mathbf{S5^2}\) is finitely axiomatizable and NP-complete; in this paper the conjecture is proved. The authors show that for every proper normal extension \(L\) of \(\mathbf{S5^2}\), there is a finite set \(M_L\) of finite \(\mathbf{S5^2}\)-frames such that an arbitrary finite \(\mathbf{S5^2}\)-frame is a frame for \(L\) iff it does not have any frame in \(M_L\) as a \(p\)-morphic image, and this yields a finite axiomatization of \(L\). The condition is also proved to be decidable in deterministic polynomial time; this together with the poly-size model property implies NP-completeness. It is worth to remark that the complexity results presented take the same line of research as the one about unimodal logics pursued by \textit{M. Kracht} [Math. Log. Q. 39, No. 3, 301--322 (1993; Zbl 0799.03011)]; however, the theory of well-quasi-orderings is not sufficient and better-quasi-orderings have been used instead.