[FOM] Eliminating AC

[Ali Enayat]

This is a reply to Joe Shipman's queries, especially the most recent
one (March 24) concerning eliminating AC from ZFC-proofs of
arithmetical statements.

Earlier replies (by Smorynski, Eskew, Solovay, Caicedo, and McLarty)
suggested the use of L (the class of constructible sets) and/or HOD
(the class of hereditarily ordinal definable sets) to get the job
done, via appropriate relativization and absoluteness considerations.

In his most recent query, Shipman has asked if there is a proof of
eliminability of AC for arithmetical statements that do not involve
the use of absoluteness and inner models.

I doubt that an "elementary" proof of eliminability of the *general*
sort that Shipman is asking for can be provided; in contrast, for any
concrete ZFC-provable arithmetical statement, it is perfectly
reasonable to ask for a ZF-proof that does not involve a detour of
overt considerations of absoluteness and inner models.

To put this matter in historical perspective, let me note that, to my
knowledge, the first person who went on record to note that if ZFC+
(G)CH proves an arithmetical statement S, then there is a ZF-proof of
S, was George Kreisel, who considered it as a notable application of
advanced methods of metamathematics to mathematics. Kreisel wrote:

"A consequence of Gödel's work on the consistency of the axiom of
choice and the continuum hypothesis is this: if an arithmetical theorem
can be proved in standard set theory from these axioms it can also be
proved without them: one 'relativises' the proof to so-called constructible
sets and classes, and observes that an arithmetical theorem is its
own relativised form since the integers are absolute. In particular, this
applies to recent work on the order of homotopy groups where the
axiom of choice is applied to certain vector spaces of the power of the
continuum; for, by means of simplicial mappings, the order of a
homotopy group can be expressed in an arithmetical proposition."

The above quote is from p.165 of Kreisel's "Some uses of
metamathematics" (British Journal for the Philosophy of Science, Vol.
7, No. 26, Aug., 1956, pp. 161-173), which is a review of Abraham
Robinson's book Théorie métamathématique des idéaux (Paris, 1955).

Best regards,

Ali Enayat