Undecidability of relatively free Hilbert algebras (Q1103604)

Let H stand for the variety of Hilbert algebras and I for its subvariety of implication algebras. In this paper the author interprets (by a method presented by \textit{S. Burris} and \textit{R. McKenzie} [Mem. Am. Math. Soc. 246 (1981; Zbl 0483.03019)]) the class of finite partition lattices, known to have hereditarily undecidable first order theory, into a particular class of implication algebras. This class is a subclass both of the class FI of finitely generated free implication algebras and of the class of the finite members of every non-trivial variety of Hilbert algebras. Thus he proves that the above classes have hereditarily undecidable first-order theories. Also he shows that FI can be interpreted into the class FV of the finitely generated free members of every non-trivial variety of Hilbert algebras; so he derives that the first-order theories of FV's are hereditarily undecidable.