Axioms for induction with nonnegative integers

Question

Which axioms are assumed to hold for any standard inductive proof of a formula using only nonnegative integers (e.g. of $1+2+\ldots+n=\frac{n(n+1)}{2}$, where $n\ge0$) ? For example, are Peano axioms assumed to hold for this proof by induction?

Answer 1

First of all, an elaboration of Mercio's comment: in the language of $PA$, there is no direct way to talk about something like "$1+2+...+n$". That's simply not something $PA$ can express.

. . . without work. It turns out we can talk about finite sequencs in $PA$, and hence summations. But this takes real effort - Goedel was the first to do this in his proof of the incompleteness theorem, and it involved clever use of the Chinese Remainder Theorem.

So even expressing the theorems you want to prove in the language of PA is hard. However, once we've done so, it turns out that very few PA-axioms are actually needed.

PA consists of basic algebraic axioms (together called $P^-$), together with an induction scheme. By restricting attention to certain types of formulas in the induction scheme, we get a family of weak versions of PA - for instance, $I\Sigma_1$ is the theory gotten from $P^-$ by adding induction for $\Sigma_1$ formulas. $I\Sigma_1$ is enough to run essentially every "basic" induction argument, including the one you describe.

The study of exactly how much induction is needed to prove a given theorem is part of Reverse Mathematics.

Answer 2

It wouldn't be easy, but you should eventually be able to prove the above sum starting with only the usual five Peano Axioms (defining a successor function, but not addition or multiplication), and some set theory and logic.

To do so, you would first need to construct the addition and multiplication functions on $N$ as well as the finite summation operator. Then you should be able to formally prove your sum by induction. Note that the principle of mathematical induction is included in the Peano's Axioms.

To give you an idea of the magnitude of such a task, here is just my formal construction of the addition function on $N$ starting from Peano's Axioms: Construct Add on N (727 lines of formal proof). And that's probably only about a quarter of the job done toward your sum!

EDIT: To do even the simplest formal proofs by induction on the natural numbers, you will, of course, need to use the principle of mathematical induction from Peano's axioms which essentially define the set of natural numbers. If you want to prove things about addition, multiplication and summations (as in your example), you will have to define/construct each of these. Older versions of Peano's Axioms included definititions of addition and multiplication. If you are allowed the axioms of set theory, you do not need to include them in your definition of $N$; you can construct them, i.e. you can actually prove their existence.