Fermat, set theory, and arithmetic (guest post by Colin McLarty)

This is a guest post by Colin McLarty, Truman P. Handy Professor of Intellectual Philosophy and professor of Mathematics at Case Western Reserve University. It is a follow-up to a short post I wrote last month on his exciting current work on the foundations of mathematics. In this post, Colin explains to us what the whole project is about in just 1000 words.

--------------

Some philosophers suspect mathematicians don't care about foundations but only care about what works. But that elides the problem mathematicians constantly face: what will work? And it can promote the misapprehension that modern mathematics abandons intuition in favor of technicalities. Mathematics works by making rigor serve intuition.  Mathematicians use tools that help them see how to do what they want---without breaking down even in what I will call "deliberate, utterly reliable gaps".

By that I mean points in an argument where a mathematician cites a substantial, hard to prove result where the citing mathematician may or may not have once gone through the whole proof of that result but certainly is not calling the whole proof to mind in citing it.  The citing mathematician relies on that earlier result not only to be proved correctly, but to be stated in full precision so it can be applied concisely out of context without fear of error. Major proofs today have many deliberate utterly reliable gaps, as do their citations in turn.

These themes converged in the on-line row over whether Wiles’s proof of Fermat's Last Theorem (FLT) uses Grothendieck universes. Universes are controversial in some circles since they are sets large enough to model Zermelo Fraenkel set theory (ZF) and so, by Gödel's incompleteness theorem, ZF cannot prove they exist.

The term "universe" is not in Wiles's paper. Neither are proofs of most theorems he uses.  He gives citations which cite others in turn.  The citations often lead to the works where Grothendieck and colleagues established the modern methods of number theory (and about half of today’s category theory) using universes. As he depended on those proofs so he depended on universes.

One way out is never taken. Grothendieck knew everything he does with universes in practice he could also do by discarding some larger scale structures and treating others as mere ways of speaking rather than actual entities. Number theorists often say something like this would put their work on a ZF foundation. But they give no precise statement. And really doing it would distract from arithmetic by offering un-insightful set theoretic complications for no serious foundational benefit. ZF itself is remote from arithmetic.

It is no surprise theoretically that a statement about numbers could be proved by high level set theory.   Gödel showed things like this have to happen sometimes, since any increase in the consistency strength of a foundation makes new number theoretic statements provable.  Consistency itself can be expressed by number theoretic statements. But it is surprising in fact that FLT should be proved this way. We do not expect to see the Gödel phenomenon in such simple statements.  I am working to lessen the surprise in the case of FLT and other recent number theory by bringing the proofs closer to arithmetic. I have formalized the whole Grothendieck toolkit in finite order arithmetic. That is the strongest theory that is commonly called "arithmetic".  From that point of view it is the simple theory of types including an axiom of infinity. From another viewpoint it is the weakest theory that is commonly called "set theory". It is set theory using only numbers and sets of numbers and sets of sets of numbers, all built from numbers in some finite number of levels by bounded comprehension.

The version in my article "A finite order arithmetic foundation for cohomology" looks like Grothendieck’s to anyone but a professional logician. You can just replace a few foundational passages in the Grothendieck work by this foundation. It proves less than Grothendieck’s universes in principle.  But all the general theorems actually in the Grothendieck corpus follow verbatim as Grothendieck and his colleagues proved them.

On the other hand, this foundation is still much stronger than PA. It uses every finite level above PA, though only finite levels.

My current focus is to formalize the central Grothendieck tools at the logical strength of second or third order arithmetic. On one hand this will formalize the insight of practitioners who say their work with these tools really only uses "very small sets". And on the other hand it will bring the foundation within striking distance of methods of reverse mathematics, a well-developed discipline exploring the exact logical strength of mathematical results expressible in second order arithmetic. My article "Zariski cohomology in second order arithmetic" gives some progress on this front.

One goal is to take current methods of number theory, which textbooks and reference works justify by various combinations of Grothendieck universes and hand waving, and justify them rigorously in pretty much their current form in low order arithmetic. Essential to this goal is that most proofs do not get longer and their appearance is not much changed. The other goal is to show that the great number theoretic results proved by these tools can be proved in Peano Arithmetic. It would be great to find proofs in PA without changing the existing proofs very much. But that may not be possible. At any rate it is not intrinsic to the second goal. Showing these theorems can be proved in PA is likely to require serious advances in number theory. I can try to clear up the logical side.

As a philosophical goal I want to show how Grothendieck and many mathematicians since him have cared enough to either develop rigorous foundations for these tools or else to protest foundations they do not like—and others draw on these foundations without needing to highlight them. Grothendieck has been clear that the size of sets is not important to him but the conceptual unity of his toolkit is. I have shown that unity can be preserved without anything like the size of his original universes. I regard Grothendieck as developing the unity of intuition and rigor, in terms very like the post "Terry Tao on rigor in mathematics". I hope others will too.