The finite inseparability of the first-order theory of diagonalisable algebras (Q795036)

In this paper, the author proves the finite inseparability of the first order theory of diagonalizable algebras (shortly: DAs). DAs constitute the algebraic analogue of the modal logic of provability, and can be considered as an algebraic approach to the study of the provability predicate for Peano Arithmetic or related theories. Smoryński's proof uses a result of \textit{Yu. L. Ershov} and \textit{M. A. Taj'tslin}, who proved the finite inseparability of the theory of distributive lattices [Algebra Logika, Sem. 2, No.5, 37-41 (1963; Zbl 0192.056)]. The undecidability of the first order theory of diagonalizable algebras was proved by the reviewer by direct means [Stud. Logica 39, 355-359 (1980; Zbl 0463.03016)]. Of course, Smoryński's result is stronger (it implies the undecidability of the first order theory of finite DAs); however, it does not solve the problem of the decidability or undecidability of the Lindenbaum DA of Peano Arithmetic.