Reduced sub-powers and the decision problem for finite algebras in arithmetical varieties

The aim of this paper is to prove that every finitely generated, arithmetical variety of finite type, in which every subdirectly irreducible algebra has linearly ordered congruences has a decidable first order theory of its finite members. The proof is based on a representation of finite algebras from such varieties by some quotients of special subdirect products in which sets of indices are partially ordered into dual trees. Then the result of M. O. Rabin about decidability of the monadic second order theory of two successors is applied.Presented by Stanley Burris.