Un treillis borné (avec 0 et 1) muni d'une opération binaire d'implication → satisfaisant l'adjonction a ∧ b ≤ c si et seulement si a ≤ (b → c) ; il fournit une sémantique algébrique pour la logique propositionnelle intuitionniste où le tiers exclu n'est pas assuré.

Principe

L'idée organisatrice est la résiduation : l'implication est le adjoint à droite du produit logique (∧) pour un antécédent fixé, codant une conditionnelle constructive qui peut manquer de négation classique et du tiers exclu.

Démonstration

Le treillis des ouverts d'un espace topologique, ordonné par inclusion, avec l'implication U → V donnée par le plus grand ouvert W tel que W ∧ U ≤ V (ou via l'intérieur de ((X ar{U}) ∪ V)), est une algèbre de Heyting et modèle de vérités intuitionnistes en topologie.

Mauvaise application

Confondre l'implication de Heyting avec l'implication matérielle (¬a ∨ b) ou supposer que chaque élément a un complément booléen conduit à des inférences classiques incorrectes comme le tiers exclu ou l'élimination de la double négation.

Conséquence

Une algèbre de Heyting permet des principes de raisonnement constructif, internalise algébriquement l'implication et peut servir d'objet de valeurs de vérité dans des contextes de type topos ; les transformations de preuves reflètent la résiduation algébrique.

Inversion

Spécifier une algèbre de Heyting en imposant à chaque élément un complément tel que a ∨ a' = 1 produit une algèbre de Boole et rétablit les lois classiques telles que le tiers exclu et l'élimination de la double négation.

Limite

Nécessite un treillis borné avec une implication satisfaisant la condition de résiduation ; exclut les treillis généraux sans cet adjoint ou les structures qui imposent la négation classique. Les algèbres de Heyting ne sont pas nécessairement complémentaires ni dotées de propriétés supplémentaires au-delà des axiomes du treillis.

Tension sémantique

Tension avec l'algèbre de Boole (logique classique) et avec des treillis sans implication ; la tension est entre l'implication constructive (résiduation) et l'implication matérielle classique, ainsi qu'entre sémantiques constructives internes et évaluations classiques externes.

Synthèse

Une algèbre de Heyting est le cadre algébrique de la logique intuitionniste : un treillis borné muni d'une implication résiduelle codant la conditionnelle constructive sans présupposer de compléments classiques.