Algèbre de Heyting

Pour tout élément ${\displaystyle a\in H}$ on définit le pseudo-complément de ${\displaystyle a}$ par ${\displaystyle \neg a=(a\to 0)}$. Cet élément vérifie la non contradiction : ${\displaystyle a\wedge \neg a=0}$, et c'est d'ailleurs le plus grand élément de ${\displaystyle 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 ${\displaystyle 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

$${\displaystyle {\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 ${\displaystyle a,b,c\in H}$.

Un élément régulier ${\displaystyle x\in H}$ est tel que ${\displaystyle \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.

Un morphisme d'algèbres de Heyting commute aux opérations ${\displaystyle (\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 ${\displaystyle \wedge }$ et ${\displaystyle \to }$ dans ${\displaystyle H}$.

On a toujours ${\displaystyle \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 : ${\displaystyle \forall x,y\in H,\lnot (x\wedge y)=\lnot \lnot (\lnot x\vee \lnot y)}$.