[FOM] Three answers on AC in arithmetic

[Colin McLarty]

There are three questions people ask about eliminating AC in arithmetic
depending on their expertise:

1) A popular question: How do we know the proofs in a good first graduate
course on number theory (say Ireland and Rosen Classical Introduction to
Modern Number Theory) do not need choice?

2)  Serre's question to Kreisel  (if I remember the history correctly) can
we be sure cohomological number theory does not require choice?

3) The question Kreisel answered:  Can we show
every arithmetical statement provable in ZFC is provable in ZF?

The answer to 1 is "by inspection."  The proofs are explicit calculations
albeit some are long and subtle.

The answer to 3 is as Kreisel originally gave it, and several people here
have said,  absoluteness for L of arithmetic statements.  This is
necessarily remote from current methods of number theory, since
the question is posed without regard to any currently known
or conceivable methods of number theory.

This gives a method for actually removing choice from any proof, by giving
the proof in ZF with all quantifiers relativized to L.   But it is a bit
technical and i doubt many number theorists would like to work that way.  I
suspect that most who care about the issue at all would rather just know
you always can work that way in principle.

More specifically number theoretic answers to 2 depend on specifically what
you want to know.

Do you want to remove choice from proofs of, say, the Mordell conjecture,
without going through V=L?  Current proofs use lemmas like "every ring has
a maximal ideal."  Probably every case used of this lemma admits explicitly
definable maximal ideals, so no use of choice.  I do not know what other
ways the published proofs invoke choice.  I expect all can be eliminated in
pretty much that way, but it would be odd to say this is known
"by inspection "  Even today the published proofs are pretty
long, inexplicit on logical details, and not easily "inspected."

The case get more complicated in detail (perhaps not harder in principle,
so far as removing choice goes) if you want etale cohomology.

 When we ask about concrete ways of eliminating choice from known proofs,
but we do not want to get "technical," then we have to say exactly what
means of elimination we consider concrete and what we consider technical.

best, Colin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130326/7c3575f4/attachment-0001.html>