THE UNDECIDABILITY OF THE DEFINABILITY OF PRINCIPAL SUBCONGRUENCES
MATTHEW MOORE · Journal of Symbolic Logic · 2015
Abstract 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.