Heyting Algebra

What is Heyting Algebra?Why we study Heyting Algebra?Some Property of Heyting AlgebraLawvere Theory of Heyting Algebra

What is Heyting Algebra?

 

Let $(P,\le )$$(P,\le)$ be a poset, we know it form a category, with $x\in P$$x\in P$ as object and the morphism between $x,y$$x,y$ is $x\le y$$x\le y$.

A Heyting Algebra $H$$H$ is a Cartesian Closed Poset Category with finite product and coproduct.

Hence, $H$$H$ is a lattice, with $\mathrm{\top },\mathrm{\perp }$$\top,\bot$ (Empty product and coproduct). It satisfies $x\wedge (y\vee z)=(x\wedge y)\vee (x\wedge z)$$x\wedge (y\vee z)=(x\wedge y)\vee (x\wedge z)$ since it is Cartesian Closed, we have $x\wedge$$x\wedge$ is the left adjoint functor, hence preserve coproduct.

We use $\Rightarrow$$\Rightarrow$ to denote the internal hom:

$$x\wedge y\le z⟺x\le y\Rightarrow z$$

In particular, we have $x\wedge y\le x⟺x\le y\Rightarrow x$$x\wedge y\le x\iff x\le y\Rightarrow x$.

Since it is Cartesian Closed and has $\mathrm{\perp }$$\bot$, we could define $\mathrm{\neg }x:=x\Rightarrow \mathrm{\perp }$$\neg x:=x\Rightarrow \bot$.

Then $y\le \mathrm{\neg }x⟺x\wedge y=\mathrm{\perp }$$y\le\neg x\iff x\wedge y=\bot$. In particular, $\mathrm{\neg }x\wedge x=\mathrm{\perp }$$\neg x\wedge x=\bot$. In a complete Heyting algebra, $\mathrm{\neg }x$$\neg x$ is the join of all the $y$$y$ such that $y\wedge x=0$$y\wedge x=0$.

Example. Every Boolean Algebra form a Heyting Algebra. The internal hom is given by $x\Rightarrow y:=\mathrm{\neg }x\vee y$$x\Rightarrow y:=\neg x\vee y$

For example, $(P(S),\cup ,\cap ,\mathrm{\neg },S,\mathrm{\varnothing })$$(P(S),\cup,\cap,\neg,S,\empty)$.

Why we study Heyting Algebra?

Let $\mathcal{E}$$\mathcal{E}$ be a topos such that ${\mathsf{Sub}}_{\mathcal{E}}(-)\cong {\mathrm{Hom}}_{\mathcal{E}}(-,\mathrm{\Omega })$$\mathsf{Sub}_{\mathcal E}(-)\cong\mathrm{Hom}_{\mathcal E}(-,\Omega)$. Then $\mathrm{\Omega }$$\Omega$ is an internal Heyting Algebra(We will discuss the Lawvere Theory of Heyting Algebra later), hence ${\mathrm{Hom}}_{\mathcal{E}}(-,\mathrm{\Omega })$$\mathrm{Hom}_{\mathcal E}(-,\Omega)$ is an Heyting Algebra Valued functor.

In addition, the open set lattice of a topological space is a Heyting Algebra.

Proposition.

Let $(X,\mathcal{O}(X))$$(X,\mathcal O(X))$ be a topological space, then $\mathcal{O}(X)$$\mathcal O(X)$ is a Heyting Algebra.

Remark. I feel confused when I saw Maclane's definition and proof about the internal hom in $\mathcal{O}(X)$$\mathcal O(X)$. Here is mine.

Proof. Easy to see that the product and coproduct are just $\cup ,\cap$$\cup,\cap$. For any open set $U,V$$U,V$, we define $U\Rightarrow V$$U\Rightarrow V$ as $\text{int}(U^c\cup V)$$\text{int}(U^c\cup V)$.

It is not a big surprise. Since in $P(X)$$P(X)$, we have $U\Rightarrow V:=U^c\cup V$$U\Rightarrow V:= U^c\cup V$. Also, we have

