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.