Heyting algebra
A Heyting lattice is a Brouwerian lattice with a bottom element . Equivalently, is Heyting iff it is relatively pseudocomplemented and pseudocomplemented iff it is bounded and relatively pseudocomplemented.
Let denote the pseudocomplement of and the pseudocomplement of relative to . Then we have the following properties:
-
1.
(equivalence of definitions)
-
2.
(if , then by the definition of .)
-
3.
iff ( implies that whenever . In particular , so or . On the other hand, if , then .)
-
4.
and (already true in any pseudocomplemented lattice)
-
5.
(since )
-
6.
Proof.
If , then so , and likewise, so . This means precisely that . ∎
-
7.
(since
-
8.
(since and )
Note that in property 4, , whereas is in general not true, contrasting with the equality 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 |