Satisfiability in an Heyting algebra implies satisfiability in a Boolean algebra for propositional logic?

Question

Let $\mathcal{L}$ be a propositional language and let $\text{Prop}(\mathcal{L})$ be the set of all the propositions of the language $\mathcal{L}$.

Let $(H,\wedge,\vee,\rightarrow,1,0)$ be an Heyting algebra. An evaluation of the propositions of $\mathcal{L}$ in $(H,\wedge,\vee,\rightarrow,1,0)$ is a map $V:\text{Prop}(\mathcal{L}) \to H$ such that $V(\top)=1$, $V(\bot)=0$, $V(P \wedge Q)=V(P) \wedge V(Q)$, $V(P \vee Q)=V(P) \vee V(Q)$ and $V(P \rightarrow Q)=V(P) \rightarrow V(Q)$.

Let $\Gamma$ be a set of propositions of the language $\mathcal{L}$. Suppose that there exist an Heyting algebra $(H,\wedge,\vee,\rightarrow,1,0)$ and an evaluation $V:\text{Prop}(\mathcal{L}) \to H$ such that $V(P)=1$ for every $P \in \Gamma$.

Can I construct a Boolean algebra $(B,\wedge,\vee,\rightarrow,\neg,1,0)$ and an evaluation $V':\text{Prop}(\mathcal{L}) \to B$ such that $V'(P)=1$ for every $P \in \Gamma$?

Answer 1

Consider a homomorphism h from the Heyting algebra H into the two elements Boolean algebra 2. Then the induced valuation $h\circ V$ witnesses the satisfiability of $\Gamma$ over 2.

---

For a proof which does not make use the axiom of choice you can also proceed as follows. Let $(H,\lor,\land,\to,1,0)$ be the Heyting algebra witnessing the satisfiability of $\Gamma$ under the valuation $V$. Remember that its subset of regular elements $H_\neg=\{ x\in H : x=\neg \neg x \}$ forms a Boolean algebra $(H_{\neg},\lor',\land,\to,1,0)$, where $\lor':=\neg \neg (x\lor y)$ -- see also this question.

Now consider the map $f:H\to H_\neg$ such that $f(x)=\neg \neg x$. The same proof that establishes that $H_\neg$ is a Boolean algebra also gives that $f(0)=0, f(1)=1, f(x\land y)=f(x)\land f(y)$ and $f(x\to y)=f(x)\to f(y)$ (see the link above). For disjunction, as you pointed out in the comments, it is not true in general that $\neg\neg (x\lor y)=\neg\neg x\lor \neg\neg y$. However, since Heyting algebras satisfy the De morgan rule $\neg(a\lor b)=\neg a\land \neg b$ and also simplify triple negation to single negation, we have:

$$ f(x\lor y)=\neg\neg (x\lor y) = \neg(\neg x\land \neg y) = \neg(\neg \neg \neg x \land \neg \neg \neg y) = \neg \neg (\neg \neg x \lor \neg \neg y)=f(x)\lor' f(y). $$

Which establishes that $f:H\to H_{\neg}$ is a homomorphism. Then the valuation $f\circ V$ witnesses the satisfiability of $\Gamma$ over $H_\neg$.