| Version current |
Version 11 |
| A \emph{Heyting lattice} $L$ is a Brouwerian lattice with a bottom element $0$. Equivalently, it is a relatively pseudocomplemented and pseudocomplemented lattice. |
A \emph{Heyting lattice} $L$ is a Brouwerian lattice with a bottom element $0$. Equivalently, it is a relatively pseudocomplemented and pseudocomplemented lattice. |
|
|
| Let $a^*$ denote the pseudocomplement of $a$ and $a\to b$ the pseudocomplement of $a$ relative to $b$. Then we have the following properties: |
Let $a^*$ denote the pseudocomplement of $a$ and $a\to b$ the pseudocomplement of $a$ relative to $b$. Then we have the following properties: |
|
|
| \begin{enumerate} |
\begin{enumerate} |
| \item $a^*=a\to 0$ (equivalence of definitions) |
\item $a^*=a\to 0$ (equivalence of definitions) |
| \item $1^*=0$ (if $c=1\to 0$, then $c=c\wedge 1\le 0$ by the definition of $\to$.) |
\item $1^*=0$ (if $c=1\to 0$, then $c=c\wedge 1\le 0$ by the definition of $\to$.) |
| \item $a^*=1$ iff $a=0$ ($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 $a=0$. On the other hand, if $a=0$, then $a^*=0^*=0\to 0=1$.) |
\item $a^*=1$ iff $a=0$ ($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 $a=0$. On the other hand, if $a=0$, then $a^*=0^*=0\to 0=1$.) |
| \item $a\le a^{**}$ and $a^*=a^{***}$ (already true in any pseudocomplemented lattice) |
\item $a\le a^{**}$ and $a^*=a^{***}$ (already true in any pseudocomplemented lattice) |
| \item $a^*\le a\to b$ (since $a^*\wedge a=0\le b$) |
\item $a^*\le a\to b$ (since $a^*\wedge a=0\le b$) |
| \item $(a\to b)\wedge (a\to b^*)=a^*$ |
\item $(a\to b)\wedge (a\to b^*)=a^*$ |
| \begin{proof} |
\begin{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^*)$. |
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^*)$. |
| \end{proof} |
\end{proof} |
| \item $a\to b\le b^*\to a^*$ (since $(a\to b)\wedge b^*\le (a\to b)\wedge (a\to b^*)=a^*)$ |
\item $a\to b\le b^*\to a^*$ (since $(a\to b)\wedge b^*\le (a\to b)\wedge (a\to b^*)=a^*)$ |
| \item $a^*\vee b\le a\to b$ (since $b\wedge a\le b$ and $a^* \wedge a=0\le b$) |
\item $a^*\vee b\le a\to b$ (since $b\wedge a\le b$ and $a^* \wedge a=0\le b$) |
| \end{enumerate} |
\end{enumerate} |
|
|
| 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 $a$ in a Heyting lattice $L$, then $L$ 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 \PMlinkname{relative pseudocomplementation}{RelativelyPseudocomplemented} coincides with the material implication in classical propositional logic. |
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 $a$ in a Heyting lattice $L$, then $L$ 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 \PMlinkname{relative pseudocomplementation}{RelativelyPseudocomplemented} coincides with the material implication in classical propositional logic. |
|
|
| A \emph{Heyting algebra} is a Heyting lattice $L$ such that $^*$ is a unary operator and $\to$ is a binary operator on $L$. 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 $f$ preserving $0,1$ 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)^*$. |
A \emph{Heyting algebra} is a Heyting lattice $L$ such that $^*$ is a unary operator and $\to$ is a binary operator on $L$. 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 $f$ preserving $0,1$ 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)^*$. |
|
|
| \textbf{Remark}. In the literature, the assumption that a Heyting algebra contains $0$ is sometimes dropped. Here, we call it a Brouwerian lattice instead. |
\textbf{Remark}. In the literature, the assumption that a Heyting algebra contains $0$ is sometimes dropped. Here, we call it a Brouwerian lattice instead. |
