Cylindric algebra

Definition of a cylindric algebra

A cylindric algebra of dimension α (where α is any ordinal number) is an algebraic structure ( A , + , ⋅ , − , 0 , 1 , c κ , d κ λ ) κ , λ < α such that ( A , + , ⋅ , − , 0 , 1 ) is a Boolean algebra, c κ a unary operator on A for every κ , and d κ λ a distinguished element of A for every κ and λ , such that the following hold:

(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 κ ∉ { λ , μ } , then d λ μ = c κ ( d λ κ ⋅ d κ μ )

(C7) If κ ≠ λ , then c κ ( d κ λ ⋅ x ) ⋅ c κ ( d κ λ ⋅ − x ) = 0

Assuming a presentation of first-order logic without function symbols, the operator c κ x models existential quantification over variable κ in formula x while the operator d κ λ models the equality of variables κ and λ . Henceforth, reformulated using standard logical notations, the axioms read as

(C1) ∃ κ . f a l s e ⇔ f a l s e

(C2) x ⇒ ∃ κ . x

(C3) ∃ κ . ( x ∧ ∃ κ . y ) ⇔ ( ∃ κ . x ) ∧ ( ∃ κ . y )

(C4) ∃ κ ∃ λ . x ⇔ ∃ λ ∃ κ . x

(C5) κ = κ ⇔ t r u e

(C6) If κ is a variable different from both λ and μ , then λ = μ ⇔ ∃ κ . ( λ = κ ∧ κ = μ )

(C7) If κ and λ are different variables, then ∃ κ . ( κ = λ ∧ x ) ∧ ∃ κ . ( κ = λ ∧ ¬ x ) ⇔ f a l s e

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.