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 called implication such that is equivalent to In a Heyting algebra can be found to be equivalent to i.e. if then a proves b. From a logical standpoint, is by this definition the weakest proposition for which modus ponens, the inference rule , 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 (non-contradiction). 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.
Formal definition 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 H1 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.
Alternative definitions Category-theoretic definition 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 confusion with the use of to indicate a morphism) 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:
Lattice-theoretic definitions 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 fa is the lower adjoint of a monotone Galois connection. In this case the respective upper adjoint ga is given by ga(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.
Bounded lattice with an implication operation 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 →.
Characterization using the axioms of intuitionistic logic 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 ) if and only if the following conditions hold for any elements x, y and z of A:
Finally, we define ¬x to be .
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.
Examples
Every Boolean algebra is a Heyting algebra, with p→q given by ¬p∨q. 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> 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: + 0 1 0 0 0 0 0 1 0 1 + 0 1 0 0 1 1 1 1 1 1 + 0 1 0 1 1 1 0 1 1 1 0 1 a ¬a 0 1 0 1 0 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 Ac and B, where Ac 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. The Lindenbaum algebra of propositional intuitionistic logic is a Heyting algebra. 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> Łukasiewicz–Moisil algebras (LMn) are also Heyting algebras for any n, Theorem 3.6 (but they are not MV-algebras for n ≥ 5Iorgulescu, A.: Connections between MVn-algebras and n-valued Łukasiewicz–Moisil algebras—I. Discrete Math. 181, 155–177 (1998) ).
Properties
General properties 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.
Provable identities 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 formula F is provably true in intuitionist propositional calculus. The identity is true for any Heyting algebra H and any elements . 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.
Distributivity Heyting algebras are always distributive. Specifically, we always have the identities