Peano axioms
[2][3] In 1881, Charles Sanders Peirce provided an axiomatization of natural-number arithmetic.
[4][5] In 1888, Richard Dedekind proposed another axiomatization of natural-number arithmetic, and in 1889, Peano published a simplified version of them as a collection of axioms in his book The principles of arithmetic presented by a new method (Latin: Arithmetices principia, nova methodo exposita).
The first axiom asserts the existence of at least one member of the set of natural numbers.
[6] The next three axioms are first-order statements about natural numbers expressing the fundamental properties of the successor operation.
A weaker first-order system is obtained by explicitly adding the addition and multiplication operation symbols and replacing the second-order induction axiom with a first-order axiom schema.
The term Peano arithmetic is sometimes used for specifically naming this restricted system.
[8] The Peano axioms define the arithmetical properties of natural numbers, usually represented as a set N or
[8] The remaining axioms define the arithmetical properties of the natural numbers.
The naturals are assumed to be closed under a single-valued "successor" function S. Axioms 1, 6, 7, 8 define a unary representation of the intuitive notion of natural numbers: the number 1 can be defined as S(0), 2 as S(S(0)), etc.
It is now common to replace this second-order principle with a weaker first-order induction scheme.
However, with first-order induction, this is not possible[citation needed] and addition and multiplication are often added as axioms.
The respective functions and relations are constructed in set theory or second-order logic, and can be shown to be unique using the Peano axioms.
[citation needed] Similarly, multiplication is a function mapping two natural numbers to another one.
[21] In 1936, Gerhard Gentzen gave a proof of the consistency of Peano's axioms, using transfinite induction up to an ordinal called ε0.
Gentzen's proof is arguably finitistic, since the transfinite ordinal ε0 can be encoded in terms of finite objects (for example, as a Turing machine describing a suitable order on the integers, or more abstractly as consisting of the finite trees, suitably linearly ordered).
Whether or not Gentzen's proof meets the requirements Hilbert envisioned is unclear: there is no generally accepted definition of exactly what is meant by a finitistic proof, and Hilbert himself never gave a precise definition.
A small number of philosophers and mathematicians, some of whom also advocate ultrafinitism, reject Peano's axioms because accepting the axioms amounts to accepting the infinite collection of natural numbers.
Curiously, there are self-verifying theories that are similar to PA but have subtraction and division instead of addition and multiplication, which are axiomatized in such a way to avoid proving sentences that correspond to the totality of addition and multiplication, but which are still able to prove all true
[24] The arithmetical operations of addition and multiplication and the order relation can also be defined using first-order axioms.
The above axiomatization of Peano arithmetic uses a signature that only has symbols for zero as well as the successor, addition, and multiplications operations.
Finally, Peano arithmetic PA is obtained by adding the first-order induction schema.
Essential incompleteness already arises for theories with weaker axioms, such as Robinson arithmetic.
Undecidability arises already for the existential sentences of PA, due to the negative answer to Hilbert's tenth problem, whose proof implies that all computably enumerable sets are diophantine sets, and thus definable by existentially quantified formulas (with free variables) of PA. Formulas of PA with higher quantifier rank (more quantifier alternations) than existential formulas are more expressive, and define sets in the higher levels of the arithmetical hierarchy.
Although the usual natural numbers satisfy the axioms of PA, there are other models as well (called "non-standard models"); the compactness theorem implies that the existence of nonstandard elements cannot be excluded in first-order logic.
[28] The upward Löwenheim–Skolem theorem shows that there are nonstandard models of PA of all infinite cardinalities.
[29] This illustrates one way the first-order system PA is weaker than the second-order Peano axioms.
The answer is affirmative as Skolem in 1933 provided an explicit construction of such a nonstandard model.
On the other hand, Tennenbaum's theorem, proved in 1959, shows that there is no countable nonstandard model of PA in which either the addition or multiplication operation is computable.
[30] This result shows it is difficult to be completely explicit in describing the addition and multiplication operations of a countable nonstandard model of PA.
However, the induction scheme in Peano arithmetic prevents any proper cut from being definable.
