Post History

What are the Peano axioms?

According to [Wikipedia](https://en.m.wikipedia.org/wiki/Peano_axioms),

> The nine Peano axioms contain three types of statements. The first axiom asserts the existence of at least one member of the set of natural numbers. The next four are general statements about equality; in modern treatments these are often not taken as part of the Peano axioms, but rather as axioms of the "underlying logic".[6] The next three axioms are first-order statements about natural numbers expressing the fundamental properties of the successor operation. The ninth, final axiom is a second-order statement of the principle of mathematical induction over the natural numbers, which makes this formulation close to second-order arithmetic.

The first axiom I find intuitive: “there exists at least something”.

What are the four axioms regarding equality - the classic properties of reflexivity, transitivity, and symmetry? And the fourth?

How can these be seen as the “underlying logic”? I think my hope was the Peano axioms were fundamental, defined in terms of primitive notions. Now it seems they are axioms written in first order logic (or second order)?

What are the three fundamental properties of the successor operation?

If the ninth axiom is “second-order”, does this mean, if a first order logic has variables restricted to some “domain” (a “domain of discourse”), that a second-order logic has variables whose values are themselves the first-order sentences?

(In which case, I believe the ninth axiom is the way of expressing the “infinitude” of natural numbers in a finite way. If we can assume the existence of any arbitrary “function” (since FOL assumes that), then the “successor function” is not any particular function; just a function, applied successively: f(x), f(f(x)), …). In order to express “do this forever”, we have to express perhaps a recursive rule? F(f(x) = f(f(x)) (where ‘f’ is now a *variable* - ie, these are variables that range over *functions*).


That said: a variant of these axioms, PA1, is considered a first order theory. Whereas the article says these axioms are close but not equal to second order arithmetic. So in what way are the natural numbers in between these two theories?