Can set-theoretic forcing exist without law of excluded middle?

Question

Of course the law of excluded middle is accepted by almost every mathematician except a few constructivists, but then I was wondering if set-theoretic forcing can exist without law of excluded middle. Of course some may say that the real question must be what will happen set theories (eg. ZF) without excluded middle, but then I will stick with my question.

Answer 1

Yes. Consider Intuitionistic Zermelo set theory (IZ) and Intuitionistic Zermelo-Fraenkel set theory (IZF) as presented in chapter 8 of Bell's "Set Theory: Boolean-valued models and Independence Proofs", third edition. Forcing in these set theories would use Heyting-algebra-valued models as classical ZF would use Boolean-valued models (pp. 165-166). Bell shows that the Law of Excluded Middle (LEM) holds in a Heyting-algebra-valued model if and only if the Heyting algebra in question is a boolean algebra. Since the Axiom of Choice implies LEM, the Axiom of choice does not hold in any Heyting-algebra-valued model for which the Heyting algebra in question is not a boolean algebra (this last sentence is a paraphrase of a statement of Bell's found on pg. 166 of his book).