Undecidability of Brouwerian semilattices (Q1821098)

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)].