Forcing the nonexistence of a certain set

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?

• The problem with forcing is that it preserves AC, so you can't force ¬WISC starting with a model of AC. You can make AC fail by passing to a symmetric submodel, but then the technologically simpler permutation models would be the first thing to try. Unfortunately most of these will fail too since set-forcing extensions and set-based permutation models will preserve SVC. So one needs use a symmetric submodel of a class-forcing extension in order to arrive at a model of ¬WISC. There are very few of those around... Oct 31 '11 at 0:20
• @François Well, I mean to start from ZF + $\lnot$C, but I infer from your comment that something in my question means I am secretly accepting Choice somewhere. Is it in the countable model? Oct 31 '11 at 0:35
• By the way, from the categorical point of view, it is harder distinguish between pure forcing extensions, symmetric models, and in-between options. See Blass and Scedrov, Freyd's models for the independence of the axiom of choice (Mem. Amer. Math. Soc. 79, 1989). Oct 31 '11 at 0:37
• @Francois: Do permutation models over a class of atoms act like symmetric submodels of class-forcing extensions? Oct 31 '11 at 0:42
• @David: No, it's that it's customary to start with a model of AC (e.g. L) and then take a symmetric model to do something different. There are very few handy models of ¬AC to start with (and all those I can think of satisfy SVC). Theoretically, you could start with a model where AC fails very badly, but then there is a good chance WISC already fails there without doing anything. Oct 31 '11 at 0:44