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 a→b the pseudocomplement of a relative to b. Then we have the following properties:

  1. 1.

    a*=a→0 (equivalence of definitions)

  2. 2.

    1*=0 (if c=1→0, then c=c∧1≤0 by the definition of →.)

  3. 3.

    a*=1 iff a=0 (1=a→0 implies that c∧a≤0 whenever c≤1. In particular a≤1, so a=a∧a≤0 or a=0. On the other hand, if a=0, then a*=0*=0→0=1.)

  4. 4.

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

  5. 5.

    a*≤a→b (since a*∧a=0≤b)

  6. 6.

    (a→b)∧(a→b*)=a*

    Proof.

    If c∧a=0, then c∧a≤b so c≤(a→b), and c≤(a→b*) likewise, so c≤(a→b)∧(a→b*). This means precisely that a*=(a→b)∧(a→b*). ∎

  7. 7.

    a→b≤b*→a* (since (a→b)∧b*≤(a→b)∧(a→b*)=a*)

  8. 8.

    a*∨b≤a→b (since b∧a≤b and a*∧a=0≤b)

Note that in property 4, a≤a**, 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=a→b, 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(a→0)=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