Neat Reducts and Neat Embeddings in Cylindric Algebras

Abstract

An important central concept introduced in [Hen-Mon-Tar,85] is that of neat reducts, and the related one of neat embeddings. The notion of neat reducts is due to Leon Henkin, and one can find that the discussion of this notion is comprehensive and detailed in [Hen-Mon-Tar,85] (closer to the end of the book). This notion proved useful in at least two respects. Analyzing the number of variables appearing in proofs of first order formulas [Hir-Hod,02c], and characterizing the class of representable algebras; those algebras that are isomorphic to genuine algebras of relations. In fact, several open problems that appeared in [Hen-Mon-Tar,85] are on neat reducts, some of which appeared in part 1, and (not yet resolved) appeared again in part 2. This paper, among other things, surveys the status of these problems 40 years after they first appeared. Long proofs are omitted, except for one, which gives the gist of techniques used to solve such kind of problems.