You are here
Home ›Heyting algebra
Primary tabs
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 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.
Mathematics Subject Classification
06D20 Heyting algebras03G10 Lattices and related structures
- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)
- Other useful stuff
Recent Activity
new question: Linear Algebra Combination Problem! by Bruce Lee
new question: Computation of $\varphi(2000)$ by jeremyboden
new question: Computation of $\varphi(2000)$ by jeremyboden
May 21
new question: pure subgroups by lvoyster
new correction: Typo in M\"obius function? by Aleph Zero
new collection: analytic number theory by Aleph Zero
May 20
new question: Taylor's Series Query! by unlord
new question: Laplace transform by J
new question: Residue Calculus by J
May 19
new Education: Project: PlanetMath Outlines Series by unlord


