Heyting algebra


Next: Spectral theorem Up: Appendix Previous: Functors

Definition 3.5   A Heyting Algebra H is a relative pseudo complemented distributive lattice.

The property of being distributive means that the following equations are satisfied for any $ S_i\in\textbf{H}$

$\displaystyle S_1\wedge(S_2\vee S_3)$ $\displaystyle =(S_1\wedge S_2)\vee(S_1\wedge S_3)$    
$\displaystyle S_1\vee(S_2\wedge S_3)$ $\displaystyle =(S_1\vee S_2)\wedge(S_1\vee S_2)$    

The property of being relative pseudo complemented lattice means that for any two elements $ S_1,S_2\in\textbf{H}$ there exists a third element $ S_3\in\textbf{H}$, such that:
  1. $ S_1\cap S_3\subseteq S_2$
  2. $ \forall S\in\textbf{H}\hspace{.2in}S\subseteq S_3\hspace{.2in}iff\hspace{.2in}S_1\cap S\subseteq S_2$
where $ S_3$ is defined as the pseudo complement of $ S_1$ relative to $ S_2$ i.e., the greatest element of the set $ \{S:S_1\cap S\subseteq S_2\}$, and it is denoted as $ S_1\Rightarrow S_2$.
A particular feature of the Heyting algebra is the negation operation. The negation of an element S is defined to be the pseudo-complement of S i.e. $ \neg S:=S\Rightarrow 0$, therefore we can write

$\displaystyle \neg S:=\{f:B\rightarrow A\vert\forall g:C\rightarrow B, f o g \notin S\}$    

The above equation entails that $ \neg S$ is the least upper bound of the set $ \{x:S\cap x=0\}$, i.e. the biggest set that does not contain any element of S. From the above definition of negation operation it follows that the Heyting algebra does not satisfy the law of excluded middle, i.e. given any element S of an Heyting algebra, we have the following relation: $ S\vee\neg S\leq1$.

Proof. Let us consider $ S\vee\neg S=S\cup\neg S$. This represents the least upper bound of S and $ \neg S$ therefore, given any other element $ S_1$ in the Heyting algebra such that $ S\leq S_1$ and $ \neg S\leq\ S_1$ then, $ S\vee\neg S\leq S_1$. But, since for any S we have $ S\leq1$ and $ \neg S\leq1$ it follows that $ S\vee\neg S\leq1$. $ \qedsymbol$


Next: Spectral theorem Up: Appendix Previous: Functors
Cecilia Flori 2007-01-02