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.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (53)

Cours associés (6)

Séances de cours associées (18)

Algèbre de Boole (logique)

Lalgèbre de Boole, ou calcul booléen, est la partie des mathématiques qui s'intéresse à une approche algébrique de la logique, vue en termes de variables, d'opérateurs et de fonctions sur les variables logiques, ce qui permet d'utiliser des techniques algébriques pour traiter les expressions à deux valeurs du calcul des propositions. Elle fut lancée en 1854 par le mathématicien britannique George Boole. L'algèbre de Boole trouve de nombreuses applications en informatique et dans la conception des circuits électroniques.

Algèbre de Heyting

Treillis (ensemble ordonné)

En mathématiques, un treillis () est une des structures algébriques utilisées en algèbre générale. C'est un ensemble partiellement ordonné dans lequel chaque paire d'éléments admet une borne supérieure et une borne inférieure. Un treillis peut être vu comme le treillis de Galois d'une relation binaire. Il existe en réalité deux définitions équivalentes du treillis, une concernant la relation d'ordre citée précédemment, l'autre algébrique. Tout ensemble muni d'une relation d'ordre total est un treillis.

Ce cours couvre les fondements des systèmes numériques. Sur la base d'algèbre Booléenne et de circuits combinatoires et séquentiels incluant les machines d'états finis, les methodes d'analyse et de sy

Ce cours couvre les fondements des systèmes numériques. Sur la base d'algèbre Booléenne et de circuitscombinatoires et séquentiels incluant les machines d'états finis, les methodes d'analyse et de syn

Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.

Théorème de la courbe de Jordan MATH-323: Algebraic topology

Couvre la preuve du théorème de la courbe de Jordan et les propriétés des sphères incorporées.

Aperçu des systèmes numériques : évolution et principes fondamentaux EE-110: Logic systems (for MT)

Explore l'évolution des systèmes numériques, couvrant les bases comme l'algèbre booléenne et les portes logiques, et met l'accent sur les compétences de travail d'équipe et le vocabulaire professionnel.

Aperçu des systèmes numériques : des transistors aux circuits intégrés EE-110: Logic systems (for MT)

Explore l'évolution des systèmes numériques des transistors aux circuits intégrés et leur impact sur les applications grand public et les technologies IoT.