Algèbre cylindrique

Une algèbre cylindrique de dimension ${\displaystyle \alpha }$ (où ${\displaystyle \alpha }$ est un nombre ordinal) est une structure algébrique ${\displaystyle (A,+,\cdot ,-,0,1,c_{\kappa },d_{\kappa \lambda })_{\kappa ,\lambda <\alpha }}$ tel que ${\displaystyle (A,+,\cdot ,-,0,1)}$ est une algèbre booléenne, ${\displaystyle c_{\kappa }}$ un opérateur unaire sur ${\displaystyle A}$ pour tout ${\displaystyle \kappa }$, et ${\displaystyle d_{\kappa \lambda }}$ un élément distingué de ${\displaystyle A}$ pour tout ${\displaystyle \kappa }$ et ${\displaystyle \lambda }$, de telle sorte que:

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

(C2) ${\displaystyle x\leq c_{\kappa }x}$

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

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

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

(C6) Si ${\displaystyle \kappa \notin \{\lambda ,\mu \}}$, alors ${\displaystyle d_{\lambda \mu }=c_{\kappa }(d_{\lambda \kappa }\cdot d_{\kappa \mu })}$

(C7) Si ${\displaystyle \kappa \neq \lambda }$, alors ${\displaystyle c_{\kappa }(d_{\kappa \lambda }\cdot x)\cdot c_{\kappa }(d_{\kappa \lambda }\cdot -x)=0}$

En supposant une présentation de la logique du premier ordre sans symboles de fonction, l'opérateur ${\displaystyle c_{\kappa }x}$ modélise quantification existentielle sur la variable ${\displaystyle \kappa }$ dans la formule ${\displaystyle x}$ tandis que l'opérateur ${\displaystyle d_{\kappa \lambda }}$ l'égalité des modèles des variables ${\displaystyle \kappa }$ et ${\displaystyle \lambda }$. Désormais, reformulé en utilisant les notations logiques standard, les axiomes peuvent se lire ainsi

(C1) ${\displaystyle \exists \kappa .{\mathit {faux}}\Leftrightarrow {\mathit {faux}}}$

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

(C3) ${\displaystyle \exists \kappa .(x\wedge \exists \kappa .y)\Leftrightarrow (\exists \kappa .x)\wedge (\exists \kappa .y)}$

(C4) ${\displaystyle \exists \kappa \exists \lambda .x\Leftrightarrow \exists \lambda \exists \kappa .x}$

(C5) ${\displaystyle \kappa =\kappa \Leftrightarrow {\mathit {vrai}}}$

(C6) Si ${\displaystyle \kappa }$ est une variable différente de ${\displaystyle \lambda }$ et ${\displaystyle \mu }$, alors ${\displaystyle \lambda =\mu \Leftrightarrow \exists \kappa .(\lambda =\kappa \wedge \kappa =\mu )}$

(C7) Si ${\displaystyle \kappa }$ et ${\displaystyle \lambda }$ sont différents entre elles, alors ${\displaystyle \exists \kappa .(\kappa =\lambda \wedge x)\wedge \exists \kappa .(\kappa =\lambda \wedge \neg x)\Leftrightarrow {\mathit {faux}}}$

• Logique algébrique abstraite
• Lambda calcul et logique combinatoire
• Logique algébrique

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Cylindric algebra » (voir la liste des auteurs).
• Leon Henkin, Monk, J.D., et Alfred Tarski (1971) Cylindric Algebras, Partie I. North-Holland. (ISBN 978-0-7204-2043-2).
• -------- (1985) Cylindric Algebras, Partie II. North-Holland.
• (en) Recent trends in algebraic development techniques : 18th International Workshop, WADT 2006, La Roche en Ardenne, Belgium, June 1-3, 2006, Revised Selected Papers, Springer, coll. « Lecture notes in computer science » (n^o 4409), 2007 (ISBN 978-3-540-71997-7, DOI 10.1007/978-3-540-71998-4_2, lire en ligne), « On the algebraization of many-sorted logics », p. 21-36