From: AndrEs Eduardo Caicedo
Newsgroups: sci.math
Subject: Re: Proof of Fermat's Last Theorem
Date: Sun, 25 Oct 1998 12:18:09 -0800
torquemada@my-dejanews.com wrote:
> [...]
> Out of curioisty - does any such theory exist already. Are there any
> interesting theorems about lengths of proofs out there? --
Yes. There is an area of foundations of mathematics, called reverse
mathematics', and there are some theorems along these lines. Some very
interesting are due to Harvey Friedman. They are usually of the form
"Any proof of P in the sistem Q requires at least R steps". Here P can
be a statement depending on a natural number n, and so R can be a
function of n. Q can be a weak system of arithmetic, or something
powerful as ZFC+some strong axioms of infinity. It's possible to go
further and establish results of the form "For any n, the statement P(n)
can be proven in Q, but the proof takes at least R(n) steps". Sometimes,
however, you cannot prove "for all n P(n)" in system Q. This means, for
example, that you cannot prove in Q that R is a total function (ie. for
all n, R(n) exists), or that R grows too fast (so in fact faster than
any function you can prove total in Q).
A concrete example of what I mean by "fast-growing" function:
Ramsey theorem says that for any n,r there is an m such that for any
coloring of the complete graph on m vertices with r colors, there is a
complete monochromatic subgraph with n vertices.
We can prove in PA (Peano Arithmetic) that the function R(n,r)="least
such m" exists.
Paris and Harrington showed in 1978:
Assume you not only have m vertices, but they are numbered (1,2,...,m).
Then you can find a complete monochromatic subgraph with n vertices,
such that n>=least number in any of those n vertices.
Then the function R(n,r)="least such m" cannot be proven to exist in PA.
Of course, given n and r you can prove in PA that R(n,r) exists. But you
cannot prove it at once for all n,r. Given n,r, a proof in PA of the
existence of R(n,r) can take the form: Consider m vertices: 1,...,m, and
all the colorings f:[{1,...,m}]^2->{1,...r}, where [A]^2 is the
collection of 2-subsets (arcs) of the graph with set of vertices A, say
f_1,...,f_s. Then notice that for f_1 the subgraph A_1=... is
monochromatic with color ..., has n vertices, and the least vertex of
A_1 is ... which is smaller than n; for f_2...
Here, the idea is that you fix m in advance, because you have some
external way of knowing that it will work, and then show in PA, in the
worst possible way (listing all cases) that it works.
Of course, this requires a huge number of steps. And you can in general
improve it, but not too much, really.
It requires using some form of the axiom of infinity, which cannot be
proven in PA.
And the number of steps grows as fast as R(n,m).
Another way this theorems take uses Godel's incompleteness theorem. It
states that, for example, we cannot prove in ZFC that ZFC is consistent
(or in PA that PA is consistent, or...).
Now, PA is consistent (let's say we all assume that). Then, for any n,
there is no proof of the inconsistency of PA in at most n steps. For any
n we can prove that in PA. But the proof is awfully long, growing with
n.
There are some papers about this phenomenon. See, for example,
Samuel R. Buss, "On Godel's Theorems on Lenghts of Proofs I: number of
lines and speedup for arithmetics", Journal of Symbolic Logic, Vol 59, N
3, 1994, 737-756.
I don't know if the second part of Buss's paper has been published yet.
P. Pudlak, "Improved Bounds to the lenght of proofs in finitistic
consistency statements", Contemporary Mathematics Vol. 65, "Logic and
Combinatorics", AMS, 1987, 309-332. In fact, almost all the papers in
this book touch this subject.
Or you can visit Harvey Friedman's web-page and take a look at some of
their papers. http://www.math.ohio-state.edu/~friedman/
And there are several other sources, but I think I'll stop here.
Now, as for the question of: 'ok, this is interesting, but I was
wondering about statements like Fermat's Last Theorem'. Then I do not
know. I think some result of reverse mathematics by Simpson can be of
this form, but I don't think there is a general theory which would give
you a result like "Any proof (or disproof) of the Goldbach conjecture in
ZFC requires at least n steps" for some n.
Such a theory has to be very involved, because the usual way that we
logicians measure the complexity of statements, alternation of
quantifiers, say, is of no use here (Buss's paper deals with Pi^0_1
statements, which are at the bottom of the hierarchy).
AndrEs Caicedo