$$i(U)\subseteq V⟺U\subseteq \text{int}(V)$$

Here $i:\mathcal{O}(X)\hookrightarrow P(X)$$i:\mathcal O(X)\hookrightarrow P(X)$ is the inclusion functor.

So, in $P(X)$$P(X)$, we have

$$O\cap U\subseteq V⟺O\subseteq U^c\cup V$$

Also, since $O\cap U\in \mathcal{O}(X)$$O\cap U\in\mathcal O(X)$, we have

$$O\cap U\subseteq V⟺O\subseteq \text{int}(U^c\cup V)$$

Thus $\text{int}(U^c\cup V)=U\Rightarrow V$$\text{int}(U^c\cup V)=U\Rightarrow V$. $◻$$\square$

Some Property of Heyting Algebra

Since Heyting Algebra is a Cartesian Closed Category, we have:

The unit and counit

$$X\to (X\times Y{)}^Y,Y\times X^Y\to X$$

gives us

$$x\le (y\Rightarrow (x\wedge y)),y\wedge (y\Rightarrow x)\le x$$

The properties $X^1\cong X,1^X\cong 1$$X^1\cong X,1^X\cong 1$ gives us

$$\mathrm{\top }\Rightarrow X=X,X\Rightarrow \mathrm{\top }=\mathrm{\top }$$

Since $x\Rightarrow -$$x\Rightarrow-$ is the right adjoint of $x\wedge -$$x\wedge -$, we have $x\Rightarrow -$$x\Rightarrow-$ preserve products.

$$x\Rightarrow (y\wedge z)=x\Rightarrow y\wedge x\Rightarrow z$$

And $x\wedge -$$x\wedge -$ preserve coproducts

$$x\wedge (y\vee z)=(x\wedge y)\vee (x\wedge z)$$

The associative law for product $X^{Y\times Z}\cong (X^Y{)}^Z$$X^{Y\times Z}\cong (X^{Y})^Z$ gives us

$$(y\wedge z)\Rightarrow x=z\Rightarrow (y\Rightarrow x)$$

Also, we have

$$(x\Rightarrow y)\ge z⟺z\le (x\Rightarrow y)⟺z\wedge x\le y⟺x\wedge z\le y⟺x\le (z\Rightarrow y)$$

Hence we have $-\Rightarrow y:H\to H^{\mathrm{op}}:-\Rightarrow y$$-\Rightarrow y:H\to H^{\mathrm{op}}:-\Rightarrow y$ is adjoint of itself.

Now since $-\Rightarrow y:H\to H^{\mathrm{op}}$$-\Rightarrow y:H\to H^{\mathrm{op}}$ is left adjoint, it will preserve coproducts.

Hence we have

$$(x\vee z)\Rightarrow y=(x\Rightarrow y)\vee (z\Rightarrow y)$$

Now let us discuss some properties about $\mathrm{\neg }$$\neg$

Proposition. In any Heyting Algebra, we have $x\le \mathrm{\neg }\mathrm{\neg }x(1),\mathrm{\neg }x=\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }x(2),\mathrm{\neg }\mathrm{\neg }(x\wedge y)=\mathrm{\neg }\mathrm{\neg }x\wedge \mathrm{\neg }\mathrm{\neg }y(3)$$x\le\neg\neg x\quad(1),\neg x=\neg \neg\neg x\quad(2),\neg\neg(x\wedge y)=\neg\neg x\wedge\neg\neg y\quad(3)$.

Proof.

Recall that $\mathrm{\neg }x=x\Rightarrow \mathrm{\perp }$$\neg x=x\Rightarrow \bot$, hence $y\le \mathrm{\neg }x⟺x\wedge y=\mathrm{\perp }$$y\le \neg x\iff x\wedge y=\bot$. If $y=\mathrm{\neg }x$$y=\neg x$, we have $x\wedge \mathrm{\neg }x=\mathrm{\perp }$$x\wedge \neg x=\bot$.

So

$$x\le \mathrm{\neg }(\mathrm{\neg }x)⟺x\wedge \mathrm{\neg }x=\mathrm{\perp }$$

