Algèbre de Heyting

En mathématiques, une algèbre de Heyting est une structure algébrique introduite en 1930 par le mathématicien néerlandais Arend Heyting pour rendre compte formellement de la logique intuitionniste de Brouwer, alors récemment développée. Les algèbres de Heyting sont donc pour la logique intuitionniste analogue à ce que sont des algèbres de Boole pour la logique classique : un modèle formel permettant d'en fixer les propriétés.

Les algèbres de Heyting jouent aujourd'hui un rôle important au-delà du seul domaine de la logique, par exemple en topologie dans la théorie des locales, et en informatique théorique. Dans ce domaine, Saul Kripke a montré en 1965 que toute équation dans une algèbre de Heyting est décidable, et Richard Statman a précisé que le problème est PSPACE-complet en 1979.

Définition

Une algèbre de Heyting est un treillis borné $H$ tel que, pour tout couple d'éléments $a,b\in H$, il existe un plus grand élément $x\in H$ qui satisfait

$$a\wedge x\leq b$$

Cet élément est noté $a\to b$. Le plus grand élément de $H$ est dénoté 1 et le plus petit élément de $H$ est dénoté 0.

Pseudo-complément

Pour tout élément $a\in H$ on définit le pseudo-complément de $a$ par $\neg a=(a\to 0)$. Cet élément vérifie la non contradiction : $a\wedge \neg a=0$, et c'est d'ailleurs le plus grand élément de $H$ qui satisfait cette propriété. En revanche, et c'est la différence notable entre la logique intuitionniste et la logique classique, il n'est pas vrai en général que $a\vee \neg a=1$.

Il découle de l'existence de cet élément que toute algèbre de Heyting est distributive, c'est-à-dire

$${\begin{aligned}a\wedge (b\vee c)=(a\wedge b)\vee (a\wedge c)\\a\vee (b\wedge c)=(a\vee b)\wedge (a\vee c)\end{aligned}}$$

pour tout triplet $a,b,c\in H$.

Éléments réguliers

Un élément régulier $x\in H$ est tel que $\neg \neg x=x$. Les éléments 0 et 1 sont toujours réguliers, mais ce n'est pas le cas des autres en général. Une algèbre de Heyting dans laquelle tous les éléments sont réguliers est en fait une algèbre de Boole.

Morphismes d'algèbres de Heyting

Un morphisme d'algèbres de Heyting commute aux opérations $(\vee ,\wedge ,\to )$ et envoie 0 sur 0. Cette opération est associative, et les algèbres de Heyting forment donc une catégorie. On peut, réciproquement, définir une algèbre de Heyting en termes catégoriques, comme un treillis borné possédant tous les objets exponentiels. La flèche de Heyting correspond alors à l'exponentielle, et on a une adjonction entre $\wedge$ et $\to$ dans $H$.

Exemples

Treillis de Rieger-Nishimura, correspondant à l'algèbre de Heyting libre engendrée par un élément $p$.

• Toute algèbre de Boole est en particulier une algèbre de Heyting, où $a\to b$ est donné par $\neg p\vee q$.
• L'ensemble des formules intuitionnistes générées par un terme est une algèbre de Heyting, on l'appelle treillis de Rieger-Nishimura.
• Dans tout espace topologique, la collection des ouverts forme une algèbre de Heyting. Dans ce cas, la flèche de Heyting $a\to b$ est donnée par $\operatorname {Int} (\complement _{a}\cup b)$, l'intérieur de l'union du complément de $a$ et de $b$. C'est le point de départ de la théorie des locales.
• L'algèbre de Lindenbaum est une algèbre de Heyting.
• Les algèbres de Łukasiewicz-Moisil sont des algèbres de Heyting.

Propriétés

Lois de De Morgan

On a toujours $\forall x,y\in H,\lnot (x\vee y)=\lnot x\wedge \lnot y$ dans une algèbre de Heyting comme en logique classique. En revanche, la relation duale n'est pas satisfaite, et on a à la place une version faible : $\forall x,y\in H,\lnot (x\wedge y)=\lnot \lnot (\lnot x\vee \lnot y)$.