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