Definable principal congruences in congruence distributive varieties (Q759785)

The paper presents an algorithm that, given a finite algebra A generating a congruence distributive variety, determines whether this variety has first order definable principal congruences (DPC). In fact, DPC turns out to be equivalent to the extendability of the principal congruences of certain subalgebras of the algebras in \(HS(A^ 3)\). To verify this algorithm, combinatorial properties of the finite subdirect powers of A are investigated. As an application, R. McKenzie's result that there are no non-distributive lattice varieties with DPC is obtained.