In mathematics, a Heyting algebra (also known as pseudo-Boolean algebra) is a bounded lattice (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). In a Heyting algebra a ⤠b can be found to be equivalent to 1 ⤠a â b; i.e. if a ⤠b then a proves b. From a logical standpoint, A â B is by this definition the weakest proposition for which modus ponens, the inference rule A â B, A ⢠B, is sound. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced in 1930 by Arend Heyting to formalize intuitionistic logic.
Heyting algebras are distributive lattices. Every Boolean algebra is a Heyting algebra when a â b is defined as ìa ⨠b, as is every complete distributive lattice satisfying a one-sided infinite distributive law when a â b is taken to be the supremum of the set of all c for which c ⧠a ⤠b. In the finite case, every nonempty distributive lattice, in particular every nonempty finite chain, is automatically complete and completely distributive, and hence a Heyting algebra.
It follows from the definition that 1 ⤠0 â a, corresponding to the intuition that any proposition a is implied by a contradiction 0. Although the negation operation ìa is not part of the definition, it is definable as a â 0. The intuitive content of ìa is the proposition that to assume a would lead to a contradiction. The definition implies that a ⧠ìa = 0. It can further be shown that a ⤠ììa, although the converse, ììa ⤠a, is not true in general, that is, double negation elimination does not hold in general in a Heyting algebra.
Heyting algebras generalize Boolean algebras in the sense that Boolean algebras are precisely the Heyting algebras satisfying a ⨠ìa = 1 (excluded middle), equivalently ììa = a. Those elements of a Heyting algebra H of the form ìa comprise a Boolean lattice, but in general this is not a subalgebra of H (see below).
Heyting algebras serve as the algebraic models of propositional intuitionistic logic in the same way Boolean algebras model propositional classical logic. The internal logic of an elementary topos is based on the Heyting algebra of subobjects of the terminal object 1 ordered by inclusion, equivalently the morphisms from 1 to the subobject classifier é.
The open sets of any topological space form a complete Heyting algebra. Complete Heyting algebras thus become a central object of study in pointless topology.
Every Heyting algebra whose set of non-greatest elements has a greatest element (and forms another Heyting algebra) is subdirectly irreducible, whence every Heyting algebra can be made subdirectly irreducible by adjoining a new greatest element. It 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. Hence no finite set of finite Heyting algebras can supply all the counterexamples to non-laws of Heyting algebra. This 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 decision method. Nevertheless, it is decidable whether an equation holds of all Heyting algebras.
Heyting 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.
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 pseudo-complement 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 pseudo-complement ìa of any element a by setting ìa = (aâÂÂ0). By definition, , and ìa is the largest element having this property. However, it is not in general true that , thus ì is only a pseudo-complement, 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<sub>1</sub> 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.
A Heyting algebra is a bounded lattice that has all exponential objects.
The lattice is regarded as a category where meet, , is the product. The exponential condition means that for any objects and in an exponential uniquely exists as an object in .
A Heyting implication (often written using or to avoid confusions such as the use of to indicate a functor) is just an exponential: is an alternative notation for . From the definition of exponentials we have that implication () is right adjoint to meet (). This adjunction can be written as or more fully as:
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 every mapping f<sub>a</sub> is the lower adjoint of a monotone Galois connection. In this case the respective upper adjoint g<sub>a</sub> is given by g<sub>a</sub>(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 equation 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 as meaning, intuitively, "provably true". Compare with the axioms at Intuitionistic logic.
Given a set A with three binary operations âÂÂ, ⧠and â¨, and two distinguished elements and , then A is a Heyting algebra for these operations (and the relation ⤠defined by the condition that when aâÂÂb = ) if and only if the following conditions hold for any elements x, y and z of A:
Finally, we define ìx to be xâ .
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.
<ul> <li> Every Boolean algebra is a Heyting algebra, with pâÂÂq given by ìpâ¨q.</li> <li> Every totally ordered set that has a least element 0 and a greatest element 1 is a Heyting algebra (if viewed as a lattice). In this case pâÂÂq equals to 1 when pâ¤q, and q otherwise.</li> <li> The simplest Heyting algebra that is not already a Boolean algebra is the totally ordered set {0, , 1} (viewed as a lattice), yielding the operations:
In this example, note that falsifies the law of excluded middle.
<li> Every topology provides a complete Heyting algebra in the form of its open set lattice. In this case, the element AâÂÂB is the interior of the union of A<sup>c</sup> and B, where A<sup>c</sup> denotes the complement of the open set A. Not all complete Heyting algebras are of this form. These issues are studied in pointless topology, where complete Heyting algebras are also called frames or locales. <li> Every interior algebra provides a Heyting algebra in the form of its lattice of open elements. Every 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 in this Boolean algebra. <li> The Lindenbaum algebra of propositional intuitionistic logic is a Heyting algebra.</li> <li> The global elements of the subobject classifier é of an elementary topos form a Heyting algebra; it is the Heyting algebra of truth values of the intuitionistic higher-order logic induced by the topos. More generally, the set of subobjects of any object X in a topos forms a Heyting algebra.</li> <li> à ÂukasiewiczâÂÂMoisil algebras (LM<sub>n</sub>) are also Heyting algebras for any n (but they are not MV-algebras for n âÂÂ¥ 5). </ul>
The ordering on a Heyting algebra H can be recovered from the operation â as follows: for any elements a, b of H, if and only if aâÂÂb = 1.
In contrast to some many-valued 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 one-element Heyting algebra.
Given 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:
The metaimplication that the first implies the second, which we'll write as , 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 if and only if aâÂÂb = 1, it follows from that whenever a formula FâÂÂG is provably true, we have for any Heyting algebra H, and any elements . (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.
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 Hilbert-style ones given at Intuitionistic logic#Axiomatization. Then the facts to be verified follow immediately from the axiom-like 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 is not provable, it is enough to exhibit a Heyting algebra H and elements such that .
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 .
For more on the metaimplication 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 pseudo-complements. 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 pseudo-complement 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 in 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 is equal to
The regular (respectively complemented) elements of any Heyting algebra H constitute a Boolean algebra H<sub>reg</sub> (respectively H<sub>comp</sub>), in which the operations â§, ì and âÂÂ, as well as the constants 0 and 1, coincide with those of H. In the case of H<sub>comp</sub>, the operation ⨠is also the same, hence H<sub>comp</sub> is a subalgebra of H. In general however, H<sub>reg</sub> will not be a subalgebra of H, because its join operation â¨<sub>reg</sub> may be different from â¨. For we have See below for necessary and sufficient conditions in order for â¨<sub>reg</sub> 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 â¨<sub>reg</sub> on the Boolean algebra H<sub>reg</sub> of regular elements of H coincides with the operation ⨠of H. Condition 7 states that every regular element is complemented, i.e., H<sub>reg</sub> = H<sub>comp</sub>.
We prove the equivalence. Clearly the metaimplications and are trivial. Furthermore, and result simply from the first De Morgan law and the definition of regular elements. We show that by taking ìx and ììx in place of x and y in 6 and using the identity Notice that follows from the first De Morgan law, and results from the fact that the join operation ⨠on the subalgebra H<sub>comp</sub> is just the restriction of ⨠to H<sub>comp</sub>, taking into account the characterizations we have given of conditions 6 and 7. The metaimplication 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<sub>1</sub> and H<sub>2</sub> and a mapping we say that ÃÂ is a morphism of Heyting algebras if, for any elements x and y in H<sub>1</sub>, we have:
It follows from any of the last three conditions (2, 3, or 4) that f is an increasing function, that is, that whenever .
Assume H<sub>1</sub> and H<sub>2</sub> are structures with operations âÂÂ, â§, ⨠(and possibly ì) and constants 0 and 1, and f is a surjective mapping from H<sub>1</sub> to H<sub>2</sub> with properties 1 through 4 above. Then if H<sub>1</sub> is a Heyting algebra, so too is H<sub>2</sub>. 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 from any Heyting algebra to itself is a morphism, and the composite of any two morphisms f and g is a morphism. Hence Heyting algebras form a category.
Given a Heyting algebra H and any subalgebra H<sub>1</sub>, the inclusion mapping is a morphism.
For any Heyting algebra H, the map defines a morphism from H onto the Boolean algebra of its regular elements H<sub>reg</sub>. This is not in general a morphism from H to itself, since the join operation of H<sub>reg</sub> may be different from that of H.
Let H be a Heyting algebra, and let 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, Otherwise, F is equal to the set of x in H such that there exist with
If H is a Heyting algebra and F is a filter on H, we define a relation ~ on H as follows: we write whenever and both belong to F. Then ~ is an equivalence relation; we write for the quotient set. There is a unique Heyting algebra structure on such that the canonical surjection becomes a Heyting algebra morphism. We call the Heyting algebra 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 be a morphism of Heyting algebras. The kernel of f, written ker f, is the set It is a filter on H<sub>1</sub>. (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 It is an isomorphism of onto the subalgebra f[H<sub>1</sub>] of H<sub>2</sub>.
The metaimplication 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 axiom-like definition of Heyting algebras, we define ⤠on H<sub>0</sub> 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 (possibly infinite). One obtains in this way the free Heyting algebra on the variables {A<sub>i</sub>}, which we will again denote by H<sub>0</sub>. It is free in the sense that given any Heyting algebra H given together with a family of its elements , there is a unique morphism f:H<sub>0</sub>âÂÂH satisfying f([A<sub>i</sub>])=a<sub>i</sub>. The uniqueness of f is not difficult to see, and its existence results essentially from the metaimplication of the section "Provable identities" above, in the form of its corollary that whenever F and G are provably equivalent formulas, F(ãÂÂa<sub>i</sub>ãÂÂ)=G(ãÂÂa<sub>i</sub>ãÂÂ) for any family of elements ãÂÂa<sub>i</sub>ãÂÂin H.
Given a set of formulas T in the variables {A<sub>i</sub>}, 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<sub>T</sub> the Heyting algebra so obtained. Then H<sub>T</sub> satisfies the same universal property as H<sub>0</sub> above, but with respect to Heyting algebras H and families of elements ãÂÂa<sub>i</sub>ã satisfying the property that J(ãÂÂa<sub>i</sub>ãÂÂ)=1 for any axiom J(ãÂÂA<sub>i</sub>ãÂÂ) in T. (Let us note that H<sub>T</sub>, taken with the family of its elements ãÂÂ[A<sub>i</sub>]ãÂÂ, itself satisfies this property.) The existence and uniqueness of the morphism is proved the same way as for H<sub>0</sub>, except that one must modify the metaimplication in "Provable identities" so that 1 reads "provably true from T," and 2 reads "any elements a<sub>1</sub>, a<sub>2</sub>,..., a<sub>n</sub> in H satisfying the formulas of T."
The Heyting algebra H<sub>T</sub> that we have just defined can be viewed as a quotient of the free Heyting algebra H<sub>0</sub> on the same set of variables, by applying the universal property of H<sub>0</sub> with respect to H<sub>T</sub>, and the family of its elements ãÂÂ[A<sub>i</sub>]ãÂÂ.
Every Heyting algebra is isomorphic to one of the form H<sub>T</sub>. To see this, let H be any Heyting algebra, and let be a family of elements generating H (for example, any surjective family). Now consider the set T of formulas J(ãÂÂA<sub>i</sub>ãÂÂ) in the variables such that J(ãÂÂa<sub>i</sub>ãÂÂ)=1. Then we obtain a morphism f:H<sub>T</sub>âÂÂH by the universal property of H<sub>T</sub>, 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<sub>T</sub> in the variables {A<sub>i</sub>} with respect to the axioms T is just our H<sub>TâªT<sub>1</sub></sub>, where T<sub>1</sub> is the set of all formulas of the form ììFâÂÂF, since the additional axioms of T<sub>1</sub> 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, (Pâ§Q)âÂÂP is, by definition of the pseudo-complement, 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 3-element 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 Curry–Howard 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 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. 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 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).
The problem of whether a given equation holds in every Heyting algebra was shown to be decidable by Saul Kripke in 1965. The precise computational complexity of the problem was established by Richard Statman in 1979, who showed it was PSPACE-complete and hence at least as hard as deciding equations of Boolean algebra (shown coNP-complete in 1971 by Stephen Cook) and conjectured to be considerably harder. The elementary or first-order theory of Heyting algebras is undecidable. It remains open whether the universal Horn theory of Heyting algebras, or uniform word problem, is decidable. Regarding 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.
Every Heyting algebra is naturally isomorphic to a bounded sublattice of open sets of a topological space , where the implication of is given by the interior of . More precisely, is the spectral space of prime ideals of the bounded lattice and is the lattice of open and quasi-compact subsets of .
More generally, the category of Heyting algebras is dually equivalent to the category of Heyting spaces. This duality can be seen as restriction of the classical Stone duality of bounded distributive lattices to the (non-full) subcategory of Heyting algebras.
Alternatively, the category of Heyting algebras is dually equivalent to the category of Esakia spaces. This is called Esakia duality.