The Undecidability of the Definability of Principal Subcongruences
arXiv:1301.5588 · doi:10.1017/jsl.2014.51
Abstract
For each Turing machine T, we construct an algebra A'(T) such that the variety generated by A'(T) has definable principal subcongruences if and only if 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 a decides whether that algebra is finitely based.