Are there any relatively consistent proofs based on forcing that cannot be proven outside of the AC?

Question

There are many papers that point out that the behavior of forcing is quite different with and without the AC.

I wonder how much of an impact this has on relative consistency proofs.

Answer 1

Sometimes, but not quite.

You don't need to assume $\sf AC$ in order to get forcing to work. You also don't need to assume $\sf AC$ in the meta-theory order to get forcing to work over countable models of set theory. You also don't need to assume $\sf AC$ in the meta-theory in order to do general independence results, since we can always resort to Boolean-valued models and the likes of that.

And so, for the general mechanism, you don't quite need the assumption of $\sf AC$ for things to work out.

However, you could be talking about independence results in the sense that we want to prove that something is independent by forcing. So, for example, given any model of $\sf ZFC$ it has a forcing extension which satisfies $\sf CH$ and another which does not.

In that sense, forcing will preserve $\sf AC$, and while we can force $\sf AC$ itself over some models of $\sf ZF$, we also know of some models where we simply cannot do it.

Finally, there are concepts that just don't have good definitions without $\sf AC$, for example cardinal characteristics of the continuum, and that requires further explorations and work before we can say something concrete about the independence and the techniques that we use.

But overall, if something is independent of $\sf ZFC$, it will be independent of $\sf ZF$, and in fact, of any weaker theory.