|
|
Re: Axiomization of Number Theory
Posted:
Jul 31, 2003 4:40 AM
|
|
I wrote:
|I've been told that Wiles' proof rests on a result that was proven using
|the consequence of the axiom of choice that a certain extension of the
|p-adics which is both algebraically closed and complete in the p-adic
|metric is isomorphic as a field to (a subset of?) the complex numbers.
|Now, we know that any proof of Fermat's Last Theorem (or even of the
|modularity conjecture) which uses the axiom of choice doesn't really need
|it. But I don't know whether there's any non-messy automatic way of
|extracting it from the proof.
In article <3F282AAE.9020303@wanadoo.fr>, Andrew Boucher
<Helene.Boucher@wanadoo.fr> writes:
|David C. Ullrich wrote:
|>On Wed, 30 Jul 2003 20:45:00 +0200, Andrew Boucher
|><Helene.Boucher@wanadoo.fr> wrote:
[...]
|>>Shouldn't Wiles proof goes through in second-order PA ?
|>
|>Supposing for the sake of argument that Keith was correct
|>when he said that there's no formal system for second-order
|>logic corresponding to the well-known formal systems for
|>first-order logic, exactly what does it mean for something
|>to go through in second-order PA?
|>
|>>If it doesn't, then I'm afraid here's one vote for saying he hasn't
|>>really proved FLT, and JH still has a chance.
|
|It means, can it be proved in the system PA2, second-order Peano
|Arithmetic?
Saying that if it didn't, you wouldn't count it as a proof strikes me as
unduly paranoid about "PA_3" or "PA_4" (say). Do you really think that the
impredicativity involved in talking about sets of sets of natural numbers
(defined by phrases which casually quantify over sets of sets of natural
numbers) poses a meaningful possibility of introducing an error? Of course
we would enjoy seeing an elementary proof, but not for this reason.
I would be very surprised if it couldn't be proven in PA_2. The objects it
mainly is concerned with encode pretty straightforwardly either as integers
or as sequences of integers. A modular form is essentially an infinite
series in this context, for example. A sequence of complex numbers
(coefficients) can be encoded as a sequence of integers. I believe the
mentioned workaround (which I don't happen to know) shows a way out of
using AC, which doesn't require referring to w_1 or whatever.
On the other hand, I think such a translation has a certain messiness to
it. I think it could be fairly tedious to verify with any care. Here's an
example.
I've had described to me a place in the deformation theory where the Freyd
special adjoint functor theorem is applied. The Freyd special adjoint
functor theorem gives a sufficient condition for a functor to have an
adjoint. Half of the condition is one of the usual consequences of a
functor having an adjoint. The other half is one of these conditions which
hinges on something being a set rather than a proper class. For example,
when using Freyd to show that there's such a thing as the free group on a
set of generators, the condition being used is that given a group G, there
exists a _set_ of maps {G->H_i} with the property that any homomorphism
G->K factors through one of them, G->H_i->K. One choice for that is a set
of groups including each isomorphism class of groups of cardinality no
greater than G, with all possible homomorphism from G to them. (We could
consider alternative group laws on subsets of the underlying set of G.)
Obviously, a *class* of such maps exists (take all of them), but for the
theorem to work we need there to be a *set*.
This abstraction is what we get for having had Grothendieck work on
algebraic geometry. :-) I believe the place where my acquaintance said it
was being used is where there are functors from the category of rings to
the category of sets: a functor giving the set of either elliptic curves
or modular forms with certain properties, having coefficients in the given
ring. Luckily, only certain appropriate rings need to be considered, or
we'd have to cope somehow also with the issue of what a functor from one
big category (i.e., whose objects form a proper class) to another one
really is.
Anyhow, I don't think there's any actual "gotcha" involved in the way this
lemma is used, but to be rigorously confident that it can all be done with
PA_2 one would have to think it all over carefully in the context where
it's used.
And to return to my original point, there's some value in trying to make
an axiom system within which some proofs can be translated *and still
look like the same proof* (unlike a complete translation of this proof
into PA_2). I admit I had forgotten the O.P. wanted to do automatic proof
generation, but even so, trying to get an automatic proof generator to
prove results in an unsuitable language might cause it to thrash.
Keith Ramsay
|
|
