[sbazerque]

Arithmetic is usually formalized using first order logic (that's what Godel did in his incompleteness paper, for example).

That means that one can write formulas quantifying only over numbers (that's what's done for the axioms defining addition and multiplication), but in order to get recursion, one needs to use infinite many axioms, one for each predicate P, saying:

if P(0) and (∀n)P(n) => P(n+1) then (∀n) P(n)

Intuitively, this gets us that all the numbers that can be reached starting from zero by using the "+1" operation will follow the rules of arithmetic.

But it does not guarantee that all numbers _can_ be reached this way. In the standard model, the one we have in mind, that is the case, but it turns out that there are constructions like this

0, 1, 2, ... -2', -1', 0', 1', 2' ...

having numbers that came after the ones in the standard model, but that cannot be reached by applying "+1" a finite number of times, where all the axioms of arithmetic are also true, and are therefore also models of arithmetic.

Some formulas are going to be true in one and false in the other, but all those are independent of the axioms of arithmetic. The study of formal methods in mathematics and their limitations is truly fascinating.