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

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$$?

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$$.

• How can I construct the homomorphism $h:H \to \{1,0\}$? May 28 at 18:43
• It should work if you quotient H by a maximal filter.
– D.Q.
May 28 at 18:59
• I think I cannot construct a maximal filter on H, I can prove that it exists using Zorn's lemma but this proof is not constructive. May 28 at 19:08
• Yes, indeed. Is that a problem? Are you working without choice?
– D.Q.
May 28 at 19:15
• Yes, I am working in constructive mathematics. May 28 at 19:19