Cylindric algebra

The notion of cylindric algebra, invented by Alfred Tarski, arises naturally in the algebraization of first-order logic with equality. This is comparable to the role Boolean algebras play for propositional logic. Indeed, cylindric algebras are Boolean algebras equipped with additional cylindrification operations that model quantification and equality. They differ from polyadic algebras in that the latter do not model equality.
Definition of a cylindric algebra.
A cylindric algebra of dimension formula_1 (where formula_1 is any ordinal number) is an algebraic structure formula_3 such that formula_4 is a Boolean algebra, formula_5 a unary operator on formula_6 for every formula_7 (called a "cylindrification"), and formula_8 a distinguished element of formula_6 for every formula_7 and formula_11 (called a "diagonal"), such that the following hold:
Assuming a presentation of first-order logic without function symbols, 
the operator formula_21 models existential quantification over variable formula_7 in formula formula_23 while the operator formula_8 models the equality of variables formula_7 and formula_11. Henceforth, reformulated using standard logical notations, the axioms read as
Cylindric set algebras.
A cylindric set algebra of dimension formula_1 is an algebraic structure formula_40 such that formula_41 is a field of sets, formula_42 is given by formula_43, and formula_8 is given by formula_45. It necessarily validates the axioms C1–C7 of a cylindric algebra, with formula_46 instead of formula_47, formula_48 instead of formula_49, set complement for complement, empty set as 0, formula_50 as the unit, and formula_51 instead of formula_52. The set "X" is called the "base".
Not every cylindric algebra has a representation as a cylindric set algebra. It is easier to connect the semantics of first-order predicate logic with cylindric set algebra. (For more details, see the "Further reading" section.)
Generalizations.
Cylindric algebras have been generalized to the case of many-sorted logic (Caleiro and Gonçalves 2006), which allows for a better modeling of the duality between first-order formulas and terms.
Relation to monadic Boolean algebra.
When formula_53 and formula_54 are restricted to being only 0, then formula_5 becomes formula_56, the diagonals can be dropped out, and the following theorem of cylindric algebra (Pinter 1973):
turns into the axiom
of monadic Boolean algebra. The axiom (C4) drops out. Thus monadic Boolean algebra can be seen as a restriction of cylindric algebra to the one variable case.