# complete Heyting algebra

A Heyting algebra that is also a complete lattice is called a complete Heyting algebra. In the following, we give a lattice characterization of complete Heyting algebras without the relative pseudocomplementation operator $\to$.

###### Proposition 1.

Let $H$ be a complete Heyting algebra, then

 $x\to y=\bigvee\{z\mid z\wedge x\leq y\}$

for any $x,y\in H$, and

 $x\wedge\bigvee A=\bigvee(x\wedge A),$

where $x\wedge A:=\{x\wedge y\mid y\in A\}$, for any $x\in H$, and any subset $A$ of $H$.

###### Proof.

We first prove the identity $x\wedge\bigvee A=\bigvee(x\wedge A)$. For any $y\in H$, we have $x\wedge\bigvee A\leq y$ iff $\bigvee A\leq x\to y$ iff $a\leq x\to y$ for all $a\in A$ iff $x\wedge a\leq y$ for all $a\in A$ iff $\bigvee(x\wedge A)\leq y$, hence $x\wedge\bigvee A=\bigvee(x\wedge A)$.

Next, we show $x\to y=\bigvee\{z\mid z\wedge x\leq y\}$. For any $a\in H$, we have $a\leq x\to y$ iff $a\wedge x\leq y$ iff $a\in\{z\mid z\wedge x\leq y\}$ iff $a\leq\bigvee\{z\mid z\wedge x\leq y\}$. ∎

The converse of the above is also true.

###### Proposition 2.

Let $H$ be a complete lattice such that

 $x\wedge\bigvee A=\bigvee(x\wedge A),$

where $x\wedge A:=\{x\wedge y\mid y\in A\}$, for any $x\in H$, and any subset $A$ of $H$. Then for any $x,y\in H$, defining

 $x\to y:=\bigvee\{z\mid z\wedge x\leq y\}$

turns $H$ into a complete Heyting algebra.

###### Proof.

We want to show that $a\leq x\to y$ iff $a\wedge x\leq y$ for any $a\in H$: $a\leq x\to y$ iff $a\leq\bigvee\{z\mid z\wedge x\leq y\}$. So $x\wedge a\leq x\wedge\bigvee\{z\mid z\wedge x\leq y\}=\bigvee\{x\wedge z\mid z% \wedge x\leq y\}\leq\bigvee\{y\}=y$

From this, one readily concludes that any finite distributive lattice is Heyting.

Remark. Since any complete lattice is bounded, a complete Brouwerian lattice is a complete Heyting algebra. A complete Heyting algebra is also called a frame.

Title complete Heyting algebra CompleteHeytingAlgebra 2013-03-22 19:31:42 2013-03-22 19:31:42 CWoo (3771) CWoo (3771) 10 CWoo (3771) Definition msc 03G10 msc 06D20 Locale