Hence we have

$$\mathrm{\neg }x\ge \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }x$$

$\mathrm{\neg }:=-\Rightarrow 0$$\neg:=-\Rightarrow 0$ is a functor. But $x\le \mathrm{\neg }\mathrm{\neg }x⟹\mathrm{\neg }x\le \mathrm{\neg }\mathrm{\neg }(\mathrm{\neg }x)$$x\le\neg\neg x\implies\neg x\le\neg\neg(\neg x)$. Hence $\mathrm{\neg }x=\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }x$$\neg x=\neg\neg\neg x$.

Now we need to prove that

$$\mathrm{\neg }\mathrm{\neg }(x\wedge y)=\mathrm{\neg }\mathrm{\neg }x\wedge \mathrm{\neg }\mathrm{\neg }y$$

First notice that we have $x\wedge y\le x$$x\wedge y\le x$, hence $\mathrm{\neg }\mathrm{\neg }(x\wedge y)\le \mathrm{\neg }\mathrm{\neg }x$$\neg\neg (x\wedge y)\le\neg\neg x$. Similarly we have $\mathrm{\neg }\mathrm{\neg }(x\wedge y)\le \mathrm{\neg }\mathrm{\neg }y$$\neg\neg(x\wedge y)\le\neg\neg y$.

Hence we have $\mathrm{\neg }\mathrm{\neg }(x\wedge y)\le \mathrm{\neg }\mathrm{\neg }x\wedge \mathrm{\neg }\mathrm{\neg }y$$\neg\neg(x\wedge y)\le\neg\neg x\wedge\neg\neg y$. For the converse, see Sheaves in Geometric and Logic, page 53. $◻$$\square$

Proposition. Let $H$$H$ be a Heyting algebra, if $x$$x$ has complement, then the complement of $x$$x$ must be $\mathrm{\neg }x$$\neg x$.

Proof. Assume that $x$$x$ has complement $a$$a$. Then $x\wedge a=\mathrm{\perp },x\vee a=\mathrm{\top }$$x\wedge a=\bot,x\vee a=\top$.

By $x\wedge a\le \mathrm{\perp }$$x\wedge a\le\bot$ we have $x\le \mathrm{\neg }a⟹\mathrm{\neg }x\ge a$$x\le\neg a\implies \neg x\ge a$.

Now consider $\mathrm{\neg }x=\mathrm{\neg }x\wedge (x\vee a)=(\mathrm{\neg }x\wedge x)\vee (\mathrm{\neg }x\wedge a)=\mathrm{\neg }x\wedge a⟹a\ge \mathrm{\neg }x$$\neg x=\neg x\wedge (x\vee a)=(\neg x\wedge x)\vee(\neg x\wedge a)=\neg x\wedge a\implies a\ge\neg x$. Hence $\mathrm{\neg }x=a$$\neg x=a$. $◻$$\square$

Lawvere Theory of Heyting Algebra

In this section, we will use equations to describe Heyting algebra, and get the Lawvere Theory of Heyting Algebra and see that in any topos $\mathcal{E}$$\mathcal E$, the subobject classifier is a model of Lawvere Theory of Heyting Algebra in $\mathcal{E}$$\mathcal E$.

Proposition.

A Latice $H$$H$ with $\mathrm{\top },\mathrm{\perp }$$\top,\bot$ is a Heyting Algebra iff it has a operation $\Rightarrow :H^2\to H$$\Rightarrow:H^2\to H$ such that

$$(x\Rightarrow x)=\mathrm{\top },x\wedge (x\Rightarrow y)=x\wedge y,y\wedge (x\Rightarrow y)=y,x\Rightarrow (y\wedge z)=(x\Rightarrow y)\wedge (x\Rightarrow z)$$

Proof. See Sheaves in Geometric and Logic, page 54. $◻$$\square$

Definition.

The Lawvere Theory of Heyting Algebra is the Lawvere Theory of bounded Lattice plus the following identity

