Heyting algebra

The ordering $\backslash le$ on a Heyting algebra H can be recovered from the operation → as follows: for any elements a, b of H, $a\; \backslash le\; b$ 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 $F(A\_1,\; A\_2,\backslash ldots,\; A\_n)$ of propositional calculus (using, in addition to the variables, the connectives $\backslash land,\; \backslash lor,\; \backslash lnot,\; \backslash to$, 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:

1. The formula F is provably true in intuitionist propositional calculus.
2. The identity $F(a\_1,\; a\_2,\backslash ldots,\; a\_n)\; =\; 1$ is true for any Heyting algebra H and any elements $a\_1,\; a\_2,\backslash ldots,\; a\_n\; \backslash in\; H$.

The metaimplication {{nowrap|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\; \backslash le\; b$ if and only if a→b = 1, it follows from {{nowrap|1 ⇒ 2}} that whenever a formula F→G is provably true, we have $F(a\_1,\; a\_2,\backslash ldots,\; a\_n)\; \backslash le\; G(a\_1,\; a\_2,\backslash ldots,\; a\_n)$ for any Heyting algebra H, and any elements $a\_1,\; a\_2,\backslash ldots,\; a\_n\; \backslash in\; H$. (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 $F(a\_1,\; a\_2,\backslash ldots,\; a\_n)\; =\; G(a\_1,\; a\_2,\backslash ldots,\; 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 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 $F(A\_1,\; A\_2,\backslash ldots,\; A\_n)$ is not provable, it is enough to exhibit a Heyting algebra H and elements $a\_1,\; a\_2,\backslash ldots,\; a\_n\; \backslash in\; H$ such that $F(a\_1,\; a\_2,\backslash ldots,\; a\_n)\; \backslash ne\; 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\; \backslash land\; b)\; \backslash to\; c\; =\; a\; \backslash to\; (b\; \backslash to\; c)$.

For more on the metaimplication 2 ⇒ 1, see the section "Universal constructions" below.

Heyting algebras are always distributive. Specifically, we always have the identities

1. $a\; \backslash wedge\; (b\; \backslash vee\; c)\; =\; (a\; \backslash wedge\; b)\; \backslash vee\; (a\; \backslash wedge\; c)$
2. $a\; \backslash vee\; (b\; \backslash wedge\; c)\; =\; (a\; \backslash vee\; b)\; \backslash wedge\; (a\; \backslash vee\; c)$

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, $\backslash wedge$ preserves all existing suprema. Distributivity in turn is just the preservation of binary suprema by $\backslash wedge$.

By a similar argument, the following infinite distributive law holds in any complete Heyting algebra:

:$x\backslash wedge\backslash bigvee\; Y\; =\; \backslash bigvee\; \backslash \{x\backslash wedge\; y\; \backslash mid\; y\; \backslash in\; Y\backslash \}$

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

:$a\backslash to\; b=\backslash bigvee\backslash \{c\backslash mid\; a\backslash land\; c\backslash le\; b\backslash \}$

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:

1. x = ¬¬x.
2. x = ¬y for some y in H.

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:

1. H is a Boolean algebra;
2. every x in H is regular;Rutherford (1965), Th.26.2 p.78.
3. every x in H is complemented.Rutherford (1965), Th.26.1 p.78.

In this case, the element {{nowrap|1=a→b}} is equal to {{nowrap|1=¬a ∨ b.}}

The regular (respectively complemented) elements of any Heyting algebra H constitute a Boolean algebra H_reg (respectively 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 different from ∨. For {{nowrap|1=x, y ∈ H_reg,}} we have {{nowrap|1=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

:$\backslash forall\; x,y\; \backslash in\; H:\; \backslash qquad\; \backslash lnot(x\; \backslash vee\; y)=\backslash lnot\; x\; \backslash wedge\; \backslash lnot\; y.$

However, the other De Morgan law does not always hold. We have instead a weak de Morgan law:

:$\backslash forall\; x,y\; \backslash in\; H:\; \backslash qquad\; \backslash lnot(x\; \backslash wedge\; y)=\; \backslash lnot\; \backslash lnot\; (\backslash lnot\; x\; \backslash vee\; \backslash lnot\; y).$

The following statements are equivalent for all Heyting algebras H:

1. H satisfies both De Morgan laws,
2. $\backslash lnot(x\; \backslash wedge\; y)=\backslash lnot\; x\; \backslash vee\; \backslash lnot\; y\; \backslash mbox\{\; for\; all\; \}\; x,\; y\; \backslash in\; H,$
3. $\backslash lnot(x\; \backslash wedge\; y)=\backslash lnot\; x\; \backslash vee\; \backslash lnot\; y\; \backslash mbox\{\; for\; all\; regular\; \}\; x,\; y\; \backslash in\; H,$
4. $\backslash lnot\backslash lnot\; (x\; \backslash vee\; y)\; =\; \backslash lnot\backslash lnot\; x\; \backslash vee\; \backslash lnot\backslash lnot\; y\; \backslash mbox\{\; for\; all\; \}\; x,\; y\; \backslash in\; H,$
5. $\backslash lnot\backslash lnot\; (x\; \backslash vee\; y)\; =\; x\; \backslash vee\; y\; \backslash mbox\{\; for\; all\; regular\; \}\; x,\; y\; \backslash in\; H,$
6. $\backslash lnot(\backslash lnot\; x\; \backslash wedge\; \backslash lnot\; y)\; =\; x\; \backslash vee\; y\; \backslash mbox\{\; for\; all\; regular\; \}\; x,\; y\; \backslash in\; H,$
7. $\backslash lnot\; x\; \backslash vee\; \backslash lnot\backslash lnot\; x\; =\; 1\; \backslash mbox\{\; for\; all\; \}\; x\; \backslash in\; 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 the metaimplications {{nowrap|1 ⇒ 2,}} {{nowrap|2 ⇒ 3}} and {{nowrap|4 ⇒ 5}} are trivial. Furthermore, {{nowrap|3 ⇔ 4}} and {{nowrap|5 ⇔ 6}} result simply from the first De Morgan law and the definition of regular elements. We show that {{nowrap|6 ⇒ 7}} by taking ¬x and ¬¬x in place of x and y in 6 and using the identity {{nowrap|a ∧ ¬a {{=}} 0.}} Notice that {{nowrap|2 ⇒ 1}} follows from the first De Morgan law, and {{nowrap|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 metaimplication {{nowrap|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₁ and H₂ and a mapping {{nowrap|1=f : H₁ → H₂,}} we say that ƒ is a morphism of Heyting algebras if, for any elements x and y in H₁, we have:

1. $f(0)\; =\; 0,$
2. $f(x\; \backslash land\; y)\; =\; f(x)\; \backslash land\; f(y),$
3. $f(x\; \backslash lor\; y)\; =\; f(x)\; \backslash lor\; f(y),$
4. $f(x\; \backslash to\; y)\; =\; f(x)\; \backslash to\; f(y),$

It follows from any of the last three conditions (2, 3, or 4) that f is an increasing function, that is, that {{nowrap|1=f(x) ≤ f(y)}} whenever {{nowrap|1=x ≤ y}}.

Assume H₁ and H₂ are structures with operations →, ∧, ∨ (and possibly ¬) and constants 0 and 1, and f is a surjective mapping from H₁ to H₂ with properties 1 through 4 above. Then if H₁ is a Heyting algebra, so too is H₂. 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 {{nowrap|1=f(x) = x}} from any Heyting algebra to itself is a morphism, and the composite {{nowrap|1=g ∘ f}} 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₁, the inclusion mapping {{nowrap|1=i : H₁ → H}} is a morphism.

For any Heyting algebra H, the map {{nowrap|1=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 {{nowrap|1=F ⊆ H.}} We call F a filter on H if it satisfies the following properties:

1. $1\; \backslash in\; F,$
2. $\backslash mbox\{If\; \}\; x,y\; \backslash in\; F\; \backslash mbox\{\; then\; \}\; x\; \backslash land\; y\; \backslash in\; F,$
3. $\backslash mbox\{If\; \}\; x\; \backslash in\; F,\; \backslash \; y\; \backslash in\; H,\; \backslash \; \backslash mbox\{and\; \}\; x\; \backslash le\; y\; \backslash mbox\{\; then\; \}\; y\; \backslash in\; F.$

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, {{nowrap|1=F = {1}.}} Otherwise, F is equal to the set of x in H such that there exist {{nowrap|1=y₁, y₂, ..., y_n ∈ S}} with {{nowrap|1=y₁ ∧ y₂ ∧ ... ∧ 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 {{nowrap|1=x ~ y}} whenever {{nowrap|1=x → y}} and {{nowrap|1=y → x}} both belong to F. Then ~ is an equivalence relation; we write {{nowrap|1=H/F}} for the quotient set. There is a unique Heyting algebra structure on {{nowrap|1=H/F}} such that the canonical surjection {{nowrap|1=p_F : H → H/F}} becomes a Heyting algebra morphism. We call the Heyting algebra {{nowrap|1=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:

:Given any morphism of Heyting algebras {{nowrap|1=f : H → {{prime|H}}}} satisfying {{nowrap|1=f(y) = 1}} for every {{nowrap|1=y ∈ S,}} f factors uniquely through the canonical surjection {{nowrap|1=p_F : H → H/F.}} That is, there is a unique morphism {{nowrap|1={{prime|f}} : H/F → {{prime|H}}}} satisfying {{nowrap|1={{prime|f}}p_F = f.}} The morphism {{prime|f}} is said to be induced by f.

Let {{nowrap|1=f : H₁ → H₂}} be a morphism of Heyting algebras. The kernel of f, written ker f, is the set {{nowrap|1=f⁻¹[{1}].}} It is a filter on H₁. (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 {{nowrap|1={{prime|f}} : H₁/(ker f) → H₂.}} It is an isomorphism of {{nowrap|1=H₁/(ker f)}} onto the subalgebra f[H₁] of H₂.

The metaimplication {{nowrap|2 ⇒ 1}} in the section "Provable identities" is proved by showing that the result of the following construction is itself a Heyting algebra:

1. Consider the set L of propositional formulas in the variables A₁, A₂,..., A_n.
2. Endow L with a preorder ≼ by defining F≼G if G is an (intuitionist) logical consequence of F, that is, if G is provable from F. It is immediate that ≼ is a preorder.
3. Consider the equivalence relation F~G induced by the preorder F≼G. (It is defined by F~G if and only if F≼G and G≼F. In fact, ~ is the relation of (intuitionist) logical equivalence.)
4. Let H₀ be the quotient set L/~. This will be the desired Heyting algebra.
5. We write [F] for the equivalence class of a formula F. Operations →, ∧, ∨ and ¬ are defined in an obvious way on L. Verify that given formulas F and G, the equivalence classes [F→G], [F∧G], [F∨G] and [¬F] depend only on [F] and [G]. This defines operations →, ∧, ∨ and ¬ on the quotient set H₀=L/~. Further define 1 to be the class of provably true statements, and set 0=[⊥].
6. Verify that H₀, together with these operations, is a Heyting algebra. We do this using the axiom-like definition of Heyting algebras. H₀ satisfies conditions THEN-1 through FALSE because all formulas of the given forms are axioms of intuitionist logic. MODUS-PONENS follows from the fact that if a formula ⊤→F is provably true, where ⊤ is provably true, then F is provably true (by application of the rule of inference modus ponens). Finally, EQUIV results from the fact that if F→G and G→F are both provably true, then F and G are provable from each other (by application of the rule of inference modus ponens), hence [F]=[G].

As always under the axiom-like definition of Heyting algebras, we define ≤ on H₀ 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₀. 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₀→H satisfying f([A_i])=a_i. The uniqueness of f is not difficult to see, and its existence results essentially from the metaimplication {{nowrap|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₀ 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₀, except that one must modify the metaimplication {{nowrap|1 ⇒ 2}} in "Provable identities" so that 1 reads "provably true from T," and 2 reads "any elements a₁, a₂,..., 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₀ on the same set of variables, by applying the universal property of H₀ 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∪T1, where T₁ is the set of all formulas of the form ¬¬F→F, since the additional axioms of T₁ 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 $P\; \backslash land\; Q\; \backslash land\; x\; \backslash le\; P$. 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 $P\; \backslash land\; 1\; \backslash le\; Q$, and so $1\; \backslash land\; 1\; \backslash le\; Q$; 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,{{sfrac|1|2}},1} as given above. If we assign {{sfrac|1|2}} to P and 0 to Q, then the value of Peirce's law ((P→Q)→P)→P is {{sfrac|1|2}}. 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{{cite journal | last1 = Statman | first1 = R. | year = 1979 | title = Intuitionistic propositional logic is polynomial-space complete | journal = Theoretical Comput. Sci. | volume = 9 | pages = 67–72 | doi=10.1016/0304-3975(79)90006-9| hdl = 2027.42/23534 | hdl-access = free }} and hence at least as hard as deciding equations of Boolean algebra (shown coNP-complete in 1971 by Stephen Cook){{Cite conference|last = Cook | first = S.A. | author-link = Stephen A. Cook | title = The complexity of theorem proving procedures

| book-title = Proceedings, Third Annual ACM Symposium on the Theory of Computing, ACM, New York | year = 1971 | pages = 151–158 | doi = 10.1145/800157.805047| doi-access = free}} and conjectured to be considerably harder. The elementary or first-order theory of Heyting algebras is undecidable.{{cite journal | last1 = Grzegorczyk | first1 = Andrzej | author-link = Andrzej Grzegorczyk | year = 1951 | title = Undecidability of some topological theories | url =https://www.impan.pl/shop/publication/transaction/download/product/93826?download.pdf | journal = Fundamenta Mathematicae | volume = 38 | pages = 137–52 | doi = 10.4064/fm-38-1-137-152 }} It remains open whether the universal Horn theory of Heyting algebras, or word problem, is decidable.Peter T. Johnstone, Stone Spaces, (1982) Cambridge University Press, Cambridge, {{ISBN|0-521-23893-5}}. (See paragraph 4.11) 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 {{math|H}} is naturally isomorphic to a bounded sublattice {{math|L}} of open sets of a topological space {{math|X}}, where the implication $U\backslash to\; V$ of {{math|L}} is given by the interior of $(X\backslash setminus\; U)\backslash cup\; V$.

More precisely, {{math|X}} is the spectral space of prime ideals of the bounded lattice {{math|H}} and {{math|L}} is the lattice of open and quasi-compact subsets of {{math|X}}.

More generally, the category of Heyting algebras

is dually equivalent to the category of Heyting spaces.see section 8.3 in * {{cite book | last1=Dickmann | first1=Max | last2=Schwartz | first2= Niels | last3=Tressl | first3= Marcus | title=Spectral Spaces| doi=10.1017/9781316543870 | year=2019 | publisher=Cambridge University Press | series=New Mathematical Monographs | volume=35 | location=Cambridge | isbn=9781107146723 | s2cid=201542298 }}

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.

{{Reflist}}

• Alexandrov topology
• Superintuitionistic (aka intermediate) logics
• List of Boolean algebra topics
• Ockham algebra

• {{cite book | first = Daniel Edwin | last = Rutherford | year = 1965 | title = Introduction to Lattice Theory | publisher = Oliver and Boyd | oclc = 224572 }}
• F. Borceux, Handbook of Categorical Algebra 3, In Encyclopedia of Mathematics and its Applications, Vol. 53, Cambridge University Press, 1994. {{ISBN|0-521-44180-3}} {{OCLC|52238554}}
• G. Gierz, K.H. Hoffmann, K. Keimel, J. D. Lawson, M. Mislove and D. S. Scott, Continuous Lattices and Domains, In Encyclopedia of Mathematics and its Applications, Vol. 93, Cambridge University Press, 2003.
• S. Ghilardi. Free Heyting algebras as bi-Heyting algebras, Math. Rep. Acad. Sci. Canada XVI., 6:240–244, 1992.
• {{citation|last=Heyting|first= A.

|title=Die formalen Regeln der intuitionistischen Logik. I, II, III|jfm= 56.0823.01

|journal=Sitzungsberichte Akad. Berlin |year=1930|pages= 42–56, 57–71, 158–169 }}

• {{cite book | vauthors=((Mac Lane, S.)), ((Moerdijk, I.)) | date= 1994 | title=Sheaves in Geometry and Logic | series= Universitext | publisher=Springer New York | url=http://dx.doi.org/10.1007/978-1-4612-0927-0 | doi=10.1007/978-1-4612-0927-0| isbn= 978-0-387-97710-2 }}
• {{cite book | last1=Dickmann | first1=Max | last2=Schwartz | first2= Niels | last3=Tressl | first3= Marcus | title=Spectral Spaces| doi=10.1017/9781316543870 | year=2019 | publisher=Cambridge University Press | series=New Mathematical Monographs | volume=35 | location=Cambridge | isbn=9781107146723 | s2cid=201542298 }}

• {{PlanetMath|urlname=heytingalgebra|title=Heyting algebra}}

{{Order theory}}

{{DEFAULTSORT:Heyting Algebra}}

Category:Algebraic logic

Category:Constructivism (mathematics)

Category:Lattice theory