What is the dependency hierarchy in foundational mathematics?
I am confused how different frameworks build on each other, or if there are any frameworks that are circular and we just sort of handwave it away.
What is the order of what builds on what in terms of:
- Propositional logic
- First order logic
- Second order logic
- Set theory
- Functions
- Peano axioms
- Peano arithmetic (or is this not technically a separate thing)
I can't tell what is based on what, what builds on what, etc. Are there circularities? Is there a linear pathway through these things in some order? Is there a straight answer on this?
Solution 1:
You start by having ordinary mathematical reasoning, in words and probably arithmetic and algebraic expressions. Hopefully you have some experience of how to use ordinary mathematical reasoning to develop something like real analysis or other undergraduate topics.
The task is now to use those ordinary mathematical tools to build a formal model of mathematical reasoning itself. The model will help us learn interesting things about the inherent limits of mathematical reasoning, but with all your might resist the impulse to think that the model is "what is really going on" in ordinary mathematical argument. It is a model, not a divine higher truth!
Building of the model generally goes like this:
Propositional logic, mostly as a warm-up, to introduce the ideas of a formal language, the structure of formal proofs and so forth.
First-order logic. This incorporates most of the work we've done in propositional logic -- but not in the sense of being an "application" of propositional logic. Rather, most of the rules of propositional logic are taken over to become rules of first-order logic too.
In order to use first-order logic we need a particular first-order theory that gives us a vocabulary and axioms to reason from. The most important options from a foundational point of view are:
Peano arithmetic. This is a first-order theory, that is, an application of first-order logic, for speaking about arithmetic on the natural numbers.
An axiomatic set theory such as ZFC. This is a first-order theory, that is, an application of first-order logic, for speaking about sets -- and by extension everything that can be modeled as sets, which turns out to be almost all of ordinary mathematics.
At this point it turns out that with ZFC we have enough to let us build formal models of essentially all arguments that are considered valid in ordinary mathematical reasoning. In particular ZFC can model the process that constructed ZFC itself. This ability to "be circular" has important technical applications; it is a desirable feature rather than a problem. (In fact PA can do this too, or at least do it well enough for many of the technical applications).
Second-order logic is more specialized. It is possible to dismiss it as just an impoverished subset of set theory, but being weaker than set theory has some benefits, partly technical, partly philosophical. Pretty much nobody attempts to formalize all of everyday mathematics in second-order logic -- though reverse mathematics is an investigation of how far in that direction you can get with just something that looks like the Peano axioms and second-order logic, but without a full set theory.
The Peano axioms were proposed before the full development of formal logic; today they are usually seen as a particular second-order theory about the natural numbers. For most purposes they are overshadowed by the first-order Peano Arithmetic that gets its name from them.
Functions are important objects of study in ordinary informal mathematics. As such we ought to have some understanding of them before we start metamathematics. Some of the things in formal logic are intended to be interpreted as functions. Set theory can model more even more functions.
Some further relevant writings:
How to avoid perceived circularity when defining a formal language?
Why can we use induction when studying metamathematics?