The status of the axiom of choice in set theory with a universal set

The purpose of this paper is not to produce a survey of systems with a universal set: we do not yet understand them well enough. Rather it will concentrate on one particular aspect of them: the curious circumstance that there are half-a-dozen or so distinct proofs of ~ AC available in set theories with a universal set. This began to emerge in 1953 when Specker published in [2] a proof of ~ AC in Quine's system NF. Until recently this was an isolated phenomenon and poorly understood. The proof answered few questions and seemed rather ad hoc, thus inviting an investigation to determine whether this was an artefact caused by the particular axioms for NF, or part of a general conflict between the demands of big sets and AC. We will start with an informal discussion of the genesis of set theories with a universal set, collecting, en route, a number of desiderata for such theories. A number of new refutations of AC in systems meeting some or all of these conditions will then be presented. The conclusion the reader is invited to draw is that any sensible set theory with a universal set will probably have trouble with AC. Why do set theory with V e V at all? It contradicts conventional wisdom which teaches us that e is wellfounded. It must be said for this doctrine (let us abbreviate it to WOOF) that it has enabled the rapid execution of the logicist programme, so if that were the sole purpose of set theory we could consider ourselves well served. However most pure mathematicians are platonists and study things not because they are useful but simply because they are there. And the belief that V is not there can, after all, only be the result of early conditioning.