$$(x\Rightarrow x)=\mathrm{\top },x\wedge (x\Rightarrow y)=x\wedge y,y\wedge (x\Rightarrow y)=y,x\Rightarrow (y\wedge z)=(x\Rightarrow y)\wedge (x\Rightarrow z)$$

For example, the first identity should be understood as

$$\Rightarrow \circ \mathrm{\Delta }=\mathrm{\top }$$

Recall Categorical Logic Primer: Connectives and Quantifiers, we define $\wedge ,\vee ,\Rightarrow$$\wedge,\vee,\Rightarrow$ on the subobject classifier $\mathrm{\Omega }$$\Omega$.

This will make the subobject classifier $\mathrm{\Omega }$$\Omega$ becomes an Internal Heyting Algebra.

If this topos is well powered,then ${\mathsf{Sub}}_{\mathcal{E}}(-)\cong {\mathrm{Hom}}_{\mathcal{E}}(-,\mathrm{\Omega })$$\mathsf{Sub}_{\mathcal E}(-)\cong\mathrm{Hom}_{\mathcal E}(-,\Omega)$ will be a Heyting algebra valued functor.

Another example is an Internal Heyting Algebra object in $\mathsf{Top}$$\mathsf{Top}$.

Recall the open set functor $\mathcal{O}:{\mathsf{Top}}^{\mathsf{op}}\to \mathsf{Heyting}$$\mathcal O:\mathsf{Top^{op}}\to\mathsf{Heyting}$ maps each topological space to $\mathcal{O}(X)$$\mathcal O(X)$ and continuous function to $f^{-1}:\mathcal{O}(Y)\to \mathcal{O}(X)$$f^{-1}:\mathcal O(Y)\to\mathcal O(X)$. This functor is represented by Sierpinski space. i.e. This space $S=\{0,1\}$$S=\{0,1\}$ with $\mathcal{O}(S)=\{\mathrm{\varnothing },\{1\},\{0,1\}\}$$\mathcal O(S)=\{\empty,\{1\},\{0,1\}\}$.

Hence ${\mathrm{Hom}}_{\mathsf{Top}}(-,S)$$\mathrm{Hom}_{\mathsf{Top}}(-,S)$ is a Heyting Algebra valued functor, i.e. $S$$S$ is an internal Heyting Algebra in $\mathsf{Top}$$\mathsf{Top}$.

If we consider the convergent sequence on $S$$S$, denote as $F(S)$$F(S)$, then we will get a Heyting Algebra as well.

Proposition. Let $X$$X$ be a topological space, we know that $\mathsf{Sh}(X)$$\mathsf{Sh}(X)$ form a topos. Then we have:

$$\mathcal{O}(X)\cong {\mathsf{Sub}}_{\mathsf{Sh}(X)}(1)$$

i.e. The open set lattice is the truth value of $\mathsf{Sh}(X)$$\mathsf{Sh}(X)$.

Proof.

Firstly, we have the terminal object $1={\mathrm{Hom}}_{\mathcal{O}(X)}(-,X)=y_X$$1=\mathrm{Hom}_{\mathcal O(X)}(-,X)=y_X$ since Yoneda embedding preserve limit.

For each open set $U\in \mathcal{O}(X),{\mathrm{Hom}}_{\mathcal{O}(X)}(-,U)$$U\in\mathcal O(X),\mathrm{Hom}_{\mathcal O(X)}(-,U)$ is a sub sheaf of $1$$1$ since Yoneda embedding preserve monomorphism.

Give a subsheaf of $y_X$$y_X$, denote as $S$$S$. Then $S={\mathrm{colim}}_i{y}_{U_i}$$S=\operatorname{colim}_{i} y_{U_{i}}$. For all $y_{U_i}\to S$$y_{U_i}\to S$. But then the colimit is just the ${\mathrm{Hom}}_{\mathcal{O}(X)}(-,\bigcup _i{U}_i)$$\mathrm{Hom}_{\mathcal O(X)}(-,\bigcup_{i} U_i)$.

