Proof by example

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 $\alpha$ (where $\alpha$ is any ordinal number) is an algebraic structure $(A,+,\cdot ,-,0,1,c_{\kappa },d_{\kappa \lambda }{)}_{\kappa ,\lambda <\alpha }$ such that $(A,+,\cdot ,-,0,1)$ is a Boolean algebra, $c_{\kappa }$ a unary operator on $A$ for every $\kappa$, and $d_{\kappa \lambda }$ a distinguished element of $A$ for every $\kappa$ and $\lambda$, such that the following hold:

(C1) $c_{\kappa }0=0$

(C2) $x\le c_{\kappa }x$

(C3) $c_{\kappa }(x\cdot c_{\kappa }y)=c_{\kappa }x\cdot c_{\kappa }y$

(C4) $c_{\kappa }{c}_{\lambda }x=c_{\lambda }{c}_{\kappa }x$

(C5) $d_{\kappa \kappa }=1$

(C6) If $\kappa \ne \lambda \mu$,Template:Clarify then $d_{\lambda \mu }=c_{\kappa }(d_{\lambda \kappa }\cdot d_{\kappa \mu })$

(C7) If $\kappa \ne \lambda$, then $c_{\kappa }(d_{\kappa \lambda }\cdot x)\cdot c_{\kappa }(d_{\kappa \lambda }\cdot -x)=0$

Assuming a presentation of first-order logic without function symbols, the operator $c_{\kappa }x$ models existential quantification over variable $\kappa$ in formula $x$ while the operator $d_{\kappa \lambda }$ models the equality of variables $\kappa$ and $\lambda$. Henceforth, reformulated using standard logical notations, the axioms read as

(C1) $\mathrm{\exists }\kappa .𝑓𝑎𝑙𝑠𝑒\iff 𝑓𝑎𝑙𝑠𝑒$

(C2) $x\Rightarrow \mathrm{\exists }\kappa .x$

(C3) $\mathrm{\exists }\kappa .(x\wedge \mathrm{\exists }\kappa .y)\iff (\mathrm{\exists }\kappa .x)\wedge (\mathrm{\exists }\kappa .y)$

(C4) $\mathrm{\exists }\kappa \mathrm{\exists }\lambda .x\iff \mathrm{\exists }\lambda \mathrm{\exists }\kappa .x$

(C5) $\kappa =\kappa \iff 𝑡𝑟𝑢𝑒$

(C6) If $\kappa$ is a variable different from both $\lambda$ and $\mu$, Template:Clarify then $\lambda =\mu \iff \mathrm{\exists }\kappa .(\lambda =\kappa \wedge \kappa =\mu )$

(C7) If $\kappa$ and $\lambda$ are different variables, then $\mathrm{\exists }\kappa .(\kappa =\lambda \wedge x)\wedge \mathrm{\exists }\kappa .(\kappa =\lambda \wedge \mathrm{\neg }x)\iff 𝑓𝑎𝑙𝑠𝑒$

Generalizations

Recently, cylindric algebras have been generalized to the many-sorted case, which allows for a better modeling of the duality between first-order formulas and terms.

See also

• Abstract algebraic logic
• Lambda calculus and Combinatory logic, other approaches to modelling quantification and eliminating variables
• Hyperdoctrines are a categorical formulation of cylindric algebras
• Relation algebras (RA)
• Polyadic algebra

References

• Leon Henkin, Monk, J.D., and Alfred Tarski (1971) Cylindric Algebras, Part I. North-Holland. ISBN 978-0-7204-2043-2.
• -------- (1985) Cylindric Algebras, Part II. North-Holland.
• 20 year-old Real Estate Agent Rusty from Saint-Paul, has hobbies and interests which includes monopoly, property developers in singapore and poker. Will soon undertake a contiki trip that may include going to the Lower Valley of the Omo.
  
  My blog: http://www.primaboinca.com/view_profile.php?userid=5889534

Further reading

• Template:Cite doi