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. Une algèbre de Heyting est un treillis borné tel que, pour tout couple d'éléments , il existe un plus grand élément qui satisfaitCet élément est noté . Le plus grand élément de est dénoté 1 et le plus petit élément de est dénoté 0. Pour tout élément on définit le pseudo-complément de par . Cet élément vérifie la non contradiction : , et c'est d'ailleurs le plus grand élément de 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 . Il découle de l'existence de cet élément que toute algèbre de Heyting est distributive, c'est-à-direpour tout triplet . Un élément régulier est tel que . 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 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.