Tarski’s Finite Basis Problem Is Undecidable

We exhibit a construction which produces for every Turing machine Formula: see text, an algebra Formula: see text (finite and of finite type) such that the Turing machine halts iff the algebra has a finite basis for its equations.