Heyting algebra


A Heyting lattice L is a Brouwerian lattice with a bottom element 0. Equivalently, L is Heyting iff it is relatively pseudocomplemented and pseudocomplemented iff it is bounded and relatively pseudocomplemented.

Let a* denote the pseudocomplement of a and ab the pseudocomplement of a relative to b. Then we have the following properties:

  1. 1.

    a*=a0 (equivalence of definitions)

  2. 2.

    1*=0 (if c=10, then c=c10 by the definition of .)

  3. 3.

    a*=1 iff a=0 (1=a0 implies that ca0 whenever c1. In particular a1, so a=aa0 or a=0. On the other hand, if a=0, then a*=0*=00=1.)

  4. 4.

    aa** and a*=a*** (already true in any pseudocomplemented lattice)

  5. 5.

    a*ab (since a*a=0b)

  6. 6.

    (ab)(ab*)=a*

    Proof.

    If ca=0, then cab so c(ab), and c(ab*) likewise, so c(ab)(ab*). This means precisely that a*=(ab)(ab*). ∎

  7. 7.

    abb*a* (since (ab)b*(ab)(ab*)=a*)

  8. 8.

    a*bab (since bab and a*a=0b)

Note that in property 4, aa**, whereas a**a is in general not true, contrasting with the equality a=a′′ in a Boolean lattice, where is the complementPlanetmathPlanetmath operator. It is easy to see that if a**a for all a in a Heyting lattice L, then L is a Boolean lattice. In this case, the pseudocomplement coincides with the complement of an element a*=a, and we have the equality in property 7: a*b=ab, meaning that the concept of relative pseudocomplementation (http://planetmath.org/RelativelyPseudocomplemented) coincides with the material implication in classical propositional logicPlanetmathPlanetmath.

A Heyting algebra is a Heyting lattice H such that is a binary operator on H. A Heyting algebra homomorphismPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath between two Heyting algebras is a lattice homomorphismMathworldPlanetmath that preserves 0,1, and . In addition, if f is a Heyting algebra homomorphism, f preserves psudocomplementation: f(a*)=f(a0)=f(a)f(0)=f(a)0=f(a)*.

Remarks.

  • In the literature, the assumptionPlanetmathPlanetmath that a Heyting algebra contains 0 is sometimes dropped. Here, we call it a Brouwerian lattice instead.

  • Heyting algebras are useful in modeling intuitionistic logicMathworldPlanetmath. Every intuitionistic propositional logic can be modelled by a Heyting algebra, and every intuitionistic predicate logic can be modelled by a complete Heyting algebra.

Title Heyting algebra
Canonical name HeytingAlgebra
Date of creation 2013-03-22 16:33:03
Last modified on 2013-03-22 16:33:03
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 20
Author CWoo (3771)
Entry type Definition
Classification msc 06D20
Classification msc 03G10
Synonym pseudo-Boolean algebra
Related topic QuantumTopos
Related topic LatticeMathworldPlanetmath
Defines Heyting lattice