# What is the proper role of foundations in rigorous mathematics? [Paused] [closed]

[This question needs a major rewrite. Please regard it as 'paused' and inactive until I find the time to clarify the issues of concern. Thank you.]

Suppose we want to write very rigorous mathematics. Then, we need a foundation.

Now the naive approach is to just formalize everything within this foundation. Like, if our foundation is ZFC, then a group is an ordered pair (G,*), encoded as Kuratowski pair or otherwise, and formally speaking * is really a subset of G^3. By defining things in this very rigorous way, we might think that a high level of rigor is thereby achieved.

Actually, this is a really bad way of going about it! It means that if our foundations turns out to be inconsistent, then nothing we've proved in this way (say, about groups) can be trusted anymore. We have to start again from scratch. In reality, of course, we wouldn't need to start again from scratch, because most of the stuff we've proved doesn't need the full power of our foundations after all. For instance, if we're using ZFC as our foundations, well perhaps only 3 out of the 50 theorems we've proved need anything approaching the full power of ZFC, with the other results either following directly from the group axioms, or else being provable in much weaker systems.

Thus, in general, we want to prove things under minimal foundational assumptions, as opposed to committing to one particular foundations and carrying out all our activity therein.

This raises an interesting question. If foundational theories like ZFC are not the right place to formalize definitions like group, field, topological space, etc., then what is the proper role of foundations in rigorous mathematics?

## closed as unclear what you're asking by Joseph Weissman♦Apr 8 '14 at 1:05

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• Most of the question reads as if you ask for various foundational approaches. But the main question is expressed as asking for the role of specific foundations within "rigorous" mathematics. Maybe it's my bad english, but I'm not sure what you're going for. In any case, things like groups can be formalized in the language of logic alone - a set theory is just the carrier which models axioms of interest. And "rigorous" is always relative. To a person in the automated theorem proving field, the majoritiy of math papers aren't rigorous, same with math vs. physics, physics vs. engineering... – Nikolaj-K Jul 22 '13 at 8:11
• @NickKidman, yes the question needs a serious rewrite. I wish there was a 'pause' feature. – goblin Jul 22 '13 at 21:18
• What about the two answers that are already posted? Will your "major rewrite" make them obsolete? – Did Jul 28 '13 at 9:16
• @Did, I don't know. I just asked here about what to do in this situation. – goblin Aug 3 '13 at 5:44
• Ping me whenever you'd like to think about opening this back up. And by the way -- please don't use brackets at the end of headlines like that :) – Joseph Weissman Apr 8 '14 at 1:06

It sounds like you might be interested in the subject of reverse mathematics, in which logicians attempt to determine the exact set of axioms needed to prove a particular theorem.

http://en.wikipedia.org/wiki/Reverse_mathematics

A more general issue is that you're concerned that perhaps ZF[C] is inconsistent. But after all, mathematics was a very successful and rigorous discipline from the days of Archimedes, Eudoxus, and Euclid up until the early 1900's when the axioms of ZFC were agreed on.

ZFC's a relatively recent development, and is already known to be problematic in many ways. Various alternative foundational systems are under development even as we speak. Complexity theory, category theory, and homotopy type theory are just three that come to mind.

If ZFC turned out to be an insufficient or even inconsistent basis of mathematics, the vast majority of working mathematicians wouldn't be too concerned. The classic case is the development of calculus by Newton and Leibniz. It was a spectacularly successful theory; even though its proper logical foundations were not developed for another 200 years.

Conclusion: You do not need a proper foundation in order to do mathematics! This is counterintuitive to modern students who have been trained to regard ZFC as the foundation of math. But historically, discoveries in math precede logical rigor by decades if not centuries.

So the answer to the big picture question you raise is that if ZFC were to be found inconsistent tomorrow, nobody but the foundationalists would care. And they'd just get busy working out a new foundation.

This raises an interesting question. If foundational theories like ZFC are not the right place to formalize definitions like group, field, topological space, etc., then what is the proper role of foundations in rigorous mathematics?

If you invent an algorithm, the empirical approach to prove that you have not left out any important detail is to implement it in an actual programming language. Depending on the used programming language, this can look quite ugly and contingent. However, the deeper problem is that even if your program compiles and works correctly for all problems on which you test it, what does this prove? Well, it forces you to lay down all your cards, so if later something turns out to miss, you can't just claim that it had been there all along and was only not understood correctly.

My point here is that even if ZFC should turn out to correspond to an ugly programming language, it still serves the purpose of a certain kind of rigor good enough, even if this kind of rigor might not be the last word regarding rigor.

Conclusion: Rigor in mathematics has something to do with playing with open cards and not withholding boring details.