Undecidability of Brouwerian semilattices
The author shows that the first order theory of finite Brouwerian semilattices of the variety generated by the algebra \(2^ 2\oplus 1\) is undecidable. She proves the theorem by interpreting finite graphs into finite Brouwerian semilattices from the variety. The result gives an example of a finitely generated arithmetical variety whose finite members have an undecidable first order theory. This answers in negative a question of \textit{S. Burris} and \textit{H. P. Sankappanavar} [A course of universal algebra (1981; Zbl 0478.08001)].
scientific article; zbMATH DE number 3997773