Or Consider any subsehaf $S$$S$, define $U_S:=\{V\in \mathcal{O}(X):S(V)\ne \mathrm{\varnothing }\}$$U_S:=\{V\in\mathcal O(X):S(V)\ne \empty\}$. Easy to see that $S\cong \mathrm{Hom}(-,U_S)$$S\cong\mathrm{Hom}(-,U_S)$.

Hence we have the one one correspondense between $\mathcal{O}(X)$$\mathcal O(X)$ and ${\mathsf{Sub}}_{\mathsf{Sh}(X)}(1)$$\mathsf{Sub}_{\mathsf{Sh}(X)}(1)$.

Clearly we have $U\subseteq V⟺y_U\subseteq y_V$$U\subseteq V\iff y_{U}\subseteq y_V$. $◻$$\square$

Here is another way to show.

The subobject classfier of $\mathsf{Sh}(X)$$\mathsf{Sh}(X)$ is $\mathrm{\Omega }(U):=\{V\in \mathcal{O}(X):V\subseteq U\}$$\Omega(U):=\{V\in\mathcal{O}(X):V\subseteq U\}$. Hence we have

 

$$\begin{array}{c}{\mathsf{Hom}}_{\mathsf{Sh}(X)}(1,\mathrm{\Omega })=\mathsf{Nat}({\mathrm{Hom}}_{\mathcal{O}(X)}(-,X),\mathrm{\Omega })\cong \mathrm{\Omega }(X)=\mathcal{O}(X)\end{array}$$

Proof.

Firstly, we have the terminal object $1={\mathrm{Hom}}_{\mathcal{O}(X)}(-,X)=y_X$$1=\mathrm{Hom}_{\mathcal O(X)}(-,X)=y_X$ since the Yoneda embedding preserves limits.

For each open set $U\in \mathcal{O}(X)$$U\in\mathcal O(X)$, ${\mathrm{Hom}}_{\mathcal{O}(X)}(-,U)$$\mathrm{Hom}_{\mathcal O(X)}(-,U)$ is a subsheaf of $1$$1$ since the Yoneda embedding preserves monomorphisms.

Given a subsheaf $S$$S$ of $y_X$$y_X$, we have $S={\mathrm{colim}}_i{y}_{U_i}$$S=\operatorname{colim}_{i} y_{U_{i}}$. For each $i$$i$, we have $y_{U_i}\to S$$y_{U_i}\to S$. The colimit is precisely ${\mathrm{Hom}}_{\mathcal{O}(X)}(-,\bigcup _i{U}_i)$$\mathrm{Hom}_{\mathcal O(X)}(-,\bigcup_{i} U_i)$.

Alternatively, consider any subsheaf $S$$S$. Define $U_S:=\{V\in \mathcal{O}(X):S(V)\ne \mathrm{\varnothing }\}$$U_S:=\{V\in\mathcal O(X):S(V)\neq \emptyset\}$. It is easy to see that $S\cong \mathrm{Hom}(-,U_S)$$S\cong\mathrm{Hom}(-,U_S)$.

Hence we have a one-to-one correspondence between $\mathcal{O}(X)$$\mathcal O(X)$ and ${\mathsf{Sub}}_{\mathsf{Sh}(X)}(1)$$\mathsf{Sub}_{\mathsf{Sh}(X)}(1)$.

Clearly, $U\subseteq V⟺y_U\subseteq y_V$$U\subseteq V\iff y_{U}\subseteq y_V$. $◻$$\square$

Another Approach

Here is another way to show this. The subobject classifier of $\mathsf{Sh}(X)$$\mathsf{Sh}(X)$ is $\mathrm{\Omega }(U):=\{V\in \mathcal{O}(X):V\subseteq U\}$$\Omega(U):=\{V\in\mathcal{O}(X):V\subseteq U\}$.

Hence we have

$${\mathsf{Hom}}_{\mathsf{Sh}(X)}(1,\mathrm{\Omega })=\mathsf{Nat}({\mathrm{Hom}}_{\mathcal{O}(X)}(-,X),\mathrm{\Omega })\cong \mathrm{\Omega }(X)=\mathcal{O}(X)$$