Is a Hetying algebra with coexponetials Boolean?

85 Views Asked by At

Suppose we have a Heyting algebra $\mathcal A$ with coexponentials. Specifically, for every $a, b : \mathcal A$ we have an object $b \backslash a$ with the properties that $b \le a \lor (b \backslash a)$, and that $b \le (a \lor z)$ implies $(b\backslash a) \le z$, forall $z : \mathcal A$.

Is $\mathcal A$ Boolean? In other words, are coexponentials (in addition to all the usual Heyting structure) sufficient to guarantee that $((a \to \bot) \to \bot) \cong a$ forall $a : \mathcal A$? Why or why not?

(Sanity check: the coexponential properties I wrote above are dual to the exponential properties that $a \land (a \to b) \le b$ and that $a \land x \le b$ implies $x \le (a \to b)$ forall $x : \mathcal A$.)

1

There are 1 best solutions below

0
On BEST ANSWER

No. If you have just coexponentials, you're called a co-heyting algebra, and if you have both you're called a bi-heyting algebra.

Notice that $H$ is heyting if and only if $H^\text{op}$ is co-heyting. So if $H$ is heyting and $H \cong H^\text{op}$, then we'll get a bi-heyting structure on $H$! If $H$ is not boolean, then we'll be done.

Of course, there are lots of examples of $H$ with this property. For instance, a chain of length $3$,

$$\bot \leq a \leq \top$$

As a quick exercise, you might try to find the heyting and co-heyting structures on this lattice.


I hope this helps ^_^