Axioms for a Heyting Algebra as a Set System (Partial Order Lattice Under Inclusion)

Question

According to the corresponding section in Wikipedia:

An element $x$ of a Heyting algebra $H$ is called regular iff $x = \neg y$ for some $y \in H$.

Elements $x$ and $y$ of a Heyting algebra are called complements to each other iff $x \land y = 0$ and $x \lor y =1$. If it exists, any such $y$ must be unique and in fact equal to $\neg x$. If $x$ admits a complement then we call it complemented.

For any Heyting algebra, the following three conditions are equivalent:

1. $H$ is a Boolean algebra
2. Every element of $H$ is regular.
3. Every element of $H$ is complemented.

My question is the following:

If we consider this as a set system, then is a Heyting algebra the same as a Boolean algebra except that it does not necessarily need to be closed under set complements?

My reasoning is as follows:

1. The terminology complemented, complement, and set complement are quite similar.

2. If we change the lattice notation to the corresponding set notation ($\neg \iff ^c$, $\land \iff \cap$, $\lor \iff \cup$ ), then given a set $A$, and considering a Heyting algebra $H$ on its lattice of subsets, we have that $X \subset A$ is regular iff $X=Y^c$ for some $Y \in H, Y \subset A$, $X$ and $Y$ are complements if and only if $X \cap Y=\emptyset$, $X \cup Y=A \implies X = Y^c$. The above excerpt implies that if for every $X \in H$, $X=Y^c$ for some $Y\in H$ (i.e. $H$ is closed under set complements) then it is a Boolean algebra (since it is a lattice and hence closed under finite intersections and unions).

3. The same way that Boolean algebras are the algebraic model for classical logic, Heyting algebras are the algebraic model for intuitionistic logic, which rejects the Law of the Excluded Middle. Not necessarily being closed under set complements seemed to be the set-theoretic analog to the Law of the Excluded Middle not holding (because then $(X^c)^c$ is not necessarily defined, which means that we can not immediately conclude that $X=(X^c)^c$, the same way in intuitionistic logic we cannot always conclude that $\neg \neg x =x$).

Answer 1

Yes and no.

Yes, in the sense that a complement of $x$ in a bounded lattice is a (necessarily unique) element $y$ with $x\wedge y = \bot$ and $x\vee y = \top$ and these obviously need not exist for all $x$ of some Heyting algebra.

No, in the sense that $\neg x$ in a Heyting algebra does not denote a complement of $x$, but a pseudocomplement, i.e. $\neg x := x \Rightarrow \bot$. The power set of a constructive set is surely closed under pseudocomplements. It just so happens that pseudocomplements are not necessarily complements, as $x\vee \neg x < \top$ may happen.

EDIT: Here is a classical counterexample (I think, I have not tried or seen this before):

Take the standard topology $T$ on $\mathbb{R}$. This is a Heyting algebra with "implication" $A \to B := \operatorname{int}(A^c \cup B)$, hence $\neg A = A \to \emptyset = \operatorname{int}(A^c)$. Let $A:=(0\,.. 1)$. Then:

$$\neg A = \operatorname{int}((-\infty\,.. 0] \cup [1\,.. \infty)) = (-\infty\,.. 0) \cup (1\,..\infty)$$

Hence:

$$A\cup \neg A = \mathbb{R} \setminus \{0,1\} \subsetneq \mathbb{R}$$