Cylindric Algebras

Origin. Tarski with Henkin and Monk developed cylindric algebras (1950s-70s). Algebraic approach to first-order logic. Cylindrifications model existential quantification. Diagonal elements model equality. Part of algebraic logic tradition alongside relation algebras.

Models. Quantifiers as algebraic operations. Boolean algebra: propositional logic algebraically. Cylindric algebra: add operations for quantifiers and equality. Cylindrification cₖ captures ∃xₖ. Diagonal dₖₗ captures xₖ = xₗ. Alpha dimension captures number of variables.

Formalism.

Cylindric algebra of dimension α: (A, +, ·, -, 0, 1, cₖ, dₖₗ)ₖ,ₗ<α where:

(A, +, ·, -, 0, 1) is Boolean algebra
cₖ: A → A (cylindrification for variable k)
dₖₗ ∈ A (diagonal element for k = l)

Axioms: (C1) cₖ0 = 0 (C2) x ≤ cₖx (C3) cₖ(x · cₖy) = cₖx · cₖy (C4) cₖcₗx = cₗcₖx (C5) dₖₖ = 1 (C6) if k ≠ l,m then dₗₘ = cₖ(dₖₗ · dₖₘ) (C7) if k ≠ l then cₖ(dₖₗ · x) · cₖ(dₖₗ · -x) = 0

Interpretation:

cₖx corresponds to ∃xₖ.φ
dₖₗ corresponds to xₖ = xₗ
Substitution s(k,l)x = cₖ(dₖₗ · x)

Representable cylindric algebras: Concrete: subalgebras of (P(αU), ...) for some set U. Abstract cylindric algebras may not be representable.

Locally finite dimensional: Only finitely many variables "active" in each element. Models finitary first-order logic.

Symbols.

Symbol	Unicode	Name	Meaning
·	U+00B7	Middle dot	Boolean meet, conjunction
α	U+03B1	Alpha	Dimension: the supply of variables
ω	U+03C9	Omega	First infinite dimension, the one that models full FOL
∃	U+2203	Existential quantifier	What cₖ algebraizes
∈	U+2208	Element of	Membership, as in dₖₗ ∈ A
≠	U+2260	Not equal to	Side condition on the diagonal axioms
≤	U+2264	Less than or equal	Boolean order, x ≤ cₖx
⊆	U+2286	Subset	Class inclusion, as in Lf_ω ⊆ RCA_ω
⊊	U+228A	Proper inclusion	RCA_α ⊊ CA_α for α ≥ 3
cₖ	—	Cylindrification	Existential quantifier over variable k
dₖₗ	—	Diagonal	Equality xₖ = xₗ
+	—	Join	Disjunction
-	—	Complement	Negation
0, 1	—	Bottom and top	Contradiction and validity
s(k,l)	—	Substitution	Replace variable l by k
CA_α	—	Cylindric algebras	The variety axiomatized by (C1)–(C7)
RCA_α	—	Representable cylindric algebras	Those embeddable in a set algebra
Lf_α	—	Locally finite dimensional	Each element moved by finitely many cₖ
P(αU)	—	Full set algebra	Power set of the α-ary sequences over U

Metatheory. CA_α is by construction a variety, and Tarski proved that RCA_α is one too — closed under subalgebras, products, and homomorphic images — which is why the representation problem is an equational question rather than a structural one. The two classes coincide for α ≤ 2 and separate from dimension 3 upward: RCA_α ⊊ CA_α for α ≥ 3, so the axioms (C1)–(C7) are incomplete for set-algebra semantics. Henkin's completeness theorem appears here as the statement Lf_ω ⊆ RCA_ω: every locally finite dimensional cylindric algebra of infinite dimension is representable, which is the algebraic form of "every consistent first-order theory has a model". Monk (JSL, 1969) proved RCA_α is not finitely axiomatizable for 3 ≤ α < ω, and Andréka (APAL, 1997) strengthened this to show no axiomatization using finitely many variables exists. Hodkinson (1997) showed RCA_α is not atom-canonical for α ≥ 3, ruling out Sahlqvist-style axiomatizations. The equational theory of RCA_α is undecidable for α ≥ 3, matching the undecidability of the three-variable fragment of first-order logic.

Applies to. Algebraic foundations of logic. Database theory (cylindric algebra of relations). Model theory (algebraic methods). Storage and retrieval. Algebraic specification. Relation to dynamic algebra.

Limitations. The axioms do not capture the intended semantics: from dimension 3 on there are cylindric algebras satisfying (C1)–(C7) that embed in no set algebra, and the gap cannot be closed easily — RCA_α is not finitely axiomatizable, admits no axiomatization in finitely many variables (Andréka), and is not atom-canonical (Hodkinson), so every equational base for it is infinite and irredundant in a strong sense. Deciding membership is worse: the equational theory of RCA_α for α ≥ 3 is undecidable, so representability cannot be checked mechanically. Full first-order logic needs dimension ω together with local finiteness; dropping either condition loses the correspondence, and locally finite algebras of infinite dimension are the only ones for which representability is automatic. The dimension is fixed in the signature, so a cylindric algebra encodes a language with a fixed variable supply and there is no uniform algebra covering all of them at once.