In mathematics, the notion of cylindric algebra, developed 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. 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.
A cylindric algebra of dimension
\alpha
\alpha
(A,+, ⋅ ,-,0,1,c\kappa,d\kappaλ)\kappa,λ<\alpha
(A,+, ⋅ ,-,0,1)
c\kappa
A
\kappa
d\kappaλ
A
\kappa
λ
(C1)
c\kappa0=0
(C2)
x\leqc\kappax
(C3)
c\kappa(x ⋅ c\kappay)=c\kappax ⋅ c\kappay
(C4)
c\kappacλx=cλc\kappax
(C5)
d\kappa\kappa=1
(C6) If
\kappa\notin\{λ,\mu\}
dλ\mu=c\kappa(dλ\kappa ⋅ d\kappa\mu)
(C7) If
\kappa ≠ λ
c\kappa(d\kappaλ ⋅ x) ⋅ c\kappa(d\kappaλ ⋅ -x)=0
Assuming a presentation of first-order logic without function symbols, the operator
c\kappax
\kappa
x
d\kappaλ
\kappa
λ
(C1)
\exists\kappa.false\ifffalse
(C2)
x\implies\exists\kappa.x
(C3)
\exists\kappa.(x\wedge\exists\kappa.y)\iff(\exists\kappa.x)\wedge(\exists\kappa.y)
(C4)
\exists\kappa\existsλ.x\iff\existsλ\exists\kappa.x
(C5)
\kappa=\kappa\ifftrue
(C6) If
\kappa
λ
\mu
λ=\mu\iff\exists\kappa.(λ=\kappa\wedge\kappa=\mu)
(C7) If
\kappa
λ
\exists\kappa.(\kappa=λ\wedgex)\wedge\exists\kappa.(\kappa=λ\wedge\negx)\ifffalse
A cylindric set algebra of dimension
\alpha
(A,\cup,\cap,-,\empty,X\alpha,c\kappa,d\kappaλ)\kappa,λ<\alpha
\langleX\alpha,A\rangle
c\kappaS
\{y\inX\alpha\mid\existsx\inS \forall\beta ≠ \kappa y(\beta)=x(\beta)\}
d\kappaλ
\{x\inX\alpha\midx(\kappa)=x(λ)\}
\cup
+
\cap
⋅
X\alpha
\subseteq
\le
A representation of a cylindric algebra is an isomorphism from that algebra to a cylindric set algebra. Not every cylindric algebra has a representation as a cylindric set algebra.[2] It is easier to connect the semantics of first-order predicate logic with cylindric set algebra. (For more details, see .)
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.
When
\alpha=1
\kappa,λ
c\kappa
\exists
c\kappa(x+y)=c\kappax+c\kappay
\exists(x+y)=\existsx+\existsy