[FOM] Global Choice, Again

[Ali Enayat]

I am writing to update my recent postings on this topic (April 5 and
8), and to comment on a question posed by Linnebo (April 9).

1. First a historical clarification: according to Rubin-and-Rubin's
monograph on the equivalents of the axiom of choice (1985 edition, p.
xii), the list of people who independently came up with the forcing
proof of the conservativity of global choice over local choice in the
ZF context includes (in alphabetical order): Cohen, Felgner, Grishin,
Jensen, Kripke, and Solovay. Among these, only Felgner and Grishin
published full  accounts (the latter in the former Soviet Union, in
1972), but Cohen mentions the result on p.77 of his 1966 text Set
Theory and the Continuum Hypothesis.

2. It is well-known that GB (Godel-Bernays) is conservative over ZF
(Novak, 1948); but GB turns out to have "super-exponential speed-up"
over ZF (Pudlak 1986, using on a key lemma due independently to
Solovay and Vopenka). This motivates the question:

Does ZF+ global choice have superexponential speed-up over ZFC?

Avigad (Formalizing forcing arguments in subsystems of second-order
arithmetic, Annals of Pure and Applied Logic, 82:165-191, 1996) has
shown that certain conservativity results obtained by forcing
constructions do not necessarily lead to superpolynomial speed-up,
e.g., Harrington's forcing to expand a countable model of RCA_0 to a
model of WKL_0 without introducing new numbers. Perhaps similar
techniques can settle this question.

3. Thomas Forster (April 7) asked about the role of the foundation
axiom in the conservativity result mentioned in (1) above. In my
previous posting I expressed my strong suspicion that foundation is
not needed for the proof. As it turns out, I was "half-right", as I
will explain below.

Felgner addresses this very question in section 5 of his 1976 paper
(published in Sets and Classes, edited by G.H. Muller). He shows that

GB + GC (Godel-Bernays theory of classes with a global choice
function) \ {Foundation}

is conservative over ZF \ {Foundation} plus a scheme of **dependent
choice** for classes (DCC^alpha, for each ordinal alpha, in Felgner's
notation).

Note that in ZF (with Foundation) the schema of dependent choice for
classes is provable from dependent choice for sets, which is itself a
theorem of ZFC [as shown by Levy in his key 1964 paper in which
dependent choice scheme DC^alpha for ordinal alpha>omega were
introduced and studied].

In the same paper, Felgner poses the conservativity of GB\{Foundation}
+ GC over ZFC\{Foundation} as an open question.

Let me add that in the context of second order arithmetic Z_2, a
similar situation arises - but is unrelated to the foundation axiom.
Mostowski showed, using a similar forcing proof, that Z_2 (full second
order arithmetic) plus a global well-ordering of the reals is
conservative over Z_2 plus the full dependent choice scheme DC, but
the issue of whether the DC scheme can be relaxed to the choice scheme
AC is quite subtle and not completely settled; see remark VII.6.4 of
Simpson's Subsystems of Second Order Arithmetic.

4. Linnebo's posting of April 9 points to another related open
question, which can be formulated as follows: Let KMU be the
modification of the Kelley-Morse theory of classes with urelements
that do not necessarily form a set.  Linnebo asks whether in KMU +
"given any two classes A and B, there is either an injection of A to B
or vice-versa" one can prove "There is a global well-ordering".

I do not know the answer to Linnebo's interesting question, but I
would like to point out a related question which might have a known
answer: let NFU be Jensen's urelement-version of Quine's NF. Does the
axiom of choice (which for NFU is equivalent to global choice, since
NFU has a universal set) follow from NFU plus the assumption "given
any two sets A and B, there is either an injection of A to B or
vice-versa" using an appropriate implementation of Hartogs' theorem?

Regards,

Ali Enayat