{"history":[],"article":{"id":"0dcccf64-8eb0-4fd7-88d0-246a53459e9b","title":"Heyting algebra","slug":"heyting-algebra","content":":::summary\n:::\n\n# \nIn [mathematics](https://bliptext.com/articles/mathematics), a **Heyting algebra** (also known as **pseudo-Boolean algebra** ) is a [bounded lattice](https://bliptext.com/articles/lattice-order) (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation a → b called implication such that (c ∧ a) ≤ b is equivalent to c ≤ (a → b).\nFrom a logical standpoint, A → B is by this definition the weakest proposition for which [modus ponens](https://bliptext.com/articles/modus-ponens), the inference rule A → B, A ⊢ B, is sound.\nLike [Boolean algebras](https://bliptext.com/articles/boolean-algebra-structure), Heyting algebras form a [variety](https://bliptext.com/articles/variety-universal-algebra) axiomatizable with finitely many equations.\nHeyting algebras were introduced by to formalize [intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic).\nHeyting algebras are [distributive lattices](https://bliptext.com/articles/distributive-lattice).\nEvery Boolean algebra is a Heyting algebra when a → b is defined as ¬a ∨ b, as is every [complete](https://bliptext.com/articles/completeness-order-theory) [distributive lattice](https://bliptext.com/articles/distributive-lattice) satisfying a one-sided [infinite distributive law](https://bliptext.com/articles/distributivity-order-theory) when a → b is taken to be the [supremum](https://bliptext.com/articles/supremum) of the set of all c for which c ∧ a ≤ b.\nIn the finite case, every nonempty distributive lattice, in particular every nonempty finite [chain](https://bliptext.com/articles/total-order), is automatically complete and completely distributive, and hence a Heyting algebra.\nIt follows from the definition that 1 ≤ 0 → a, corresponding to the intuition that any proposition a is implied by a contradiction 0.\nAlthough the negation operation ¬a is not part of the definition, it is definable as a → 0.\nThe intuitive content of ¬a is the proposition that to assume a would lead to a contradiction.\nThe definition implies that a ∧ ¬a = 0.\nIt can further be shown that a ≤ ¬¬a, although the converse, ¬¬a ≤ a, is not true in general, that is, [double negation elimination](https://bliptext.com/articles/double-negation-elimination) does not hold in general in a Heyting algebra.\nHeyting algebras generalize Boolean algebras in the sense that Boolean algebras are precisely the Heyting algebras satisfying a ∨ ¬a = 1 ([excluded middle](https://bliptext.com/articles/excluded-middle)), equivalently ¬¬a = a.\nThose elements of a Heyting algebra H of the form ¬a comprise a Boolean lattice, but in general this is not a [subalgebra](https://bliptext.com/articles/subalgebra) of H (see [below](https://bliptext.com/articles/)).\nHeyting algebras serve as the algebraic models of propositional [intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic) in the same way Boolean algebras model propositional [classical logic](https://bliptext.com/articles/classical-logic).\nThe internal logic of an [elementary topos](https://bliptext.com/articles/elementary-topos) is based on the Heyting algebra of [subobjects](https://bliptext.com/articles/subobject) of the [terminal object](https://bliptext.com/articles/terminal-object) 1 ordered by inclusion, equivalently the morphisms from 1 to the [subobject classifier](https://bliptext.com/articles/subobject-classifier) Ω.\nThe [open sets](https://bliptext.com/articles/open-set) of any [topological space](https://bliptext.com/articles/topological-space) form a [complete Heyting algebra](https://bliptext.com/articles/complete-heyting-algebra).\nComplete Heyting algebras thus become a central object of study in [pointless topology](https://bliptext.com/articles/pointless-topology).\nEvery Heyting algebra whose set of non-greatest elements has a greatest element (and forms another Heyting algebra) is [subdirectly irreducible](https://bliptext.com/articles/subdirectly-irreducible-algebra), whence every Heyting algebra can be made [subdirectly irreducible](https://bliptext.com/articles/subdirectly-irreducible-algebra) by adjoining a new greatest element.\nIt follows that even among the finite Heyting algebras there exist infinitely many that are subdirectly irreducible, no two of which have the same [equational theory](https://bliptext.com/articles/equational-theory).\nHence no finite set of finite Heyting algebras can supply all the counterexamples to non-laws of Heyting algebra.\nThis is in sharp contrast to Boolean algebras, whose only subdirectly irreducible one is the two-element one, which on its own therefore suffices for all counterexamples to non-laws of Boolean algebra, the basis for the simple [truth table](https://bliptext.com/articles/truth-table) decision method.\nNevertheless, it is [decidable](https://bliptext.com/articles/decidability-logic) whether an equation holds of all Heyting algebras.\nHeyting algebras are less often called **pseudo-Boolean algebras**, or even **Brouwer lattices**, although the latter term may denote the dual definition, or have a slightly more general meaning.\n\n# Formal definition\nA Heyting algebra H is a [bounded lattice](https://bliptext.com/articles/lattice-order) such that for all a and b in H there is a greatest element x of H such that\nThis element is the **relative pseudo-complement** of a with respect to b, and is denoted a→b.\nWe write 1 and 0 for the largest and the smallest element of H, respectively.\nIn any Heyting algebra, one defines the **[pseudo-complement](https://bliptext.com/articles/pseudo-complement)** ¬a of any element a by setting ¬a = (a→0).\nBy definition,, and ¬a is the largest element having this property.\nHowever, it is not in general true that, thus ¬ is only a pseudo-[complement](https://bliptext.com/articles/complement-set-theory), not a true [complement](https://bliptext.com/articles/complement-set-theory), as would be the case in a Boolean algebra.\nA **[complete Heyting algebra](https://bliptext.com/articles/complete-heyting-algebra)** is a Heyting algebra that is a [complete lattice](https://bliptext.com/articles/complete-lattice).\nA **subalgebra** of a Heyting algebra H is a subset H1 of H containing 0 and 1 and closed under the operations ∧, ∨ and →.\nIt follows that it is also closed under ¬.\nA subalgebra is made into a Heyting algebra by the induced operations.\n\n# Alternative definitions\n\n## Category-theoretic definition\nA Heyting algebra H is a bounded lattice that has all [exponential objects](https://bliptext.com/articles/exponential-object).\nThe lattice H is regarded as a [category](https://bliptext.com/articles/category-mathematics) where\nmeet, \\wedge, is the [product](https://bliptext.com/articles/product-category-theory).\nThe exponential condition means that for any objects Y and Z in H an exponential Z^Y uniquely exists as an object in H.\nA Heyting implication (often written using \\Rightarrow or \\multimap to avoid confusions such as the use of \\to to indicate a [functor](https://bliptext.com/articles/functor)) is just an exponential: is an alternative notation for Z^Y.\nFrom the definition of exponentials we have that implication is [right adjoint](https://bliptext.com/articles/right-adjoint) to meet.\nThis adjunction can be written as or more fully as:\n\n## Lattice-theoretic definitions\nAn equivalent definition of Heyting algebras can be given by considering the mappings:\nfor some fixed a in H.\nA bounded lattice H is a Heyting algebra [if and only if](https://bliptext.com/articles/if-and-only-if) every mapping fa is the lower adjoint of a monotone [Galois connection](https://bliptext.com/articles/galois-connection).\nIn this case the respective upper adjoint ga is given by ga(x) = a→x, where → is defined as above.\nYet another definition is as a [residuated lattice](https://bliptext.com/articles/residuated-lattice) whose monoid operation is ∧.\nThe monoid unit must then be the top element 1.\nCommutativity of this monoid implies that the two residuals coincide as a→b.\n\n## Bounded lattice with an implication operation\nGiven a bounded lattice A with largest and smallest elements 1 and 0, and a binary operation →, these together form a Heyting algebra if and only if the following hold:\nwhere equation 4 is the distributive law for →.\n\n## Characterization using the axioms of intuitionistic logic\nThis characterization of Heyting algebras makes the proof of the basic facts concerning the relationship between intuitionist propositional calculus and Heyting algebras immediate.\n(For these facts, see the sections \"[Provable identities](https://bliptext.com/articles/)\" and \"[Universal constructions](https://bliptext.com/articles/)\".) One should think of the element \\top as meaning, intuitively, \"provably true\".\nCompare with the axioms at [Intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic).\nGiven a set A with three binary operations →, ∧ and ∨, and two distinguished elements \\bot and \\top, then A is a Heyting algebra for these operations (and the relation ≤ defined by the condition that a \\le b when a→b = \\top) if and only if the following conditions hold for any elements x, y and z of A:\nFinally, we define ¬x to be x→ \\bot.\nCondition 1 says that equivalent formulas should be identified.\nCondition 2 says that provably true formulas are closed under [modus ponens](https://bliptext.com/articles/modus-ponens).\nConditions 3 and 4 are then conditions.\nConditions 5, 6 and 7 are and conditions.\nConditions 8, 9 and 10 are or conditions.\nCondition 11 is a false condition.\nOf course, if a different set of axioms were chosen for logic, we could modify ours accordingly.\n\n# Examples\n

Every [Boolean algebra](https://bliptext.com/articles/boolean-algebra-structure) is a Heyting algebra, with p→q given by ¬p∨q.
Every [totally ordered set](https://bliptext.com/articles/total-order) that has a least element 0 and a greatest element 1 is a Heyting algebra (if viewed as a lattice).\nIn this case p→q equals to 1 when p≤q, and q otherwise.
The simplest Heyting algebra that is not already a Boolean algebra is the totally ordered set {0, 1⁄2, 1} (viewed as a lattice), yielding the operations:\nIn this example, that\n1⁄2∨¬1⁄2 = 1⁄2∨(1⁄2 → 0) = 1⁄2∨0 = 1⁄2\nfalsifies the law of excluded middle.\n
Every [topology](https://bliptext.com/articles/topology) provides a complete Heyting algebra in the form of its [open set](https://bliptext.com/articles/open-set) lattice.\nIn this case, the element A→B is the [interior](https://bliptext.com/articles/interior-topology) of the union of Ac and B, where Ac denotes the [complement](https://bliptext.com/articles/complement-set-theory) of the [open set](https://bliptext.com/articles/open-set) A.\nNot all complete Heyting algebras are of this form.\nThese issues are studied in [pointless topology](https://bliptext.com/articles/pointless-topology), where complete Heyting algebras are also called **frames** or **locales**.\n
Every [interior algebra](https://bliptext.com/articles/interior-algebra) provides a Heyting algebra in the form of its lattice of open elements.\nEvery Heyting algebra is of this form as a Heyting algebra can be completed to a Boolean algebra by taking its free Boolean extension as a bounded distributive lattice and then treating it as a [generalized topology](https://bliptext.com/articles/generalized-topology) in this Boolean algebra.\n
The [Lindenbaum algebra](https://bliptext.com/articles/lindenbaum-algebra) of propositional [intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic) is a Heyting algebra.
The [global elements](https://bliptext.com/articles/global-element) of the [subobject classifier](https://bliptext.com/articles/subobject-classifier) Ω of an [elementary topos](https://bliptext.com/articles/elementary-topos) form a Heyting algebra; it is the Heyting algebra of [truth values](https://bliptext.com/articles/truth-value) of the intuitionistic higher-order logic induced by the topos.\nMore generally, the set of [subobjects](https://bliptext.com/articles/subobject) of any object X in a topos forms a Heyting algebra.
[Łukasiewicz–Moisil algebras](https://bliptext.com/articles/ukasiewicz-moisil-algebra) (LMn) are also Heyting algebras for any n (but they are not [MV-algebras](https://bliptext.com/articles/mv-algebras) for n ≥ 5 ).\n

\n# [The free Heyting algebra over one generator (aka Rieger–Nishimura lattice) | upload.wikimedia.org/wikipedia/commons/5/5c/Rieger-Nishimura.svg]\n\n# Properties\n\n## General properties\nThe ordering \\le on a Heyting algebra H can be recovered from the operation → as follows: for any elements a, b of H, a \\le b if and only if a→b = 1.\nIn contrast to some [many-valued logics](https://bliptext.com/articles/many-valued-logic), Heyting algebras share the following property with Boolean algebras: if negation has a [fixed point](https://bliptext.com/articles/fixed-point-mathematics) (i.e. ¬a = a for some a), then the Heyting algebra is the trivial one-element Heyting algebra.\n\n## Provable identities\nGiven a formula of propositional calculus (using, in addition to the variables, the connectives, and the constants 0 and 1), it is a fact, proved early on in any study of Heyting algebras, that the following two conditions are equivalent:\nThe metaimplication 1 ⇒ 2 is extremely useful and is the principal practical method for proving identities in Heyting algebras.\nIn practice, one frequently uses the [deduction theorem](https://bliptext.com/articles/deduction-theorem) in such proofs.\nSince for any a and b in a Heyting algebra H we have a \\le b if and only if a→b = 1, it follows from 1 ⇒ 2 that whenever a formula F→G is provably true, we have for any Heyting algebra H, and any elements.\n(It follows from the deduction theorem that F→G is provable (unconditionally) if and only if G is provable from F, that is, if G is a provable consequence of F.) In particular, if F and G are provably equivalent, then, since ≤ is an order relation.\n1 ⇒ 2 can be proved by examining the logical axioms of the system of proof and verifying that their value is 1 in any Heyting algebra, and then verifying that the application of the rules of inference to expressions with value 1 in a Heyting algebra results in expressions with value 1.\nFor example, let us choose the system of proof having [modus ponens](https://bliptext.com/articles/modus-ponens) as its sole rule of inference, and whose axioms are the Hilbert-style ones given at [Intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic).\nThen the facts to be verified follow immediately from the axiom-like definition of Heyting algebras given above.\n1 ⇒ 2 also provides a method for proving that certain propositional formulas, though [tautologies](https://bliptext.com/articles/tautology-logic) in classical logic, cannot be proved in intuitionist propositional logic.\nIn order to prove that some formula is not provable, it is enough to exhibit a Heyting algebra H and elements such that.\nIf one wishes to avoid mention of logic, then in practice it becomes necessary to prove as a lemma a version of the deduction theorem valid for Heyting algebras: for any elements a, b and c of a Heyting algebra H, we have.\nFor more on the metaimplication 2 ⇒ 1, see the section \"[Universal constructions](https://bliptext.com/articles/)\" below.\n\n## Distributivity\nHeyting algebras are always [distributive](https://bliptext.com/articles/distributivity-order-theory).\nSpecifically, we always have the identities\nThe distributive law is sometimes stated as an axiom, but in fact it follows from the existence of relative pseudo-complements.\nThe reason is that, being the lower adjoint of a [Galois connection](https://bliptext.com/articles/galois-connection), \\wedge [preserves](https://bliptext.com/articles/limit-preserving-function-order-theory) all existing [suprema](https://bliptext.com/articles/suprema).\nDistributivity in turn is just the preservation of binary suprema by \\wedge.\nBy a similar argument, the following [infinite distributive law](https://bliptext.com/articles/infinite-distributive-law) holds in any complete Heyting algebra:\nfor any element x in H and any subset Y of H.\nConversely, any complete lattice satisfying the above infinite distributive law is a complete Heyting algebra, with\nbeing its relative pseudo-complement operation.\n\n## Regular and complemented elements\nAn element x of a Heyting algebra H is called **regular** if either of the following equivalent conditions hold:\nThe equivalence of these conditions can be restated simply as the identity ¬¬¬x = ¬x, valid for all x in H.\nElements x and y of a Heyting algebra H are called **complements** to each other if x∧y = 0 and x∨y = 1.\nIf it exists, any such y is unique and must in fact be equal to ¬x.\nWe call an element x **complemented** if it admits a complement.\nIt is true that if x is complemented, then so is ¬x, and then x and ¬x are complements to each other.\nHowever, confusingly, even if x is not complemented, ¬x may nonetheless have a complement (not equal to x).\nIn any Heyting algebra, the elements 0 and 1 are complements to each other.\nFor instance, it is possible that ¬x is 0 for every x different from 0, and 1 if x = 0, in which case 0 and 1 are the only regular elements.\nAny complemented element of a Heyting algebra is regular, though the converse is not true in general.\nIn particular, 0 and 1 are always regular.\nFor any Heyting algebra H, the following conditions are equivalent:\nIn this case, the element a→b is equal to ¬a ∨ b.\nThe regular (respectively complemented) elements of any Heyting algebra H constitute a Boolean algebra Hreg (respectively Hcomp), in which the operations ∧, ¬ and →, as well as the constants 0 and 1, coincide with those of H.\nIn the case of Hcomp, the operation ∨ is also the same, hence Hcomp is a subalgebra of H.\nIn general however, Hreg will not be a subalgebra of H, because its join operation ∨reg may be differ from ∨.\nFor x, y ∈ Hreg, we have x ∨reg y = ¬(¬x ∧ ¬y).\nSee below for necessary and sufficient conditions in order for ∨reg to coincide with ∨.\n\n## The De Morgan laws in a Heyting algebra\nOne of the two [De Morgan laws](https://bliptext.com/articles/de-morgan-laws) is satisfied in every Heyting algebra, namely\nHowever, the other De Morgan law does not always hold.\nWe have instead a weak de Morgan law:\nThe following statements are equivalent for all Heyting algebras H:\nCondition 2 is the other De Morgan law.\nCondition 6 says that the join operation ∨reg on the Boolean algebra Hreg of regular elements of H coincides with the operation ∨ of H.\nCondition 7 states that every regular element is complemented, i.e., Hreg = Hcomp.\nWe prove the equivalence.\nClearly the metaimplications 1 ⇒ 2, 2 ⇒ 3 and 4 ⇒ 5 are trivial.\nFurthermore, 3 ⇔ 4 and 5 ⇔ 6 result simply from the first De Morgan law and the definition of regular elements.\nWe show that 6 ⇒ 7 by taking ¬x and ¬¬x in place of x and y in 6 and using the identity a ∧ ¬a = 0.\nNotice that 2 ⇒ 1 follows from the first De Morgan law, and 7 ⇒ 6 results from the fact that the join operation ∨ on the subalgebra Hcomp is just the restriction of ∨ to Hcomp, taking into account the characterizations we have given of conditions 6 and 7.\nThe metaimplication 5 ⇒ 2 is a trivial consequence of the weak De Morgan law, taking ¬x and ¬y in place of x and y in 5.\nHeyting algebras satisfying the above properties are related to [De Morgan logic](https://bliptext.com/articles/intermediate-logic) in the same way Heyting algebras in general are related to intuitionist logic.\n\n# Heyting algebra morphisms\n\n## Definition\nGiven two Heyting algebras H1 and H2 and a mapping f : H1 → H2, we say that ƒ is a **[morphism](https://bliptext.com/articles/morphism)** of Heyting algebras if, for any elements x and y in H1, we have:\nIt follows from any of the last three conditions (2, 3, or 4) that f is an increasing function, that is, that f(x) ≤ f(y) whenever x ≤ y.\nAssume H1 and H2 are structures with operations →, ∧, ∨ (and possibly ¬) and constants 0 and 1, and f is a surjective mapping from H1 to H2 with properties 1 through 4 above.\nThen if H1 is a Heyting algebra, so too is H2.\nThis follows from the characterization of Heyting algebras as bounded lattices (thought of as algebraic structures rather than partially ordered sets) with an operation → satisfying certain identities.\n\n## Properties\nThe identity map f(x) = x from any Heyting algebra to itself is a morphism, and the composite g ∘ f of any two morphisms f and g is a morphism.\nHence Heyting algebras form a [category](https://bliptext.com/articles/category-mathematics).\n\n## Examples\nGiven a Heyting algebra H and any subalgebra H1, the inclusion mapping i : H1 → H is a morphism.\nFor any Heyting algebra H, the map x ↦ ¬¬x defines a morphism from H onto the Boolean algebra of its regular elements Hreg.\nThis is not in general a morphism from H to itself, since the join operation of Hreg may be different from that of H.\n\n# Quotients\nLet H be a Heyting algebra, and let F ⊆ H. We call F a **filter** on H if it satisfies the following properties:\nThe intersection of any set of filters on H is again a filter.\nTherefore, given any subset S of H there is a smallest filter containing S.\nWe call it the filter **generated** by S.\nIf S is empty, F = {1}.\nOtherwise, F is equal to the set of x in H such that there exist y1, y2, ..., yn ∈ S with y1 ∧ y2 ∧ ... ∧ yn ≤ x.\nIf H is a Heyting algebra and F is a filter on H, we define a relation ~ on H as follows: we write x ~ y whenever x → y and y → x both belong to F.\nThen ~ is an [equivalence relation](https://bliptext.com/articles/equivalence-relation); we write H/F for the [quotient set](https://bliptext.com/articles/quotient-set).\nThere is a unique Heyting algebra structure on H/F such that the canonical surjection pF : H → H/F becomes a Heyting algebra morphism.\nWe call the Heyting algebra H/F the **quotient** of H by F.\nLet S be a subset of a Heyting algebra H and let F be the filter generated by S.\nThen H/F satisfies the following universal property:\nLet f : H1 → H2 be a morphism of Heyting algebras.\nThe **kernel** of f, written ker f, is the set f−1[{1}].\nIt is a filter on H1.\n(Care should be taken because this definition, if applied to a morphism of Boolean algebras, is dual to what would be called the kernel of the morphism viewed as a morphism of rings.) By the foregoing, f induces a morphism : H1/(ker f) → H2.\nIt is an isomorphism of H1/(ker f) onto the subalgebra f[H1] of H2.\n\n# Universal constructions\n\n## Heyting algebra of propositional formulas in n variables up to intuitionist equivalence\nThe metaimplication 2 ⇒ 1 in the section \"[Provable identities](https://bliptext.com/articles/)\" is proved by showing that the result of the following construction is itself a Heyting algebra:\nAs always under the axiom-like definition of Heyting algebras, we define ≤ on H0 by the condition that x≤y if and only if x→y=1.\nSince, by the [deduction theorem](https://bliptext.com/articles/deduction-theorem), a formula F→G is provably true if and only if G is provable from F, it follows that [F]≤[G] if and only if F≼G.\nIn other words, ≤ is the order relation on L/~ induced by the preorder ≼ on L.\n\n## Free Heyting algebra on an arbitrary set of generators\nIn fact, the preceding construction can be carried out for any set of variables {Ai : i∈I} (possibly infinite).\nOne obtains in this way the free Heyting algebra on the variables {Ai}, which we will again denote by H0.\nIt is free in the sense that given any Heyting algebra H given together with a family of its elements 〈ai: i∈I 〉, there is a unique morphism f:H0→H satisfying f([Ai])=ai. The uniqueness of f is not difficult to see, and its existence results essentially from the metaimplication 1 ⇒ 2 of the section \"[Provable identities](https://bliptext.com/articles/)\" above, in the form of its corollary that whenever F and G are provably equivalent formulas, F(〈ai〉)=G(〈ai〉) for any family of elements 〈ai〉in H.\n\n## Heyting algebra of formulas equivalent with respect to a theory T\nGiven a set of formulas T in the variables {Ai}, viewed as axioms, the same construction could have been carried out with respect to a relation F≼G defined on L to mean that G is a provable consequence of F and the set of axioms T.\nLet us denote by HT the Heyting algebra so obtained.\nThen HT satisfies the same universal property as H0 above, but with respect to Heyting algebras H and families of elements 〈ai〉 satisfying the property that J(〈ai〉)=1 for any axiom J(〈Ai〉) in T.\n(Let us note that HT, taken with the family of its elements 〈[Ai]〉, itself satisfies this property.) The existence and uniqueness of the morphism is proved the same way as for H0, except that one must modify the metaimplication 1 ⇒ 2 in \"[Provable identities](https://bliptext.com/articles/)\" so that 1 reads \"provably true from T,\" and 2 reads \"any elements a1, a2,..., an in H satisfying the formulas of T.\"\nThe Heyting algebra HT that we have just defined can be viewed as a quotient of the free Heyting algebra H0 on the same set of variables, by applying the universal property of H0 with respect to HT, and the family of its elements 〈[Ai]〉.\nEvery Heyting algebra is isomorphic to one of the form HT. To see this, let H be any Heyting algebra, and let 〈ai: i∈I〉 be a family of elements generating H (for example, any surjective family).\nNow consider the set T of formulas J(〈Ai〉) in the variables 〈Ai: i∈I〉 such that J(〈ai〉)=1.\nThen we obtain a morphism f:HT→H by the universal property of HT, which is clearly surjective.\nIt is not difficult to show that f is injective.\n\n## Comparison to Lindenbaum algebras\nThe constructions we have just given play an entirely analogous role with respect to Heyting algebras to that of [Lindenbaum algebras](https://bliptext.com/articles/lindenbaum-algebra) with respect to [Boolean algebras](https://bliptext.com/articles/boolean-algebra-structure).\nIn fact, The Lindenbaum algebra BT in the variables {Ai} with respect to the axioms T is just our HT∪T 1, where T1 is the set of all formulas of the form ¬¬F→F, since the additional axioms of T1 are the only ones that need to be added in order to make all classical tautologies provable.\n\n# Heyting algebras as applied to intuitionistic logic\nIf one interprets the axioms of the intuitionistic propositional logic as terms of a Heyting algebra, then they will evaluate to the largest element, 1, in any Heyting algebra under any assignment of values to the formula's variables.\nFor instance, (P∧Q)→P is, by definition of the pseudo-complement, the largest element x such that.\nThis inequation is satisfied for any x, so the largest such x is 1.\nFurthermore, the rule of [modus ponens](https://bliptext.com/articles/modus-ponens) allows us to derive the formula Q from the formulas P and P→Q.\nBut in any Heyting algebra, if P has the value 1, and P→Q has the value 1, then it means that, and so ; it can only be that Q has the value 1.\nThis means that if a formula is deducible from the laws of intuitionistic logic, being derived from its axioms by way of the rule of modus ponens, then it will always have the value 1 in all Heyting algebras under any assignment of values to the formula's variables.\nHowever one can construct a Heyting algebra in which the value of [Peirce's law](https://bliptext.com/articles/peirce-s-law) is not always 1.\nConsider the 3-element algebra {0,1⁄2,1} as given above.\nIf we assign 1⁄2 to P and 0 to Q, then the value of Peirce's law ((P→Q)→P)→P is 1⁄2.\nIt follows that Peirce's law cannot be intuitionistically derived.\nSee [Curry–Howard isomorphism](https://bliptext.com/articles/curry-howard-isomorphism) for the general context of what this implies in [type theory](https://bliptext.com/articles/type-theory).\nThe converse can be proven as well: if a formula always has the value 1, then it is deducible from the laws of intuitionistic logic, so the intuitionistically valid formulas are exactly those that always have a value of 1.\nThis is similar to the notion that classically valid formulas are those formulas that have a value of 1 in the [two-element Boolean algebra](https://bliptext.com/articles/two-element-boolean-algebra) under any possible assignment of true and false to the formula's variables—that is, they are formulas that are tautologies in the usual truth-table sense.\nA Heyting algebra, from the logical standpoint, is then a generalization of the usual system of truth values, and its largest element 1 is analogous to 'true'.\nThe usual two-valued logic system is a special case of a Heyting algebra, and the smallest non-trivial one, in which the only elements of the algebra are 1 (true) and 0 (false).\n\n# Decision problems\nThe problem of whether a given equation holds in every Heyting algebra was shown to be decidable by [Saul Kripke](https://bliptext.com/articles/saul-kripke) in 1965.\nThe precise [computational complexity](https://bliptext.com/articles/computational-complexity-theory) of the problem was established by [Richard Statman](https://bliptext.com/articles/richard-statman) in 1979, who showed it was [PSPACE-complete](https://bliptext.com/articles/pspace-complete) and hence at least as hard as [deciding equations of Boolean algebra](https://bliptext.com/articles/boolean-satisfiability-problem) (shown coNP-complete in 1971 by [Stephen Cook](https://bliptext.com/articles/stephen-cook)) and conjectured to be considerably harder.\nThe elementary or first-order theory of Heyting algebras is undecidable.\nIt remains open whether the [universal Horn theory](https://bliptext.com/articles/universal-horn-theory) of Heyting algebras, or [word problem](https://bliptext.com/articles/word-problem-mathematics), is decidable.\nRegarding the word problem it is known that Heyting algebras are not locally finite (no Heyting algebra generated by a finite nonempty set is finite), in contrast to Boolean algebras, which are locally finite and whose word problem is decidable.\nIt is unknown whether free complete Heyting algebras exist except in the case of a single generator where the free Heyting algebra on one generator is trivially completable by adjoining a new top.\n\n# Topological representation and duality theory\nEvery Heyting algebra\nH\nis naturally isomorphic to a bounded sublattice\nL\nof open sets of a topological space\nX\n, where the implication U\\to V of\nL\nis given by the interior of.\nMore precisely,\nX\nis the [spectral space](https://bliptext.com/articles/spectral-space) of prime [ideals](https://bliptext.com/articles/ideal-order-theory) of the bounded lattice\nH\nand\nL\nis the lattice of open and quasi-compact subsets of\nX\n.\nMore generally, the category of Heyting algebras\nis dually equivalent to the category of Heyting spaces.\nThis duality can be seen as restriction of the classical [Stone duality](https://bliptext.com/articles/stone-duality) of bounded distributive lattices to the (non-full) subcategory of Heyting algebras.\nAlternatively, the category of Heyting algebras is dually equivalent to the category of [Esakia spaces](https://bliptext.com/articles/esakia-space).\nThis is called [Esakia duality](https://bliptext.com/articles/esakia-duality).","current_revision":null,"created_by":"kACnuQmH5k9Nr5VNVEpVeg7XpvUmMctD","created_at":"2025-01-25T19:07:21.564Z","updated_at":"2025-01-25T19:07:21.564Z","search_vector":"'algebra':2 'heyt':1","search_content":" \n \n\n# \nIn [mathematics](https://bliptext.com/articles/mathematics), a **Heyting algebra** (also known as **pseudo-Boolean algebra** ) is a [bounded lattice](https://bliptext.com/articles/lattice-order) (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation a → b called implication such that (c ∧ a) ≤ b is equivalent to c ≤ (a → b).\nFrom a logical standpoint, A → B is by this definition the weakest proposition for which [modus ponens](https://bliptext.com/articles/modus-ponens), the inference rule A → B, A ⊢ B, is sound.\nLike [Boolean algebras](https://bliptext.com/articles/boolean-algebra-structure), Heyting algebras form a [variety](https://bliptext.com/articles/variety-universal-algebra) axiomatizable with finitely many equations.\nHeyting algebras were introduced by to formalize [intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic).\nHeyting algebras are [distributive lattices](https://bliptext.com/articles/distributive-lattice).\nEvery Boolean algebra is a Heyting algebra when a → b is defined as ¬a ∨ b, as is every [complete](https://bliptext.com/articles/completeness-order-theory) [distributive lattice](https://bliptext.com/articles/distributive-lattice) satisfying a one-sided [infinite distributive law](https://bliptext.com/articles/distributivity-order-theory) when a → b is taken to be the [supremum](https://bliptext.com/articles/supremum) of the set of all c for which c ∧ a ≤ b.\nIn the finite case, every nonempty distributive lattice, in particular every nonempty finite [chain](https://bliptext.com/articles/total-order), is automatically complete and completely distributive, and hence a Heyting algebra.\nIt follows from the definition that 1 ≤ 0 → a, corresponding to the intuition that any proposition a is implied by a contradiction 0.\nAlthough the negation operation ¬a is not part of the definition, it is definable as a → 0.\nThe intuitive content of ¬a is the proposition that to assume a would lead to a contradiction.\nThe definition implies that a ∧ ¬a = 0.\nIt can further be shown that a ≤ ¬¬a, although the converse, ¬¬a ≤ a, is not true in general, that is, [double negation elimination](https://bliptext.com/articles/double-negation-elimination) does not hold in general in a Heyting algebra.\nHeyting algebras generalize Boolean algebras in the sense that Boolean algebras are precisely the Heyting algebras satisfying a ∨ ¬a = 1 ([excluded middle](https://bliptext.com/articles/excluded-middle)), equivalently ¬¬a = a.\nThose elements of a Heyting algebra H of the form ¬a comprise a Boolean lattice, but in general this is not a [subalgebra](https://bliptext.com/articles/subalgebra) of H (see [below](https://bliptext.com/articles/)).\nHeyting algebras serve as the algebraic models of propositional [intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic) in the same way Boolean algebras model propositional [classical logic](https://bliptext.com/articles/classical-logic).\nThe internal logic of an [elementary topos](https://bliptext.com/articles/elementary-topos) is based on the Heyting algebra of [subobjects](https://bliptext.com/articles/subobject) of the [terminal object](https://bliptext.com/articles/terminal-object) 1 ordered by inclusion, equivalently the morphisms from 1 to the [subobject classifier](https://bliptext.com/articles/subobject-classifier) Ω.\nThe [open sets](https://bliptext.com/articles/open-set) of any [topological space](https://bliptext.com/articles/topological-space) form a [complete Heyting algebra](https://bliptext.com/articles/complete-heyting-algebra).\nComplete Heyting algebras thus become a central object of study in [pointless topology](https://bliptext.com/articles/pointless-topology).\nEvery Heyting algebra whose set of non-greatest elements has a greatest element (and forms another Heyting algebra) is [subdirectly irreducible](https://bliptext.com/articles/subdirectly-irreducible-algebra), whence every Heyting algebra can be made [subdirectly irreducible](https://bliptext.com/articles/subdirectly-irreducible-algebra) by adjoining a new greatest element.\nIt follows that even among the finite Heyting algebras there exist infinitely many that are subdirectly irreducible, no two of which have the same [equational theory](https://bliptext.com/articles/equational-theory).\nHence no finite set of finite Heyting algebras can supply all the counterexamples to non-laws of Heyting algebra.\nThis is in sharp contrast to Boolean algebras, whose only subdirectly irreducible one is the two-element one, which on its own therefore suffices for all counterexamples to non-laws of Boolean algebra, the basis for the simple [truth table](https://bliptext.com/articles/truth-table) decision method.\nNevertheless, it is [decidable](https://bliptext.com/articles/decidability-logic) whether an equation holds of all Heyting algebras.\nHeyting algebras are less often called **pseudo-Boolean algebras**, or even **Brouwer lattices**, although the latter term may denote the dual definition, or have a slightly more general meaning.\n\n# Formal definition\nA Heyting algebra H is a [bounded lattice](https://bliptext.com/articles/lattice-order) such that for all a and b in H there is a greatest element x of H such that\nThis element is the **relative pseudo-complement** of a with respect to b, and is denoted a→b.\nWe write 1 and 0 for the largest and the smallest element of H, respectively.\nIn any Heyting algebra, one defines the **[pseudo-complement](https://bliptext.com/articles/pseudo-complement)** ¬a of any element a by setting ¬a = (a→0).\nBy definition,, and ¬a is the largest element having this property.\nHowever, it is not in general true that, thus ¬ is only a pseudo-[complement](https://bliptext.com/articles/complement-set-theory), not a true [complement](https://bliptext.com/articles/complement-set-theory), as would be the case in a Boolean algebra.\nA **[complete Heyting algebra](https://bliptext.com/articles/complete-heyting-algebra)** is a Heyting algebra that is a [complete lattice](https://bliptext.com/articles/complete-lattice).\nA **subalgebra** of a Heyting algebra H is a subset H1 of H containing 0 and 1 and closed under the operations ∧, ∨ and →.\nIt follows that it is also closed under ¬.\nA subalgebra is made into a Heyting algebra by the induced operations.\n\n# Alternative definitions\n\n## Category-theoretic definition\nA Heyting algebra H is a bounded lattice that has all [exponential objects](https://bliptext.com/articles/exponential-object).\nThe lattice H is regarded as a [category](https://bliptext.com/articles/category-mathematics) where\nmeet, \\wedge, is the [product](https://bliptext.com/articles/product-category-theory).\nThe exponential condition means that for any objects Y and Z in H an exponential Z^Y uniquely exists as an object in H.\nA Heyting implication (often written using \\Rightarrow or \\multimap to avoid confusions such as the use of \\to to indicate a [functor](https://bliptext.com/articles/functor)) is just an exponential: is an alternative notation for Z^Y.\nFrom the definition of exponentials we have that implication is [right adjoint](https://bliptext.com/articles/right-adjoint) to meet.\nThis adjunction can be written as or more fully as:\n\n## Lattice-theoretic definitions\nAn equivalent definition of Heyting algebras can be given by considering the mappings:\nfor some fixed a in H.\nA bounded lattice H is a Heyting algebra [if and only if](https://bliptext.com/articles/if-and-only-if) every mapping fa is the lower adjoint of a monotone [Galois connection](https://bliptext.com/articles/galois-connection).\nIn this case the respective upper adjoint ga is given by ga(x) = a→x, where → is defined as above.\nYet another definition is as a [residuated lattice](https://bliptext.com/articles/residuated-lattice) whose monoid operation is ∧.\nThe monoid unit must then be the top element 1.\nCommutativity of this monoid implies that the two residuals coincide as a→b.\n\n## Bounded lattice with an implication operation\nGiven a bounded lattice A with largest and smallest elements 1 and 0, and a binary operation →, these together form a Heyting algebra if and only if the following hold:\nwhere equation 4 is the distributive law for →.\n\n## Characterization using the axioms of intuitionistic logic\nThis characterization of Heyting algebras makes the proof of the basic facts concerning the relationship between intuitionist propositional calculus and Heyting algebras immediate.\n(For these facts, see the sections \"[Provable identities](https://bliptext.com/articles/)\" and \"[Universal constructions](https://bliptext.com/articles/)\".) One should think of the element \\top as meaning, intuitively, \"provably true\".\nCompare with the axioms at [Intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic).\nGiven a set A with three binary operations →, ∧ and ∨, and two distinguished elements \\bot and \\top, then A is a Heyting algebra for these operations (and the relation ≤ defined by the condition that a \\le b when a→b = \\top) if and only if the following conditions hold for any elements x, y and z of A:\nFinally, we define ¬x to be x→ \\bot.\nCondition 1 says that equivalent formulas should be identified.\nCondition 2 says that provably true formulas are closed under [modus ponens](https://bliptext.com/articles/modus-ponens).\nConditions 3 and 4 are then conditions.\nConditions 5, 6 and 7 are and conditions.\nConditions 8, 9 and 10 are or conditions.\nCondition 11 is a false condition.\nOf course, if a different set of axioms were chosen for logic, we could modify ours accordingly.\n\n# Examples\n \n Every [Boolean algebra](https://bliptext.com/articles/boolean-algebra-structure) is a Heyting algebra, with p→q given by ¬p∨q. \n Every [totally ordered set](https://bliptext.com/articles/total-order) that has a least element 0 and a greatest element 1 is a Heyting algebra (if viewed as a lattice).\nIn this case p→q equals to 1 when p≤q, and q otherwise. \n The simplest Heyting algebra that is not already a Boolean algebra is the totally ordered set {0, 1⁄2, 1} (viewed as a lattice), yielding the operations:\nIn this example, that\n1⁄2∨¬1⁄2 = 1⁄2∨(1⁄2 → 0) = 1⁄2∨0 = 1⁄2\nfalsifies the law of excluded middle.\n Every [topology](https://bliptext.com/articles/topology) provides a complete Heyting algebra in the form of its [open set](https://bliptext.com/articles/open-set) lattice.\nIn this case, the element A→B is the [interior](https://bliptext.com/articles/interior-topology) of the union of Ac and B, where Ac denotes the [complement](https://bliptext.com/articles/complement-set-theory) of the [open set](https://bliptext.com/articles/open-set) A.\nNot all complete Heyting algebras are of this form.\nThese issues are studied in [pointless topology](https://bliptext.com/articles/pointless-topology), where complete Heyting algebras are also called **frames** or **locales**.\n Every [interior algebra](https://bliptext.com/articles/interior-algebra) provides a Heyting algebra in the form of its lattice of open elements.\nEvery Heyting algebra is of this form as a Heyting algebra can be completed to a Boolean algebra by taking its free Boolean extension as a bounded distributive lattice and then treating it as a [generalized topology](https://bliptext.com/articles/generalized-topology) in this Boolean algebra.\n The [Lindenbaum algebra](https://bliptext.com/articles/lindenbaum-algebra) of propositional [intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic) is a Heyting algebra. \n The [global elements](https://bliptext.com/articles/global-element) of the [subobject classifier](https://bliptext.com/articles/subobject-classifier) Ω of an [elementary topos](https://bliptext.com/articles/elementary-topos) form a Heyting algebra; it is the Heyting algebra of [truth values](https://bliptext.com/articles/truth-value) of the intuitionistic higher-order logic induced by the topos.\nMore generally, the set of [subobjects](https://bliptext.com/articles/subobject) of any object X in a topos forms a Heyting algebra. \n [Łukasiewicz–Moisil algebras](https://bliptext.com/articles/ukasiewicz-moisil-algebra) (LMn) are also Heyting algebras for any n (but they are not [MV-algebras](https://bliptext.com/articles/mv-algebras) for n ≥ 5 ).\n \n# [The free Heyting algebra over one generator (aka Rieger–Nishimura lattice) | upload.wikimedia.org/wikipedia/commons/5/5c/Rieger-Nishimura.svg]\n\n# Properties\n\n## General properties\nThe ordering \\le on a Heyting algebra H can be recovered from the operation → as follows: for any elements a, b of H, a \\le b if and only if a→b = 1.\nIn contrast to some [many-valued logics](https://bliptext.com/articles/many-valued-logic), Heyting algebras share the following property with Boolean algebras: if negation has a [fixed point](https://bliptext.com/articles/fixed-point-mathematics) (i.e. ¬a = a for some a), then the Heyting algebra is the trivial one-element Heyting algebra.\n\n## Provable identities\nGiven a formula of propositional calculus (using, in addition to the variables, the connectives, and the constants 0 and 1), it is a fact, proved early on in any study of Heyting algebras, that the following two conditions are equivalent:\nThe metaimplication 1 ⇒ 2 is extremely useful and is the principal practical method for proving identities in Heyting algebras.\nIn practice, one frequently uses the [deduction theorem](https://bliptext.com/articles/deduction-theorem) in such proofs.\nSince for any a and b in a Heyting algebra H we have a \\le b if and only if a→b = 1, it follows from 1 ⇒ 2 that whenever a formula F→G is provably true, we have for any Heyting algebra H, and any elements.\n(It follows from the deduction theorem that F→G is provable (unconditionally) if and only if G is provable from F, that is, if G is a provable consequence of F.) In particular, if F and G are provably equivalent, then, since ≤ is an order relation.\n1 ⇒ 2 can be proved by examining the logical axioms of the system of proof and verifying that their value is 1 in any Heyting algebra, and then verifying that the application of the rules of inference to expressions with value 1 in a Heyting algebra results in expressions with value 1.\nFor example, let us choose the system of proof having [modus ponens](https://bliptext.com/articles/modus-ponens) as its sole rule of inference, and whose axioms are the Hilbert-style ones given at [Intuitionistic logic](https://bliptext.com/articles/intuitionistic-logic).\nThen the facts to be verified follow immediately from the axiom-like definition of Heyting algebras given above.\n1 ⇒ 2 also provides a method for proving that certain propositional formulas, though [tautologies](https://bliptext.com/articles/tautology-logic) in classical logic, cannot be proved in intuitionist propositional logic.\nIn order to prove that some formula is not provable, it is enough to exhibit a Heyting algebra H and elements such that.\nIf one wishes to avoid mention of logic, then in practice it becomes necessary to prove as a lemma a version of the deduction theorem valid for Heyting algebras: for any elements a, b and c of a Heyting algebra H, we have.\nFor more on the metaimplication 2 ⇒ 1, see the section \"[Universal constructions](https://bliptext.com/articles/)\" below.\n\n## Distributivity\nHeyting algebras are always [distributive](https://bliptext.com/articles/distributivity-order-theory).\nSpecifically, we always have the identities\nThe distributive law is sometimes stated as an axiom, but in fact it follows from the existence of relative pseudo-complements.\nThe reason is that, being the lower adjoint of a [Galois connection](https://bliptext.com/articles/galois-connection), \\wedge [preserves](https://bliptext.com/articles/limit-preserving-function-order-theory) all existing [suprema](https://bliptext.com/articles/suprema).\nDistributivity in turn is just the preservation of binary suprema by \\wedge.\nBy a similar argument, the following [infinite distributive law](https://bliptext.com/articles/infinite-distributive-law) holds in any complete Heyting algebra:\nfor any element x in H and any subset Y of H.\nConversely, any complete lattice satisfying the above infinite distributive law is a complete Heyting algebra, with\nbeing its relative pseudo-complement operation.\n\n## Regular and complemented elements\nAn element x of a Heyting algebra H is called **regular** if either of the following equivalent conditions hold:\nThe equivalence of these conditions can be restated simply as the identity ¬¬¬x = ¬x, valid for all x in H.\nElements x and y of a Heyting algebra H are called **complements** to each other if x∧y = 0 and x∨y = 1.\nIf it exists, any such y is unique and must in fact be equal to ¬x.\nWe call an element x **complemented** if it admits a complement.\nIt is true that if x is complemented, then so is ¬x, and then x and ¬x are complements to each other.\nHowever, confusingly, even if x is not complemented, ¬x may nonetheless have a complement (not equal to x).\nIn any Heyting algebra, the elements 0 and 1 are complements to each other.\nFor instance, it is possible that ¬x is 0 for every x different from 0, and 1 if x = 0, in which case 0 and 1 are the only regular elements.\nAny complemented element of a Heyting algebra is regular, though the converse is not true in general.\nIn particular, 0 and 1 are always regular.\nFor any Heyting algebra H, the following conditions are equivalent:\nIn this case, the element a→b is equal to ¬a ∨ b.\nThe regular (respectively complemented) elements of any Heyting algebra H constitute a Boolean algebra Hreg (respectively Hcomp), in which the operations ∧, ¬ and →, as well as the constants 0 and 1, coincide with those of H.\nIn the case of Hcomp, the operation ∨ is also the same, hence Hcomp is a subalgebra of H.\nIn general however, Hreg will not be a subalgebra of H, because its join operation ∨reg may be differ from ∨.\nFor x, y ∈ Hreg, we have x ∨reg y = ¬(¬x ∧ ¬y).\nSee below for necessary and sufficient conditions in order for ∨reg to coincide with ∨.\n\n## The De Morgan laws in a Heyting algebra\nOne of the two [De Morgan laws](https://bliptext.com/articles/de-morgan-laws) is satisfied in every Heyting algebra, namely\nHowever, the other De Morgan law does not always hold.\nWe have instead a weak de Morgan law:\nThe following statements are equivalent for all Heyting algebras H:\nCondition 2 is the other De Morgan law.\nCondition 6 says that the join operation ∨reg on the Boolean algebra Hreg of regular elements of H coincides with the operation ∨ of H.\nCondition 7 states that every regular element is complemented, i.e., Hreg = Hcomp.\nWe prove the equivalence.\nClearly the metaimplications 1 ⇒ 2, 2 ⇒ 3 and 4 ⇒ 5 are trivial.\nFurthermore, 3 ⇔ 4 and 5 ⇔ 6 result simply from the first De Morgan law and the definition of regular elements.\nWe show that 6 ⇒ 7 by taking ¬x and ¬¬x in place of x and y in 6 and using the identity a ∧ ¬a = 0.\nNotice that 2 ⇒ 1 follows from the first De Morgan law, and 7 ⇒ 6 results from the fact that the join operation ∨ on the subalgebra Hcomp is just the restriction of ∨ to Hcomp, taking into account the characterizations we have given of conditions 6 and 7.\nThe metaimplication 5 ⇒ 2 is a trivial consequence of the weak De Morgan law, taking ¬x and ¬y in place of x and y in 5.\nHeyting algebras satisfying the above properties are related to [De Morgan logic](https://bliptext.com/articles/intermediate-logic) in the same way Heyting algebras in general are related to intuitionist logic.\n\n# Heyting algebra morphisms\n\n## Definition\nGiven two Heyting algebras H1 and H2 and a mapping f : H1 → H2, we say that ƒ is a **[morphism](https://bliptext.com/articles/morphism)** of Heyting algebras if, for any elements x and y in H1, we have:\nIt follows from any of the last three conditions (2, 3, or 4) that f is an increasing function, that is, that f(x) ≤ f(y) whenever x ≤ y.\nAssume H1 and H2 are structures with operations →, ∧, ∨ (and possibly ¬) and constants 0 and 1, and f is a surjective mapping from H1 to H2 with properties 1 through 4 above.\nThen if H1 is a Heyting algebra, so too is H2.\nThis follows from the characterization of Heyting algebras as bounded lattices (thought of as algebraic structures rather than partially ordered sets) with an operation → satisfying certain identities.\n\n## Properties\nThe identity map f(x) = x from any Heyting algebra to itself is a morphism, and the composite g ∘ f of any two morphisms f and g is a morphism.\nHence Heyting algebras form a [category](https://bliptext.com/articles/category-mathematics).\n\n## Examples\nGiven a Heyting algebra H and any subalgebra H1, the inclusion mapping i : H1 → H is a morphism.\nFor any Heyting algebra H, the map x ↦ ¬¬x defines a morphism from H onto the Boolean algebra of its regular elements Hreg.\nThis is not in general a morphism from H to itself, since the join operation of Hreg may be different from that of H.\n\n# Quotients\nLet H be a Heyting algebra, and let F ⊆ H. We call F a **filter** on H if it satisfies the following properties:\nThe intersection of any set of filters on H is again a filter.\nTherefore, given any subset S of H there is a smallest filter containing S.\nWe call it the filter **generated** by S.\nIf S is empty, F = {1}.\nOtherwise, F is equal to the set of x in H such that there exist y1, y2, ..., yn ∈ S with y1 ∧ y2 ∧ ... ∧ yn ≤ x.\nIf H is a Heyting algebra and F is a filter on H, we define a relation ~ on H as follows: we write x ~ y whenever x → y and y → x both belong to F.\nThen ~ is an [equivalence relation](https://bliptext.com/articles/equivalence-relation); we write H/F for the [quotient set](https://bliptext.com/articles/quotient-set).\nThere is a unique Heyting algebra structure on H/F such that the canonical surjection pF : H → H/F becomes a Heyting algebra morphism.\nWe call the Heyting algebra H/F the **quotient** of H by F.\nLet S be a subset of a Heyting algebra H and let F be the filter generated by S.\nThen H/F satisfies the following universal property:\nLet f : H1 → H2 be a morphism of Heyting algebras.\nThe **kernel** of f, written ker f, is the set f−1[{1}].\nIt is a filter on H1.\n(Care should be taken because this definition, if applied to a morphism of Boolean algebras, is dual to what would be called the kernel of the morphism viewed as a morphism of rings.) By the foregoing, f induces a morphism : H1/(ker f) → H2.\nIt is an isomorphism of H1/(ker f) onto the subalgebra f[H1] of H2.\n\n# Universal constructions\n\n## Heyting algebra of propositional formulas in n variables up to intuitionist equivalence\nThe metaimplication 2 ⇒ 1 in the section \"[Provable identities](https://bliptext.com/articles/)\" is proved by showing that the result of the following construction is itself a Heyting algebra:\nAs always under the axiom-like definition of Heyting algebras, we define ≤ on H0 by the condition that x≤y if and only if x→y=1.\nSince, by the [deduction theorem](https://bliptext.com/articles/deduction-theorem), a formula F→G is provably true if and only if G is provable from F, it follows that [F]≤[G] if and only if F≼G.\nIn other words, ≤ is the order relation on L/~ induced by the preorder ≼ on L.\n\n## Free Heyting algebra on an arbitrary set of generators\nIn fact, the preceding construction can be carried out for any set of variables {Ai : i∈I} (possibly infinite).\nOne obtains in this way the free Heyting algebra on the variables {Ai}, which we will again denote by H0.\nIt is free in the sense that given any Heyting algebra H given together with a family of its elements 〈ai: i∈I 〉, there is a unique morphism f:H0→H satisfying f([Ai])=ai. The uniqueness of f is not difficult to see, and its existence results essentially from the metaimplication 1 ⇒ 2 of the section \"[Provable identities](https://bliptext.com/articles/)\" above, in the form of its corollary that whenever F and G are provably equivalent formulas, F(〈ai〉)=G(〈ai〉) for any family of elements 〈ai〉in H.\n\n## Heyting algebra of formulas equivalent with respect to a theory T\nGiven a set of formulas T in the variables {Ai}, viewed as axioms, the same construction could have been carried out with respect to a relation F≼G defined on L to mean that G is a provable consequence of F and the set of axioms T.\nLet us denote by HT the Heyting algebra so obtained.\nThen HT satisfies the same universal property as H0 above, but with respect to Heyting algebras H and families of elements 〈ai〉 satisfying the property that J(〈ai〉)=1 for any axiom J(〈Ai〉) in T.\n(Let us note that HT, taken with the family of its elements 〈[Ai]〉, itself satisfies this property.) The existence and uniqueness of the morphism is proved the same way as for H0, except that one must modify the metaimplication 1 ⇒ 2 in \"[Provable identities](https://bliptext.com/articles/)\" so that 1 reads \"provably true from T,\" and 2 reads \"any elements a1, a2,..., an in H satisfying the formulas of T.\"\nThe Heyting algebra HT that we have just defined can be viewed as a quotient of the free Heyting algebra H0 on the same set of variables, by applying the universal property of H0 with respect to HT, and the family of its elements 〈[Ai]〉.\nEvery Heyting algebra is isomorphic to one of the form HT. To see this, let H be any Heyting algebra, and let 〈ai: i∈I〉 be a family of elements generating H (for example, any surjective family).\nNow consider the set T of formulas J(〈Ai〉) in the variables 〈Ai: i∈I〉 such that J(〈ai〉)=1.\nThen we obtain a morphism f:HT→H by the universal property of HT, which is clearly surjective.\nIt is not difficult to show that f is injective.\n\n## Comparison to Lindenbaum algebras\nThe constructions we have just given play an entirely analogous role with respect to Heyting algebras to that of [Lindenbaum algebras](https://bliptext.com/articles/lindenbaum-algebra) with respect to [Boolean algebras](https://bliptext.com/articles/boolean-algebra-structure).\nIn fact, The Lindenbaum algebra BT in the variables {Ai} with respect to the axioms T is just our HT∪T 1, where T1 is the set of all formulas of the form ¬¬F→F, since the additional axioms of T1 are the only ones that need to be added in order to make all classical tautologies provable.\n\n# Heyting algebras as applied to intuitionistic logic\nIf one interprets the axioms of the intuitionistic propositional logic as terms of a Heyting algebra, then they will evaluate to the largest element, 1, in any Heyting algebra under any assignment of values to the formula's variables.\nFor instance, (P∧Q)→P is, by definition of the pseudo-complement, the largest element x such that.\nThis inequation is satisfied for any x, so the largest such x is 1.\nFurthermore, the rule of [modus ponens](https://bliptext.com/articles/modus-ponens) allows us to derive the formula Q from the formulas P and P→Q.\nBut in any Heyting algebra, if P has the value 1, and P→Q has the value 1, then it means that, and so ; it can only be that Q has the value 1.\nThis means that if a formula is deducible from the laws of intuitionistic logic, being derived from its axioms by way of the rule of modus ponens, then it will always have the value 1 in all Heyting algebras under any assignment of values to the formula's variables.\nHowever one can construct a Heyting algebra in which the value of [Peirce's law](https://bliptext.com/articles/peirce-s-law) is not always 1.\nConsider the 3-element algebra {0,1⁄2,1} as given above.\nIf we assign 1⁄2 to P and 0 to Q, then the value of Peirce's law ((P→Q)→P)→P is 1⁄2.\nIt follows that Peirce's law cannot be intuitionistically derived.\nSee [Curry–Howard isomorphism](https://bliptext.com/articles/curry-howard-isomorphism) for the general context of what this implies in [type theory](https://bliptext.com/articles/type-theory).\nThe converse can be proven as well: if a formula always has the value 1, then it is deducible from the laws of intuitionistic logic, so the intuitionistically valid formulas are exactly those that always have a value of 1.\nThis is similar to the notion that classically valid formulas are those formulas that have a value of 1 in the [two-element Boolean algebra](https://bliptext.com/articles/two-element-boolean-algebra) under any possible assignment of true and false to the formula's variables—that is, they are formulas that are tautologies in the usual truth-table sense.\nA Heyting algebra, from the logical standpoint, is then a generalization of the usual system of truth values, and its largest element 1 is analogous to 'true'.\nThe usual two-valued logic system is a special case of a Heyting algebra, and the smallest non-trivial one, in which the only elements of the algebra are 1 (true) and 0 (false).\n\n# Decision problems\nThe problem of whether a given equation holds in every Heyting algebra was shown to be decidable by [Saul Kripke](https://bliptext.com/articles/saul-kripke) in 1965.\nThe precise [computational complexity](https://bliptext.com/articles/computational-complexity-theory) of the problem was established by [Richard Statman](https://bliptext.com/articles/richard-statman) in 1979, who showed it was [PSPACE-complete](https://bliptext.com/articles/pspace-complete) and hence at least as hard as [deciding equations of Boolean algebra](https://bliptext.com/articles/boolean-satisfiability-problem) (shown coNP-complete in 1971 by [Stephen Cook](https://bliptext.com/articles/stephen-cook)) and conjectured to be considerably harder.\nThe elementary or first-order theory of Heyting algebras is undecidable.\nIt remains open whether the [universal Horn theory](https://bliptext.com/articles/universal-horn-theory) of Heyting algebras, or [word problem](https://bliptext.com/articles/word-problem-mathematics), is decidable.\nRegarding the word problem it is known that Heyting algebras are not locally finite (no Heyting algebra generated by a finite nonempty set is finite), in contrast to Boolean algebras, which are locally finite and whose word problem is decidable.\nIt is unknown whether free complete Heyting algebras exist except in the case of a single generator where the free Heyting algebra on one generator is trivially completable by adjoining a new top.\n\n# Topological representation and duality theory\nEvery Heyting algebra\nH\nis naturally isomorphic to a bounded sublattice\nL\nof open sets of a topological space\nX\n, where the implication U\\to V of\nL\nis given by the interior of.\nMore precisely,\nX\nis the [spectral space](https://bliptext.com/articles/spectral-space) of prime [ideals](https://bliptext.com/articles/ideal-order-theory) of the bounded lattice\nH\nand\nL\nis the lattice of open and quasi-compact subsets of\nX\n.\nMore generally, the category of Heyting algebras\nis dually equivalent to the category of Heyting spaces.\nThis duality can be seen as restriction of the classical [Stone duality](https://bliptext.com/articles/stone-duality) of bounded distributive lattices to the (non-full) subcategory of Heyting algebras.\nAlternatively, the category of Heyting algebras is dually equivalent to the category of [Esakia spaces](https://bliptext.com/articles/esakia-space).\nThis is called [Esakia duality](https://bliptext.com/articles/esakia-duality).","revisionCount":0},"hasMore":false,"nextCursor":null}

History