Search

This paper is a continuation of [3]. Congruence permutability is shown to be a necessary condition for a locally finite congruence distributive variety to have a decidable first order theory of its finite algebras. This is a positive answer to Problem 6 of S. Burns and H. P. Sankappanavar [2]. Moreover this allows us to give a full characterization of finitely generated congruence distributive varieties of finite type with decidable first order theories of their finite members.

The aim of this paper is to prove that every congruence distributive variety containing a finite subdirectly irreducible algebra whose congruences are not linearly ordered has an undecidable first order theory of its finite members. This fills a gap which kept us from the full characterization of the finitely generated, arithmetical varieties (of finite type) having a decidable first order theory of their finite members. Progress on finding this characterization was made in the papers [14] and [15].