PlanetMath: Heyting algebra

(more info)

Math for the people, by the people.

Main Menu

sections Encyclopædia
Papers
Books
Expositions

meta Requests (192)
Orphanage
Unclass'd
Unproven (496)
Corrections (20)
Classification

talkback Polls
Forums
Feedback
Bug Reports

downloads Snapshots
PM Book

information News
Docs
Wiki
ChangeLog
TODO List
Legalese
About

Entry average rating: No information on entry rating

Heyting algebra

(Definition)

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

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

$a^*=a\to 0$ (equivalence of definitions)
(if $c=1\to 0$ , then $c=c\wedge 1\le 0$ by the definition of $\to$ .)
iff ( $1=a\to 0$ implies that $c\wedge a\le 0$ whenever $c\le 1$ . In particular $a\le 1$ , so $a=a\wedge a\le 0$ or . On the other hand, if , then $a^*=0^*=0\to 0=1$ .)
$a\le a^{**}$ and $a^*=a^{***}$ (already true in any pseudocomplemented lattice)
$a^*\le a\to b$ (since $a^*\wedge a=0\le b$ )
$(a\to b)\wedge (a\to b^*)=a^*$
Proof. If $c\wedge a=0$ , then $c\wedge a\le b$ so $c\le (a\to b)$ , and $c\le (a\to b^*)$ likewise, so $c\le (a\to b)\wedge (a\to b^*)$ . This means precisely that $a^*=(a\to b)\wedge (a\to b^*)$ . $\qedsymbol$
$a\to b\le b^*\to a^*$ (since $(a\to b)\wedge b^*\le (a\to b)\wedge (a\to b^*)=a^*)$
$a^*\vee b\le a\to b$ (since $b\wedge a\le b$ and $a^* \wedge a=0\le b$ )

Note that in property 4, $a\le a^{**}$ , whereas $a^{**}\le a$ is in general not true, contrasting with the equality $a=a^{\prime\prime}$ in a Boolean lattice, where $^{\prime}$ is the complement operator. It can be shown that if $a^{**}\le a$ for all in a Heyting lattice , then is a Boolean lattice. In this case, the pseudocomplement coincides with the complement of an element $a^*=a^{\prime}$ , and we have the equality in property 7: $a^*\vee b=a\to b$ , 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 unary operator and $\to$ is a binary operator on . In other words, unlike a morphism between to Heyting lattices, which is nothing more than a lattice homomorphism, a morphism between two Heyting algebras preserves and $\to$ . Equivalently, a Heyting algebra is a p-algebra with the relative pseudocomplentation opreation $\to$ . A lattice homomorphism preserving and $\to$ is a Heyting algebra homomorphism: since $a^*=a\to 0$ , we have $f(a^*)=f(a\to 0)=f(a)\to f(0)=f(a)\to 0=f(a)^*$ .