In mathematics, Heyting algebras are special partially ordered sets that constitute a generalization of Boolean algebras, named after Arend Heyting. Heyting algebras arise as models of intuitionistic logic, a logic in which the law of excluded middle does not in general hold. Complete Heyting algebras are a central object of study in pointless topology.
Contents 
A Heyting algebra H is a bounded lattice such that for all a and b in H there is a greatest element x of H such that
This element is the relative pseudocomplement of a with respect to b, and is denoted a → b. We write 1 and 0 for the largest and the smallest element of H, respectively.
In any Heyting algebra, one defines the pseudocomplement ¬x of any element x by setting ¬x = (x → 0). By definition, a ∧ ¬a = 0, and ¬a is the largest element having this property. However, it is not in general true that a ∨ ¬a = 1, thus ¬ is only a pseudocomplement, not a true complement, as would be the case in a Boolean algebra.
A complete Heyting algebra is a Heyting algebra that is a complete lattice.
A subalgebra of a Heyting algebra H is a subset H_{1} of H containing 0 and 1 and closed under the operations ∧, ∨ and →. It follows that it is also closed under ¬. A subalgebra is made into a Heyting algebra by the induced operations.
An equivalent definition of Heyting algebras can be given by considering the mappings
for some fixed a in H. A bounded lattice H is a Heyting algebra if and only if all mappings ƒ_{a} are the lower adjoint of a monotone Galois connection. In this case the respective upper adjoints g_{a} are given by g_{a}(x) = a → x, where → is defined as above.
Yet another definition is as a residuated lattice whose monoid operation is ∧. The monoid unit must then be the top element 1. Commutativity of this monoid implies that the two residuals coincide as a → b.
Given 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:
where 4 is the distributive law for →.
This characterization of Heyting algebras makes the proof of the basic facts concerning the relationship between intuitionist propositional calculus and Heyting algebras immediate. (For these facts, see the sections "Provable identities" and "Universal constructions.") One should think of the element 1 as meaning, intuitively, "provably true." Compare with the axioms at Intuitionistic logic#Axiomatization.
Given a set A with three binary operations →, ∧ and ∨, and two distinguished elements 0 and 1, then A is a Heyting algebra for these operations (and the relation ≤ defined by the condition that a ≤ b when a → b = 1) if and only if the following conditions hold for any elements x, y and z of A:
Finally, we define ¬x to be x → 0.
Condition 1 says that equivalent formulas should be identified. Condition 2 says that provably true formulas are closed under modus ponens. Conditions 3 and 4 are then conditions. Conditions 5, 6 and 7 are and conditions. Conditions 8, 9 and 10 are or conditions. Condition 11 is a false condition.
Of course, if a different set of axioms were chosen for logic, we could modify ours accordingly.
The ordering ≤ on a Heyting algebra H can be recovered from the operation → as follows: for any elements a, b of H, a ≤ b if and only if a → b = 1.
In contrast to some manyvalued logics, Heyting algebras share the following property with Boolean algebras: if negation has a fixed point (i.e. ¬a = a for some a), then the Heyting algebra is the trivial oneelement Heyting algebra.
Given a formula F(A_{1}, A_{2},…, A_{n}) 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:
The implication 1 → 2 is extremely useful and is the principal practical method for proving identities in Heyting algebras. In practice, one frequently uses the deduction theorem in such proofs.
Since for any a and b in a Heyting algebra H we have a ≤ b if and only if a → b = 1, it follows from 1 → 2 that whenever a formula a formula F → G is provably true, we have F(a_{1}, a_{2},…, a_{n}) ≤ G(a_{1}, a_{2},…, a_{n}) for any Heyting algebra H, and any elements a_{1}, a_{2},…, a_{n} ∈ H. (It follows from the deduction theorem that F → G is provable [from nothing] if and only if G is a provable from F, that is, if G is a provable consequence of F.) In particular, if F and G are provably equivalent, then F(a_{1}, a_{2},…, a_{n}) = G(a_{1}, a_{2},…, a_{n}), since ≤ is an order relation.
1 → 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. For example, let us choose the system of proof having modus ponens as its sole rule of inference, and whose axioms are the Hilbertstyle ones given at Intuitionistic logic#Axiomatization. Then the facts to be verified follow immediately from the axiomlike definition of Heyting algebras given above.
1 → 2 also provides a method for proving that certain propositional formulas, though tautologies in classical logic, cannot be proved in intuitionist propositional logic. In order to prove that some formula F(A_{1}, A_{2},…, A_{n}) is not provable, it is enough to exhibit a Heyting algebra H and elements a_{1}, a_{2},..., a_{n} ∈ H such that F(a_{1}, a_{2},…, a_{n}) ≠ 1.
If 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 (a ∧ b) → c = a → (b → c).
For more on the implication 2 → 1, see the section "Universal constructions" below.
Heyting algebras are always distributive. Specifically, we always have the identities
The distributive law is sometimes stated as an axiom, but in fact it follows from the existence of relative pseudocomplements. The reason is that, being the lower adjoint of a Galois connection, preserves all existing suprema. Distributivity in turn is just the preservation of binary suprema by ∧.
By a similar argument, the following infinite distributive law holds in any complete Heyting algebra:
for any element x in H and any subset Y of H. Conversely, any complete lattice satisfying the above infinite distributive law is a complete Heyting algebra, with
being its relative pseudocomplement operation.
An element x of a Heyting algebra H is called regular if either of the following equivalent conditions hold:
The equivalence of these conditions can be restated simply as the identity ¬¬¬x = ¬x, valid for all x ∈ H.
Elements x and y of a Heyting algebra H are called complements to each other if x ∧ y = 0 and x ∨ y = 1. If it exists, any such y is unique and must in fact be equal to ¬x. We call an element x complemented if it admits a complement. It is true that if x is complemented, then so is ¬x, and then x and ¬x are complements to each other. However, confusingly, even if x is not complemented, ¬x may nonetheless have a complement (not equal to x). In any Heyting algebra, the elements 0 and 1 are complements to each other. For 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.
Any complemented element of a Heyting algebra is regular, though the converse is not true in general. In particular, 0 and 1 are always regular.
For any Heyting algebra H, the following conditions are equivalent:
In this case, the element a → b is equal to ¬a ∨ b.
The regular (resp. complemented) elements of any Heyting algebra H constitute a Boolean algebra H_{reg} (resp. H_{comp}), in which the operations ∧, ¬ and →, as well as the constants 0 and 1, coincide with those of H. In the case of H_{comp}, the operation ∨ is also the same, hence H_{comp} is a subalgebra of H. In general however, H_{reg} will not be a subalgebra of H, because its join operation ∨_{reg} may be differ from ∨. For x, y ∈ H_{reg}, we have x ∨_{reg} y = ¬(¬x ∧ ¬ y). See below for necessary and sufficient conditions in order for ∨_{reg} to coincide with ∨.
One of the two De Morgan laws is satisfied in every Heyting algebra, namely
However, the other De Morgan law does not always hold. We have instead a weak de Morgan law:
The following statements are equivalent for all Heyting algebras H:
Condition 2 is the other De Morgan law. Condition 6 says that the join operation ∨_{reg} on the Boolean algebra H_{reg} of regular elements of H coincides with the operation ∨ of H. Condition 7 states that every regular element is complemented, i.e., H_{reg} = H_{comp}.
We prove the equivalence. Clearly 1 → 2, 2 → 3 and 4 → 5 are trivial. Furthermore, 3 ↔ 4 and 5 ↔ 6 result simply from the first De Morgan law and the definition of regular elements. We show that 6 → 7 by taking ¬x and ¬¬x in place of x and y in 6 and using the identity a ∧ ¬a = 0. Notice that 2 → 1 follows from the first De Morgan law, and 7 → 6 results from the fact that the join operation ∨ on the subalgebra H_{comp} is just the restriction of ∨ to H_{comp}, taking into account the characterizations we have given of conditions 6 and 7. The implication 5 → 2 is a trivial consequence of the weak De Morgan law, taking ¬x and ¬y in place of x and y in 5.
Heyting algebras satisfying the above properties are related to De Morgan logic in the same way Heyting algebras in general are related to intuitionist logic.
Given two Heyting algebras H_{1} and H_{2} and a mapping ƒ : H_{1} → H_{2}, we say that ƒ is a morphism of Heyting algebras if, for any elements x and y in H_{1}, we have:
We put condition 6 in brackets because it follows from the others, as ¬x is just x→0, and one may or may not wish to consider ¬ to be a basic operation.
It follows from conditions 3 and 5 (or 1 alone, or 2 alone) that f is an increasing function, that is, that f(x) ≤ f(y) whenever x ≤ y.
Assume H_{1} and H_{2} are structures with operations →, ∧, ∨ (and possibly ¬) and constants 0 and 1, and f is a surjective mapping from H_{1} to H_{2} with properties 1 through 5 (or 1 through 6) above. Then if H_{1} is a Heyting algebra, so too is H_{2}. This 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.
The identity map ƒ(x) = x from any Heyting algebra to itself is a morphism, and the composite g ∘ ƒ of any two morphisms ƒ and g is a morphism. Hence Heyting algebras form a category.
Given a Heyting algebra H and any subalgebra H_{1}, the inclusion mapping i : H_{1} → H is a morphism.
For any Heyting algebra H, the map x ↦ ¬¬x defines a morphism from H onto the Boolean algebra of its regular elements H_{reg}. This is not in general a morphism from H to itself, since the join operation of H_{reg} may be different from that of H.
Let H be a Heyting algebra, and let F ⊆ H. We call F a filter on H if it satisfies the following properties:
The intersection of any set of filters on H is again a filter. Therefore, given any subset S of H there is a smallest filter containing S. We call it the filter generated by S. If S is empty, F = {1}. Otherwise, F is equal to the set of x in H such that there exist y_{1}, y_{2}, …, y_{n} ∈ S with y_{1} ∧ y_{2} ∧ … ∧ y_{n} ≤ x.
If 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. Then ∼ is an equivalence relation; we write H/F for the quotient set. There is a unique Heyting algebra structure on H/F such that the canonical surjection p_{F} : H → H/F becomes a Heyting algebra morphism. We call the Heyting algebra H/F the quotient of H by F.
Let S be a subset of a Heyting algebra H and let F be the filter generated by S. Then H/F satisfies the following universal property:
Let f : H_{1} → H_{2} be a morphism of Heyting algebras. The kernel of ƒ, written ker ƒ, is the set ƒ^{−1}[{1}]. It is a filter on H_{1}. (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, ƒ induces a morphism ƒ′ : H_{1}/(ker ƒ) → H_{2}. It is an isomorphism of H_{1}/(ker ƒ) onto the subalgebra ƒ[H_{1}] of H_{2}.
The implication 2→1 in the section "Provable identities" is proved by showing that the result of the following construction is itself a Heyting algebra:
As always under the axiomlike definition of Heyting algebras, we define ≤ on H_{0} by the condition that x≤y if and only if x→y=1. Since, by the 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. In other words, ≤ is the order relation on L/∼ induced by the preorder ≼ on L.
In fact, the preceding construction can be carried out for any set of variables {A_{i}: i∈I} (possibly infinite). One obtains in this way the free Heyting algebra on the variables {A_{i}}, which we will again denote by H_{0}. It is free in the sense that given any Heyting algebra H given together with a family of its elements 〈a_{i}: i∈I 〉, there is a unique morphism f:H_{0}→H satisfying f([A_{i}])=a_{i}. The uniqueness of f is not difficult to see, and its existence results essentially from the implication 1→2 of the section "Provable identities" above, in the form of its corollary that whenever F and G are provably equivalent formulas, F(〈a_{i}〉)=G(〈a_{ i}〉) for any family of elements 〈a_{i}〉in H.
Given a set of formulas T in the variables {A_{i}}, 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. Let us denote by H_{T} the Heyting algebra so obtained. Then H_{T} satisfies the same universal property as H_{0} above, but with respect to Heyting algebras H and families of elements 〈a_{i}〉 satisfying the property that J(〈a_{i}〉)=1 for any axiom J(〈A_{i}〉) in T. (Let us note that H_{T}, taken with the family of its elements 〈[A_{i}]〉, itself satisfies this property.) The existence and uniqueness of the morphism is proved the same way as for H_{0}, except that one must modify the implication 1→2 in "Provable identities" so that 1 reads "provably true from T," and 2 reads "any elements a_{1}, a_{2},..., a_{n} in H satisfying the formulas of T."
The Heyting algebra H_{T} that we have just defined can be viewed as a quotient of the free Heyting algebra H_{0} on the same set of variables, by applying the universal property of H_{0} with respect to H_{T}, and the family of its elements 〈[A_{i}]〉.
Every Heyting algebra is isomorphic to one of the form H_{T}. To see this, let H be any Heyting algebra, and let 〈a_{i}: i∈I〉 be a family of elements generating H (for example, any surjective family). Now consider the set T of formulas J(〈A_{i}〉) in the variables 〈A_{i}: i∈I〉 such that J(〈a_{i}〉)=1. Then we obtain a morphism f:H_{T}→H by the universal property of H_{T}, which is clearly surjective. It is not difficult to show that f is injective.
The constructions we have just given play an entirely analogous role with respect to Heyting algebras to that of Lindenbaum algebras with respect to Boolean algebras. In fact, The Lindenbaum algebra B_{T} in the variables {A_{i}} with respect to the axioms T is just our H_{T∪T}1, where T_{1} is the set of all formulas of the form ¬¬F→F, since the additional axioms of T_{1} are the only ones that need to be added in order to make all classical tautologies provable.
If 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. For instance, is, by definition of the pseudocomplement, the largest element x such that . This inequation is satisfied for any x, so the largest such x is 1.
Furthermore the rule of modus ponens allows us to derive the formula Q from the formulas P and P → Q. But 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.
This 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. However one can construct a Heyting algebra in which the value of Peirce's law is not always 1. Consider the 3element algebra {0,½,1} as given above. If we assign ½ to P and 0 to Q, then the value of Peirce's law ((P → Q) → P) → P is ½. It follows that Peirce's law cannot be intuitionistically derived. See CurryHoward isomorphism for the general context of what this implies in type theory.
The 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. This is similar to the notion that classically valid formulas are those formulas that have a value of 1 in the twoelement Boolean algebra under any possible assignment of true and false to the formula's variables — that is, they are formulas which are tautologies in the usual truthtable sense. A 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'. The usual twovalued logic system is a special case of a Heyting algebra, and the smallest nontrivial one, in which the only elements of the algebra are 1 (true) and 0 (false).
The word problem on free Heyting algebras is difficult.^{[3]} The only known results are that the free Heyting algebra on one generator is infinite, and that the free complete Heyting algebra on one generator exists (and has one more element than the free Heyting algebra).
