I have a certain set-theoretic axiom (WISC) which follows from Choice (this is a nuking a fly BTW), but which I suspect is independent of ZF. To show this I need to show that a certain set does not exist. I have no experience with forcing, but I'm willing to learn. I have a plan of attack, but would like to know if it is what I should be doing, or whether some other approach is needed.

Here are the details, and apologies for the vagueness of the questions.

WISC - for every set $S$, there is a set $C_S\subset \{ p:A\to S |\ p\ \mbox{is onto}\}$ such that $$ \forall\ \mbox{surjections }f:B\to S\ \exists (p:A\to S)\in C_S,\ s:A\to B \mbox{ such that } f\circ s = p $$

Clearly, to show this is independent of ZF (or other set-theoretic foundations), we just need a set $S$ such that $C_S$ doesn't exist. We might as well try as a first attempt $S = \mathbb{N}$. If we had a countable model of ZF, if we could force that $C_\mathbb{N}$ was bounded below in size by some uncountable set, and still have a countable model, then I believe we would be done.

Question 1: Is this approach likely to work, or is it too naive?

Notice that one implication of $\lnot$WISC is that there are a proper class of non-split surjections, but this is not sufficient to conclude $\lnot$WISC. Or in the above approach, we would have an uncountable collection of non-split surjections.

Failing the approach above, and in the absence of other options for $\mathbb{N}$, one could step it up a notch and try $C=\mathbb{R}$, but would obviously need a different strategy. Given that I'm familiar in principle with forcing to the level covered in MacLane-Moerdijk (a topos theoretic approach, but not very in-depth),

Question 2: What are good references to get a feel for what one can force along these lines (violations of Choice)?

I'm thinking Blass' paper on SVC might be a good start, but I may need to read something else before that.

I'm trying to show that a particular class is not a set, so perhaps I need to work with NBG + $\lnot$C, and use conservativity over ZF, but given this question: Forcing over models without the axiom of choice, one might suppose that forcing over foundations without Choice other than ZF is even rarer.

The alternative is to consider a quantitative version of WISC, where the set $C_S$ must have cardinality less than a given (regular) cardinal $\kappa$. In the case that $\kappa$ is inaccessible, we can take a Grothendieck universe and so recover the original version of WISC. The presentation axiom/COSHEP is the case when this $\kappa = 2$. Conversely, to show independence, we could just force that $|C_S| \ge \kappa$ for inaccessible $\kappa$, and so show that there is no small set $C_S$ (relative to the universe given by $\kappa$).

Question 3: is this a better way to go about it?

Freyd's models for the independence of the axiom of choice(Mem. Amer. Math. Soc. 79, 1989). – François G. Dorais♦ Oct 31 '11 at 0:37