cylindric algebra

{{Short description|Algebraization of first-order logic with equality}}

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.

The cylindric algebra should not be confused with the measure theoretic concept cylindrical algebra that arises in the study of cylinder set measures and the cylindrical σ-algebra.

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 (called a cylindrification), and d_{\kappa\lambda} a distinguished element of A for every \kappa and \lambda (called a diagonal), such that the following hold:

: (C1) c_\kappa 0=0

: (C2) x\leq 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\notin\{\lambda,\mu\}, then d_{\lambda\mu}=c_\kappa(d_{\lambda\kappa}\cdot d_{\kappa\mu})

: (C7) If \kappa\neq\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. Hence, reformulated using standard logical notations, the axioms read as

: (C1) \exists \kappa. \mathit{false} \iff \mathit{false}

: (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\lambda. x \iff \exists \lambda \exists\kappa. x

: (C5) \kappa=\kappa \iff \mathit{true}

: (C6) If \kappa is a variable different from both \lambda and \mu, then \lambda=\mu \iff \exists\kappa. (\lambda=\kappa \wedge \kappa=\mu)

: (C7) If \kappa and \lambda are different variables, then \exists\kappa. (\kappa=\lambda \wedge x) \wedge \exists\kappa. (\kappa=\lambda\wedge \neg x) \iff \mathit{false}

Cylindric set algebras

A cylindric set algebra of dimension \alpha is an algebraic structure (A, \cup, \cap, -, \empty, X^\alpha, c_\kappa,d_{\kappa\lambda})_{\kappa,\lambda<\alpha} such that \langle X^\alpha, A \rangle is a field of sets, c_\kappa S is given by \{y \in X^\alpha \mid \exists x \in S\ \forall \beta \neq \kappa\ y(\beta) = x(\beta)\}, and d_{\kappa\lambda} is given by \{x \in X^\alpha \mid x(\kappa) = x(\lambda)\}.Hirsch and Hodkinson p167, Definition 5.16 It necessarily validates the axioms C1–C7 of a cylindric algebra, with \cup instead of +, \cap instead of \cdot, set complement for complement, empty set as 0, X^\alpha as the unit, and \subseteq instead of \le. The set X is called the base.

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.Hirsch and Hodkinson p168{{example needed|date=December 2019}} It is easier to connect the semantics of first-order predicate logic with cylindric set algebra. (For more details, see {{sectionlink||Further reading}}.)

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 \alpha = 1 and \kappa, \lambda are restricted to being only 0, then c_\kappa becomes \exists, the diagonals can be dropped out, and the following theorem of cylindric algebra (Pinter 1973):

: c_\kappa (x + y) = c_\kappa x + c_\kappa y

turns into the axiom

: \exists (x + y) = \exists x + \exists y

of monadic Boolean algebra. The axiom (C4) drops out (becomes a tautology). Thus monadic Boolean algebra can be seen as a restriction of cylindric algebra to the one variable case.

See also

Notes

{{reflist}}

References

  • {{Cite journal | author = Charles Pinter | title = A Simple Algebra of First Order Logic | journal = Notre Dame Journal of Formal Logic | volume = XIV | pages = 361–366| year = 1973 | url = https://www.researchgate.net/publication/38356319}}
  • Leon Henkin, J. Donald Monk, and Alfred Tarski (1971) Cylindric Algebras, Part I. North-Holland. {{ISBN|978-0-7204-2043-2}}.
  • Leon Henkin, J. Donald Monk, and Alfred Tarski (1985) Cylindric Algebras, Part II. North-Holland.
  • Robin Hirsch and Ian Hodkinson (2002) Relation algebras by games Studies in logic and the foundations of mathematics, North-Holland
  • {{cite book| author=Carlos Caleiro, Ricardo Gonçalves| chapter=On the algebraization of many-sorted logics| title=Proc. 18th int. conf. on Recent trends in algebraic development techniques (WADT)|editor=J. Fiadeiro and P.-Y. Schobbens| year=2006| volume=4409| pages=21–36| publisher=Springer| series=LNCS| isbn=978-3-540-71997-7| contribution-url=http://sqig.math.ist.utl.pt/pub/CaleiroC/06-CG-manysorted.pdf}}

Further reading

  • {{Cite journal | last1 = Imieliński | first1 = T. | author-link= Tomasz Imieliński | last2 = Lipski | first2 = W. | author2link = Witold Lipski|doi = 10.1016/0022-0000(84)90077-1 | title = The relational model of data and cylindric algebras | journal = Journal of Computer and System Sciences | volume = 28 | pages = 80–102| year = 1984 | doi-access = free }}