Abstract

The aim of this paper is to give a new proof for the decidability and finite model property of first-order logic with two variables (without function symbols), using a combinatorial theorem due to Herwig. The results are proved in the framework of polyadic equality set algebras of dimension two (Pse 2 ). The new proof also shows the known results that the universal theory of Pse 2 is decidable and that every finite Pse 2 can be represented on a finite base. Since the class Cs 2 of cylindric set algebras of dimension 2 forms a reduct of Pse 2 , these results extend to Cs 2 as well