Proof by example

2013-12-11T17:16:22Z

24.213.201.195:

The notion of '''cylindric algebra''', invented by [[Alfred Tarski]], arises naturally in the [[Algebraic logic|algebraization]] of [[first-order logic]] with [[First-order_logic#Equality_and_its_axioms|equality]]. This is comparable to the role [[Boolean algebra (structure)|Boolean algebra]]s play for [[propositional logic]]. Indeed, cylindric algebras are Boolean algebras equipped with additional cylindrification operations that model [[quantification]] and equality. They differ from [[polyadic algebra]]s in that the latter do not model equality.

== Definition of a cylindric algebra ==

A '''cylindric algebra of dimension''' <math>\alpha</math> (where <math>\alpha</math> is any [[ordinal number]]) is an algebraic structure <math>(A,+,\cdot,-,0,1,c_\kappa,d_{\kappa\lambda})_{\kappa,\lambda<\alpha}</math> such that <math>(A,+,\cdot,-,0,1)</math> is a [[Boolean algebra (structure)|Boolean algebra]], <math>c_\kappa</math> a unary operator on <math>A</math> for every <math>\kappa</math>, and <math>d_{\kappa\lambda}</math> a distinguished element of <math>A</math> for every <math>\kappa</math> and <math>\lambda</math>, such that the following hold:

(C1) <math>c_\kappa 0=0</math>

(C2) <math>x\leq c_\kappa x</math>

(C3) <math>c_\kappa(x\cdot c_\kappa y)=c_\kappa x\cdot c_\kappa y</math>

(C4) <math>c_\kappa c_\lambda x=c_\lambda c_\kappa x</math>

(C5) <math>d_{\kappa\kappa}=1</math>

(C6) If <math>\kappa\neq\lambda\mu</math>,{{clarify|reason=What is the juxtaposition 'λμ' of variables, or ordinals, supposed to mean? One possible reformulation in standard logical notation see below.|date=August 2013}} then <math>d_{\lambda\mu}=c_\kappa(d_{\lambda\kappa}\cdot d_{\kappa\mu})</math>

(C7) If <math>\kappa\neq\lambda</math>, then <math>c_\kappa(d_{\kappa\lambda}\cdot x)\cdot c_\kappa(d_{\kappa\lambda}\cdot -x)=0</math>

Assuming a presentation of first-order logic [[Functional predicate#Doing without functional predicates|without function symbol]]s,
the operator <math>c_\kappa x</math> models [[existential quantification]] over variable <math>\kappa</math> in formula <math>x</math> while the operator <math>d_{\kappa\lambda}</math> models the equality of variables <math>\kappa</math> and <math>\lambda</math>. Henceforth, reformulated using standard logical notations, the axioms read as

(C1) <math>\exists \kappa. \mathit{false} \Leftrightarrow \mathit{false}</math>

(C2) <math>x \Rightarrow \exists \kappa. x</math>

(C3) <math>\exists \kappa. (x\wedge \exists \kappa. y) \Leftrightarrow (\exists\kappa. x) \wedge (\exists\kappa. y)</math>

(C4) <math>\exists\kappa \exists\lambda. x \Leftrightarrow \exists \lambda \exists\kappa. x</math>

(C5) <math>\kappa=\kappa \Leftrightarrow \mathit{true}</math>

(C6) If <math>\kappa</math> is a variable different from both <math>\lambda</math> and <math>\mu</math>, {{clarify|reason=See above.|date=August 2013}} then <math>\lambda=\mu \Leftrightarrow \exists\kappa. (\lambda=\kappa \wedge \kappa=\mu)</math>

(C7) If <math>\kappa</math> and <math>\lambda</math> are different variables, then <math>\exists\kappa. (\kappa=\lambda \wedge x) \wedge \exists\kappa. (\kappa=\lambda\wedge \neg x) \Leftrightarrow \mathit{false}</math>

== Generalizations ==

Recently, cylindric algebras have been generalized to the [[Many-sorted logic|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
*[[Hyperdoctrine]]s are a [[Category theory|categorical]] formulation of cylindric algebras
*[[Relation algebra]]s (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.
* {{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| url=http://sqig.math.ist.utl.pt/pub/CaleiroC/06-CG-manysorted.pdf}}

== Further reading ==
* {{cite doi|10.1016/0022-0000(84)90077-1}}

[[Category:Algebraic logic]]

formulasearchengine - User contributions [en]

Proof by example