> I don't see why you say that. Are you saying that any poset with this chain of adjunctions must be a Boolean algebra? That's imaginable, but I don't know such a theorem.

I think so.

Here's my sketch of the proof: in a Heyting algebra with the left adjoint \\(\setminus\\) to \\(\vee\\), first show \\(\top \leq \top \setminus\ (\top \setminus\ a) \to a\\) from the adjunction laws. After that, along with \\(\top \leq a \to b \to a\\) and \\(\top \leq (a \to b \to c) \to (a \to b) \to a \to c\\) and modus ponens \\(\top \leq a \to b \Longrightarrow \top \leq a \Longrightarrow \top \leq b\\) you have enough to show all of classical propositional logic. Then, using \\(\top \leq a \to b \Longleftrightarrow a \leq b\\) you can use classical propositional logic to recover the traditional axioms for a Boolean algebra.

I think so.

Here's my sketch of the proof: in a Heyting algebra with the left adjoint \\(\setminus\\) to \\(\vee\\), first show \\(\top \leq \top \setminus\ (\top \setminus\ a) \to a\\) from the adjunction laws. After that, along with \\(\top \leq a \to b \to a\\) and \\(\top \leq (a \to b \to c) \to (a \to b) \to a \to c\\) and modus ponens \\(\top \leq a \to b \Longrightarrow \top \leq a \Longrightarrow \top \leq b\\) you have enough to show all of classical propositional logic. Then, using \\(\top \leq a \to b \Longleftrightarrow a \leq b\\) you can use classical propositional logic to recover the traditional axioms for a Boolean algebra.