Algèbre de Heyting

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é.