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.
a*=a→0 (equivalence of definitions)
-
2.
1*=0 (if c=1→0, then c=c∧1≤0 by the definition of →.)
-
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.
a≤a** and a*=a*** (already true in any pseudocomplemented lattice)
-
5.
a*≤a→b (since a*∧a=0≤b)
-
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.
a→b≤b*→a* (since (a→b)∧b*≤(a→b)∧(a→b*)=a*)
-
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 complement operator. It is easy to see that if for all in a Heyting lattice , then is a Boolean lattice. In this case, the pseudocomplement coincides with the complement of an element , and we have the equality in property 7: , meaning that the concept of relative pseudocomplementation (http://planetmath.org/RelativelyPseudocomplemented) coincides with the material implication in classical propositional logic
.
A Heyting algebra is a Heyting lattice such that is a binary operator on . A Heyting algebra homomorphism between two Heyting algebras is a lattice homomorphism
that preserves , and . In addition, if is a Heyting algebra homomorphism, preserves psudocomplementation: .
Remarks.
-
•
In the literature, the assumption
that a Heyting algebra contains is sometimes dropped. Here, we call it a Brouwerian lattice instead.
-
•
Heyting algebras are useful in modeling intuitionistic logic
. 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 | Lattice![]() |
Defines | Heyting lattice |