properties of Heyting algebras

Proposition 1.

Let $H$ be a Brouwerian lattice. The following properties hold:

1. $a\to a=1$

2. $a\wedge (a\to b)=a\wedge b$

3. $b\wedge (a\to b)=b$

4. $a\to (b\wedge c)=(a\to b)\wedge (a\to c)$

Proof.

The first three equations are proved in this entry (http://planetmath.org/BrouwerianLattice). We prove the last equation here. For any $x\in H$, $x\le a\to (b\wedge c)$ iff $x\wedge a\le b\wedge c$ iff $x\wedge a\le b$ and $x\wedge a\le c$ iff $x\le a\to b$ and $x\le a\to c$ iff $x\le (a\to b)\wedge (a\to c)$. Hence the equation holds. ∎

Proposition 2.

Conversely, a lattice with a binary operation $\mathrm{\to }$ satisfying the four conditions above is a Brouwerian lattice.

Proof.

Let $H$ be a lattice with a binary operation $\to$ on it satisfying the identities above. We want to show that $x\le a\to b$ iff $x\wedge a\le b$ for any $x\in H$. First, suppose $x\le a\to b$. Then $x\wedge a\le a\wedge (a\to b)=a\wedge b\le b$. Conversely, suppose $x\wedge a\le b$. Then $a\to (x\wedge a)\le a\to b$ by the property 6 in this entry (http://planetmath.org/BrouwerianLattice). As a result, $x=x\wedge (a\to x)\le (a\to a)\wedge (a\to x)=a\to (a\wedge x)\le a\to b$. ∎

Corollary 1.

The class of Brouwerian lattices is equational. The class of Heyting algebras is equational.

Proof.

The first fact is the result of the two propositions above. The second comes from the fact that $0$ is not used in the proofs of the propositions. ∎

Proposition 3.

Let $H$ be a Heyting algebra. Then $a\mathrm{\vee }{a}^{\mathrm{*}}\mathrm{=}\mathrm{1}$ iff $a^{\mathrm{*}\mathrm{*}}\mathrm{=}a$ for all $a\mathrm{\in }H$.

Proof.

Suppose $a\vee a^{*}=1$. Since $a\le a^{**}$ in any Heyting algebra, we only need to show that $a^{**}\le a$. Since $H$ is distributive, we have $a^{**}=a^{**}\wedge (a\vee a^{*})=(a^{**}\wedge a)\vee (a^{**}\wedge a^{*})=a^{**}\wedge a$. The last equation comes from the fact that $a^{**}\wedge a^{*}=0$. As a result, $a^{**}\le a$. Conversely, suppose $a^{**}=a$. Now, ${(a\vee a^{*})}^{*}\le a^{*}\wedge a^{**}=0$, and therefore $a\vee a^{*}={(a\vee a^{*})}^{**}=0^{*}=1$. ∎

Note, the last inequality in the proof above comes from the inequality ${(a\vee b)}^{*}\le a^{*}\wedge b^{*}$, which is a direct consequence of the fact that pseudocomplementation is order-reversing: $x\le y$ implies that $y^{*}\le x^{*}$.

Corollary 2.

A Heyting algebra where psuedocomplentation $\mathrm{*}$ satisfies the equivalent conditions above is a Boolean algebra. Conversely, a Boolean algebra with $a\mathrm{\to }b\mathrm{:=}{a}^{\mathrm{*}}\mathrm{\vee }b$ is a Heyting algebra.

Proof.

Since $a\wedge a^{*}=0$ and $a\vee a^{*}=1$, the pseudocomplementation operation $*$ is the complementation operation. And because any Heyting algebra is distributive, it is Boolean as a result. Conversely, assume $B$ is Boolean. Then $c\le a\to b=a^{*}\vee b$, so that $c\wedge a\le a\wedge (a^{*}\vee b)=a\wedge b\le b$. On the other hand, if $c\wedge a\le b$, then $c\le c\vee a^{*}=(c\wedge a)\vee a^{*}\le a^{*}\vee b=a\to b$. ∎

Proposition 4.

A subset $F$ of a Heyting algebra $H$ is an ultrafilter iff there is a Heyting algebra homomorphism $f\mathrm{:}H\mathrm{\to }\mathrm{\{}\mathrm{0}\mathrm{,}\mathrm{1}\mathrm{\}}$ with $F\mathrm{=}{f}^{\mathrm{-}\mathrm{1}}\mathit{}\mathrm{(}\mathrm{1}\mathrm{)}$.

Proof.

First, assume $f:H\to \{0,1\}$ is a Heyting algebra homomorphism, and $F=f^{-1}(1)$. Clearly, $F$ is a filter. Suppose $0\ne a\notin F$, then $f(a)=0$. Now, $f(a^{*})=f{(a)}^{*}=0^{*}=1$, so $a^{*}\in F$. If $F$ is not maximal, let $G$ be a proper filter containing $F$ and $a$, then $a^{*}\in G$, so that $0\in a\wedge a^{*}\in G$, and hence $G=H$, contradicting the fact that $G$ is proper. So $F$ is maximal.

Conversely, suppose $F$ is an ultrafilter of $H$. Define $f:H\to \{0,1\}$ by $f(x)=1$ iff $x\in F$. Let $a,b\in H$. We first show that $f$ is a lattice homomorphism:

• First, $f(a\wedge b)=1$ iff $a\wedge b\in F$ iff $a,b\in F$ (since $F$ is a filter) iff $f(a)=f(b)=1$. So $f$ respects $\wedge$.

• Next, if $f(a\vee b)=0$, then $a\vee b\notin F$, which means neither $a$ nor $b$ is in $F$, or that $f(a)=f(b)=0$. On the other hand, if $f(a)=f(b)=0$, then neither $a$ nor $b$ is in $F$, since $F$ is an ultrafilter. As a result, neither is $a\vee b\in F$, which means $f(a\vee b)=0$. So $f$ respects $\vee$.

So $f$ is a lattice homomorphism. Next, we show that $f$ is a Heyting algebra homomorphism, which means showing that $f$ respects $\to$: $f(a\to b)=f(a)\to f(b)$. It suffices to show $f(a\to b)=0$ iff $f(a)=1$ and $f(b)=0$.

• First, if $f(a)=1$ and $f(b)=0$ then $a\in F$ and $b\notin F$. If $a\to b\in F$, then $(a\to b)\wedge a\in F$. Since $(a\to b)\wedge a\le b$, $b\in F$, a contradiction. So $a\to b\notin F$.

• On the other hand, suppose $f(a\to b)=0$. So $a\to b\notin F$. Now, since $b\le a\to b$, $b\notin F$, or $f(b)=0$. If $f(a)=0$, then $a\notin F$, so there is some $c\in F$ with $0=a\wedge c$. But this means $c\le a^{*}$, or $a^{*}\in F$. Since $a^{*}\le a\to b$, we would have $a\to b\in F$, a contradiction. Hence $f(a)=1$.

Therefore $f$ is a Heyting algebra homomorphism. ∎

In the proof above, we use the fact that, for any ultrafilter $F$ in a bounded lattice $L$, if $x\notin F$, then there is $y\in F$ such that $0=x\wedge y$ (for otherwise, the filter generated by $x$ and $F$ would be proper and properly contains $F$, contradicting the maximality of $F$). If in addition $L$ were distributive, then $a\vee b\in F$ implies that either $a\in F$ or $b\in F$. To see this, suppose $a\notin F$. Then there is $c\in F$ such that $0=a\wedge c$. Similarly, if $b\notin F$, there is $d\in F$ such that $0=b\wedge d$. Let $e=c\wedge d\in F$. So $e\ne 0$, and $a\wedge e=0=b\wedge e$. Furthermore, $0=(a\wedge e)\vee (b\wedge e)=(a\vee b)\wedge e$. If $a\vee b\in F$, so would $0\in F$, a contradiction. Hence $a\vee b\notin F$.

Title	properties of Heyting algebras
Canonical name	PropertiesOfHeytingAlgebras
Date of creation	2013-03-22 19:31:45
Last modified on	2013-03-22 19:31:45
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	19
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03G10
Classification	msc 06D20