Published online by Cambridge University Press: 22 April 2015
For each Turing machine ${\cal T}$, we construct an algebra $\mathbb{A}$′$\left( {\cal T} \right)$ such that the variety generated by $\mathbb{A}$′$\left( {\cal T} \right)$ has definable principal subcongruences if and only if ${\cal T}$ halts, thus proving that the property of having definable principal subcongruences is undecidable for a finite algebra. A consequence of this is that there is no algorithm that takes as input a finite algebra and decides whether that algebra is finitely based.