Peano axioms#First-order theory of arithmetic

{{improve references|date=May 2024}}

When Peano formulated his axioms, the language of mathematical logic was in its infancy. The system of logical notation he created to present the axioms did not prove to be popular, although it was the genesis of the modern notation for set membership (∈, which comes from Peano's ε). Peano maintained a clear distinction between mathematical and logical symbols, which was not yet common in mathematics; such a separation had first been introduced in the Begriffsschrift by Gottlob Frege, published in 1879.{{sfn|Van Heijenoort|1967|page=2}} Peano was unaware of Frege's work and independently recreated his logical apparatus based on the work of Boole and Schröder.{{sfn|Van Heijenoort|1967|page=83}}

The Peano axioms define the arithmetical properties of natural numbers, usually represented as a set N or $\backslash mathbb\{N\}.$ The non-logical symbols for the axioms consist of a constant symbol 0 and a unary function symbol S.

The first axiom states that the constant 0 is a natural number:

{{ordered list|start=1

| 1= 0 is a natural number.

}}

Peano's original formulation of the axioms used 1 instead of 0 as the "first" natural number,{{sfn|Peano|1889|page=1}} while the axioms in Formulario mathematico include zero.{{sfn|Peano|1908|page=27}}

The next four axioms describe the equality relation. Since they are logically valid in first-order logic with equality, they are not considered to be part of "the Peano axioms" in modern treatments.{{sfn|Van Heijenoort|1967|page=83}}

{{ordered list|start=2

| 2= For every natural number x, {{nowrap|1=x = x}}. That is, equality is reflexive.

| 3= For all natural numbers x and y, if {{nowrap|1=x = y}}, then {{nowrap|1=y = x}}. That is, equality is symmetric.

| 4= For all natural numbers x, y and z, if x = y and y = z, then {{nowrap|1=x = z}}. That is, equality is transitive.

| 5= For all a and b, if b is a natural number and {{nowrap|1=a = b}}, then a is also a natural number. That is, the natural numbers are closed under equality.

}}

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.

{{ordered list

| start = 6|

| 6 = For every natural number n, S(n) is a natural number. That is, the natural numbers are closed under S.

| 7 = For all natural numbers m and n, if {{nowrap|1=S(m) = S(n)}}, then {{nowrap|1=m = n}}. That is, S is an injection.

| 8 = For every natural number n, {{nowrap|1=S(n) = 0}} is false. That is, there is no natural number whose successor is 0.

}}

File:Domino effect visualizing exclusion of junk term by induction axiom.jpgGerardo con Diaz, [http://www.math.harvard.edu/archive/23a_fall_05/Handouts/induction.pdf Mathematical Induction] {{Webarchive|url=https://web.archive.org/web/20130502163438/http://www.math.harvard.edu/archive/23a_fall_05/Handouts/induction.pdf |date=2 May 2013 }}, Harvard University However, axioms 1–8 are {{em|also}} satisfied by the set of all dominoes—whether light or dark—taken together.The non-contiguous set satisfies axiom 1 as it has a 0 element, 2–5 as it doesn't affect equality relations, 6 as all pieces have a successor, axiom 7 as no two dominos topple, or are toppled by, the same piece, and axiom 8 as every domino bar the first light domino is toppled by another domino. The 9th axiom (induction) limits N to the chain of light pieces ("no junk") as only light dominoes will fall when the nearest is toppled.

{{sfn|Meseguer|Goguen|1986|loc=sections 2.3 (p. 464) and 4.1 (p. 471)}}]]

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. However, considering the notion of natural numbers as being defined by these axioms, axioms 1, 6, 7, 8 do not imply that the successor function generates all the natural numbers different from 0.

The intuitive notion that each natural number can be obtained by applying successor sufficiently many times to zero requires an additional axiom, which is sometimes called the axiom of induction.

{{ordered list|start=9

| 9=If K is a set such that:

• 0 is in K, and
• for every natural number n, n being in K implies that S(n) is in K,

then K contains every natural number.

}}

The induction axiom is sometimes stated in the following form:

{{ordered list|start=9

| 9=If φ is a unary predicate such that:

• φ(0) is true, and
• for every natural number n, φ(n) being true implies that φ(S(n)) is true,

then φ(n) is true for every natural number n.

}}

In Peano's original formulation, the induction axiom is a second-order axiom. It is now common to replace this second-order principle with a weaker first-order induction scheme. There are important differences between the second-order and first-order formulations, as discussed in the section {{section link||Peano arithmetic as first-order theory}} below.

If we use the second-order induction axiom, it is possible to define addition, multiplication, and total (linear) ordering on N directly using the axioms. However, {{Citation needed span|text=with first-order induction, this is not possible|date=January 2022}} 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.

Addition is a function that maps two natural numbers (two elements of N) to another one. It is defined recursively as:

: $\backslash begin\{align\}$

a + 0 &= a , & \textrm{(1)}\\

a + S (b) &= S (a + b). & \textrm{(2)}

\end{align}

For example:

: $\backslash begin\{align\}$

a + 1 &= a + S(0) & \mbox{by definition} \\

&= S(a + 0) & \mbox{using (2)} \\

&= S(a), & \mbox{using (1)} \\

\\

a + 2 &= a + S(1) & \mbox{by definition} \\

&= S(a + 1) & \mbox{using (2)} \\

&= S(S(a)) & \mbox{using } a + 1 = S(a) \\

\\

a + 3 &= a + S(2) & \mbox{by definition} \\

&= S(a + 2) & \mbox{using (2)} \\

&= S(S(S(a))) & \mbox{using } a + 2 = S(S(a)) \\

\text{etc.} & \\

\end{align}

To prove commutativity of addition, first prove $0+b=b$ and $S(a)+b=S(a+b)$, each by induction on $b$. Using both results, then prove $a+b=b+a$ by induction on $b$.

The structure {{nowrap|(N, +)}} is a commutative monoid with identity element 0. {{nowrap|(N, +)}} is also a cancellative magma, and thus embeddable in a group. The smallest group embedding N is the integers.{{cn|date=May 2024}}

Similarly, multiplication is a function mapping two natural numbers to another one. Given addition, it is defined recursively as:

: $\backslash begin\{align\}$

a \cdot 0 &= 0, \\

a \cdot S (b) &= a + (a \cdot b).

\end{align}

It is easy to see that $S(0)$ is the multiplicative right identity:

:$a\backslash cdot\; S(0)\; =\; a\; +\; (a\backslash cdot\; 0)\; =\; a\; +\; 0\; =\; a$

To show that $S(0)$ is also the multiplicative left identity requires the induction axiom due to the way multiplication is defined:

• $S(0)$ is the left identity of 0: $S(0)\backslash cdot\; 0\; =\; 0$.
• If $S(0)$ is the left identity of $a$ (that is $S(0)\backslash cdot\; a\; =\; a$), then $S(0)$ is also the left identity of $S(a)$: $S(0)\backslash cdot\; S(a)\; =\; S(0)\; +\; S(0)\backslash cdot\; a\; =\; S(0)\; +\; a\; =\; a\; +\; S(0)\; =\; S(a\; +\; 0)\; =\; S(a)$, using commutativity of addition.

Therefore, by the induction axiom $S(0)$ is the multiplicative left identity of all natural numbers. Moreover, it can be shownFor formal proofs, see e.g. :File:Inductive proofs of properties of add, mult from recursive definitions.pdf. that multiplication is commutative and distributes over addition:

: $a\; \backslash cdot\; (b\; +\; c)\; =\; (a\backslash cdot\; b)\; +\; (a\backslash cdot\; c)$.

Thus, $(\backslash N,\; +,\; 0,\; \backslash cdot,\; S(0))$ is a commutative semiring.

The usual total order relation ≤ on natural numbers can be defined as follows, assuming 0 is a natural number:

: For all {{nowrap|a, b ∈ N}}, {{nowrap|a ≤ b}} if and only if there exists some {{nowrap|c ∈ N}} such that {{nowrap|1=a + c = b}}.

This relation is stable under addition and multiplication: for $a,\; b,\; c\; \backslash in\; \backslash N$, if {{nowrap|a ≤ b}}, then:

• a + c ≤ b + c, and
• a · c ≤ b · c.

Thus, the structure {{nowrap|(N, +, ·, 1, 0, ≤)}} is an ordered semiring; because there is no natural number between 0 and 1, it is a discrete ordered semiring.

The axiom of induction is sometimes stated in the following form that uses a stronger hypothesis, making use of the order relation "≤":

: For any predicate φ, if

:* φ(0) is true, and

:* for every {{nowrap|n ∈ N}}, if φ(k) is true for every {{nowrap|k ∈ N}} such that {{nowrap|k ≤ n}}, then φ(S(n)) is true,

:* then for every {{nowrap|n ∈ N}}, φ(n) is true.

This form of the induction axiom, called strong induction, is a consequence of the standard formulation, but is often better suited for reasoning about the ≤ order. For example, to show that the naturals are well-ordered—every nonempty subset of N has a least element—one can reason as follows. Let a nonempty {{nowrap|X ⊆ N}} be given and assume X has no least element.

• Because 0 is the least element of N, it must be that {{nowrap|0 ∉ X}}.
• For any {{nowrap|n ∈ N}}, suppose for every {{nowrap|k ≤ n}}, {{nowrap|k ∉ X}}. Then {{nowrap|S(n) ∉ X}}, for otherwise it would be the least element of X.

Thus, by the strong induction principle, for every {{nowrap|n ∈ N}}, {{nowrap|n ∉ X}}. Thus, {{nowrap|1=X ∩ N = ∅}}, which contradicts X being a nonempty subset of N. Thus X has a least element.

A model of the Peano axioms is a triple {{nowrap|(N, 0, S)}}, where N is a (necessarily infinite) set, {{nowrap|0 ∈ N}} and {{nowrap|S: N → N}} satisfies the axioms above. Dedekind proved in his 1888 book, The Nature and Meaning of Numbers ({{langx|de|Was sind und was sollen die Zahlen?}}, i.e., "What are the numbers and what are they good for?") that any two models of the Peano axioms (including the second-order induction axiom) are isomorphic. In particular, given two models {{nowrap|(N_A, 0_A, S_A)}} and {{nowrap|(N_B, 0_B, S_B)}} of the Peano axioms, there is a unique homomorphism {{nowrap|f : N_A → N_B}} satisfying

: $\backslash begin\{align\}$

f(0_A) &= 0_B \\

f(S_A (n)) &= S_B (f (n))

\end{align}

and it is a bijection. This means that the second-order Peano axioms are categorical. (This is not the case with any first-order reformulation of the Peano axioms, below.)

{{Main|Set-theoretic definition of natural numbers}}

The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as ZF.{{harvnb|Suppes|1960}}, {{harvnb|Hatcher|2014}} The standard construction of the naturals, due to John von Neumann, starts from a definition of 0 as the empty set, ∅, and an operator s on sets defined as:

: $s(a)\; =\; a\; \backslash cup\; \backslash \{a\backslash \}$

The set of natural numbers N is defined as the intersection of all sets closed under s that contain the empty set. Each natural number is equal (as a set) to the set of natural numbers less than it:

: $\backslash begin\{align\}$

0 &= \emptyset \\

1 &= s(0) = s(\emptyset) = \emptyset \cup \{ \emptyset \} = \{ \emptyset \} = \{ 0 \} \\

2 &= s(1) = s(\{ 0 \}) = \{ 0 \} \cup \{ \{ 0 \} \} = \{ 0 , \{ 0 \} \} = \{ 0, 1 \} \\

3 &= s(2) = s(\{ 0, 1 \}) = \{ 0, 1 \} \cup \{ \{ 0, 1 \} \} = \{ 0, 1, \{ 0, 1 \} \} = \{ 0, 1, 2 \}

\end{align}

and so on. The set N together with 0 and the successor function {{nowrap|s : N → N}} satisfies the Peano axioms.

Peano arithmetic is equiconsistent with several weak systems of set theory.{{sfn|Tarski|Givant|1987|loc=Section 7.6}} One such system is ZFC with the axiom of infinity replaced by its negation. Another such system consists of general set theory (extensionality, existence of the empty set, and the axiom of adjunction), augmented by an axiom schema stating that a property that holds for the empty set and holds of an adjunction whenever it holds of the adjunct must hold for all sets.

The Peano axioms can also be understood using category theory. Let C be a category with terminal object 1_C, and define the category of pointed unary systems, US₁(C) as follows:

• The objects of US₁(C) are triples {{nowrap|(X, 0_X, S_X)}} where X is an object of C, and {{nowrap|0_X : 1_C → X}} and {{nowrap|S_X : X → X}} are C-morphisms.
• A morphism φ : (X, 0_X, S_X) → (Y, 0_Y, S_Y) is a C-morphism {{nowrap|φ : X → Y}} with {{nowrap|1=φ 0_X = 0_Y}} and {{nowrap|1=φ S_X = S_Y φ}}.

Then C is said to satisfy the Dedekind–Peano axioms if US₁(C) has an initial object; this initial object is known as a natural number object in C. If {{nowrap|(N, 0, S)}} is this initial object, and {{nowrap|(X, 0_X, S_X)}} is any other object, then the unique map {{nowrap|u : (N, 0, S) → (X, 0_X, S_X)}} is such that

: $\backslash begin\{align\}$

u (0) &= 0_X, \\

u (S x) &= S_X (u x).

\end{align}

This is precisely the recursive definition of 0_X and S_X.

{{Further|Hilbert's second problem|Consistency}}

When the Peano axioms were first proposed, Bertrand Russell and others agreed that these axioms implicitly defined what we mean by a "natural number".{{harvnb|Fritz|1952|loc=[https://books.google.com/books?id=Yl_XAwAAQBAJ&pg=PA137, p. 137]}}
An illustration of 'interpretation' is Russell's own definition of 'cardinal number'. The uninterpreted system in this case is Peano's axioms for the number system, whose three primitive ideas and five axioms, Peano believed, were sufficient to enable one to derive all the properties of the system of natural numbers. Actually, Russell maintains, Peano's axioms define any progression of the form $x\_0,x\_1,x\_2,\backslash ldots,x\_n,\backslash ldots$ of which the series of the natural numbers is one instance. Henri Poincaré was more cautious, saying they only defined natural numbers if they were consistent; if there is a proof that starts from just these axioms and derives a contradiction such as 0 = 1, then the axioms are inconsistent, and don't define anything.{{harvnb|Gray|2013|loc=[https://archive.org/details/henripoincaresci0000gray/page/133 p. 133]}}
So Poincaré turned to see whether logicism could generate arithmetic, more precisely, the arithmetic of ordinals. Couturat, said Poincaré, had accepted the Peano axioms as a definition of a number. But this will not do. The axioms cannot be shown to be free of contradiction by finding examples of them, and any attempt to show that they were contradiction-free by examining the totality of their implications would require the very principle of mathematical induction Couturat believed they implied. For (in a further passage dropped from S&M) either one assumed the principle in order to prove it, which would only prove that if it is true it is not self-contradictory, which says nothing; or one used the principle in another form than the one stated, in which case one must show that the number of steps in one's reasoning was an integer according to the new definition, but this could not be done (1905c, 834). In 1900, David Hilbert posed the problem of proving their consistency using only finitistic methods as the second of his twenty-three problems.{{sfn|Hilbert|1902}} In 1931, Kurt Gödel proved his second incompleteness theorem, which shows that such a consistency proof cannot be formalized within Peano arithmetic itself, if Peano arithmetic is consistent.{{sfn|Gödel|1931}}

Although it is widely claimed that Gödel's theorem rules out the possibility of a finitistic consistency proof for Peano arithmetic, this depends on exactly what one means by a finitistic proof. Gödel himself pointed out the possibility of giving a finitistic consistency proof of Peano arithmetic or stronger systems by using finitistic methods that are not formalizable in Peano arithmetic, and in 1958, Gödel published a method for proving the consistency of arithmetic using type theory.{{harvnb|Gödel|1958}} In 1936, Gerhard Gentzen gave a proof of the consistency of Peano's axioms, using transfinite induction up to an ordinal called ε₀.{{harvnb|Gentzen|1936}} Gentzen explained: "The aim of the present paper is to prove the consistency of elementary number theory or, rather, to reduce the question of consistency to certain fundamental principles". Gentzen's proof is arguably finitistic, since the transfinite ordinal ε₀ 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.

The vast majority of contemporary mathematicians believe that Peano's axioms are consistent, relying either on intuition or the acceptance of a consistency proof such as Gentzen's proof. 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. In particular, addition (including the successor function) and multiplication are assumed to be total. 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 $\backslash Pi\_1$ theorems of PA, and yet can be extended to a consistent theory that proves its own consistency (stated as the non-existence of a Hilbert-style proof of "0=1").{{sfn|Willard|2001}}

All of the Peano axioms except the ninth axiom (the induction axiom) are statements in first-order logic.{{sfn|Partee|Ter Meulen|Wall|2012|page=215}} The arithmetical operations of addition and multiplication and the order relation can also be defined using first-order axioms. The axiom of induction above is second-order, since it quantifies over predicates (equivalently, sets of natural numbers rather than natural numbers). As an alternative one can consider a first-order axiom schema of induction. Such a schema includes one axiom per predicate definable in the first-order language of Peano arithmetic, making it weaker than the second-order axiom.{{sfnp|Harsanyi|1983}} The reason that it is weaker is that the number of predicates in first-order language is countable, whereas the number of sets of natural numbers is uncountable. Thus, there exist sets that cannot be described in first-order language (in fact, most sets have this property).

First-order axiomatizations of Peano arithmetic have another technical limitation. In second-order logic, it is possible to define the addition and multiplication operations from the successor operation, but this cannot be done in the more restrictive setting of first-order logic. Therefore, the addition and multiplication operations are directly included in the signature of Peano arithmetic, and axioms are included that relate the three operations to each other.

The following list of axioms (along with the usual axioms of equality), which contains six of the seven axioms of Robinson arithmetic, is sufficient for this purpose:{{sfn|Mendelson|1997|page=155}}

• $\backslash forall\; x\; \backslash \; (0\; \backslash neq\; S\; (\; x\; ))$
• $\backslash forall\; x,\; y\; \backslash \; (S(\; x\; )\; =\; S(\; y\; )\; \backslash Rightarrow\; x\; =\; y)$
• $\backslash forall\; x\; \backslash \; (x\; +\; 0\; =\; x\; )$
• $\backslash forall\; x,\; y\; \backslash \; (x\; +\; S(\; y\; )\; =\; S(\; x\; +\; y\; ))$
• $\backslash forall\; x\; \backslash \; (x\; \backslash cdot\; 0\; =\; 0)$
• $\backslash forall\; x,\; y\; \backslash \; (x\; \backslash cdot\; S\; (\; y\; )\; =\; x\; \backslash cdot\; y\; +\; x\; )$

In addition to this list of numerical axioms, Peano arithmetic contains the induction schema, which consists of a recursively enumerable and even decidable set of axioms. For each formula {{nowrap|φ(x, y₁, ..., y_k)}} in the language of Peano arithmetic, the first-order induction axiom for φ is the sentence

:$\backslash forall\; \backslash bar\{y\}\; \backslash Bigg(\backslash bigg(\backslash varphi(0,\backslash bar\{y\})\; \backslash land\; \backslash forall\; x\; \backslash Big(\; \backslash varphi(x,\backslash bar\{y\})\backslash Rightarrow\backslash varphi(S(x),\backslash bar\{y\})\backslash Big)\backslash bigg)\; \backslash Rightarrow\; \backslash forall\; x\; \backslash varphi(x,\backslash bar\{y\})\backslash Bigg)$

where $\backslash bar\{y\}$ is an abbreviation for y₁,...,y_k. The first-order induction schema includes every instance of the first-order induction axiom; that is, it includes the induction axiom for every formula φ.

The above axiomatization of Peano arithmetic uses a signature that only has symbols for zero as well as the successor, addition, and multiplications operations. There are many other different, but equivalent, axiomatizations. One such alternative{{sfn|Kaye|1991|pages=16–18}} uses an order relation symbol instead of the successor operation and the language of discretely ordered semirings (axioms 1-7 for semirings, 8-10 on order, 11-13 regarding compatibility, and 14-15 for discreteness):

1. $\backslash forall\; x,\; y,\; z\; \backslash \; (\; (x\; +\; y)\; +\; z\; =\; x\; +\; (y\; +\; z)\; )$, i.e., addition is associative.
2. $\backslash forall\; x,\; y\; \backslash \; (\; x\; +\; y\; =\; y\; +\; x\; )$, i.e., addition is commutative.
3. $\backslash forall\; x,\; y,\; z\; \backslash \; (\; (x\; \backslash cdot\; y)\; \backslash cdot\; z\; =\; x\; \backslash cdot\; (y\; \backslash cdot\; z)\; )$, i.e., multiplication is associative.
4. $\backslash forall\; x,\; y\; \backslash \; (\; x\; \backslash cdot\; y\; =\; y\; \backslash cdot\; x\; )$, i.e., multiplication is commutative.
5. $\backslash forall\; x,\; y,\; z\; \backslash \; (\; x\; \backslash cdot\; (y\; +\; z)\; =\; (x\; \backslash cdot\; y)\; +\; (x\; \backslash cdot\; z)\; )$, i.e., multiplication distributes over addition.
6. $\backslash forall\; x\; \backslash \; (\; x\; +\; 0\; =\; x\; \backslash land\; x\; \backslash cdot\; 0\; =\; 0\; )$, i.e., zero is an identity for addition, and an absorbing element for multiplication (actually superfluous{{NoteTag|"$\backslash forall\; x\; \backslash \; (\; x\; \backslash cdot\; 0\; =\; 0\; )$" can be proven from the other axioms (in first-order logic) as follows. Firstly, $x\; \backslash cdot\; 0\; +\; x\; \backslash cdot\; 0\; =\; x\; \backslash cdot\; (0+0)\; =\; x\; \backslash cdot\; 0\; =\; x\; \backslash cdot\; 0\; +\; 0$ by distributivity and additive identity. Secondly, $x\; \backslash cdot\; 0\; =\; 0\; \backslash lor\; x\; \backslash cdot\; 0\; >\; 0$ by Axiom 15. If $x\; \backslash cdot\; 0\; >\; 0$ then $x\; \backslash cdot\; 0\; +\; x\; \backslash cdot\; 0\; >\; x\; \backslash cdot\; 0\; +\; 0$ by addition of the same element and commutativity, and hence $x\; \backslash cdot\; 0\; +\; 0\; >\; x\; \backslash cdot\; 0\; +\; 0$ by substitution, contradicting irreflexivity. Therefore it must be that $x\; \backslash cdot\; 0\; =\; 0$.}}).
7. $\backslash forall\; x\; \backslash \; (\; x\; \backslash cdot\; 1\; =\; x\; )$, i.e., one is an identity for multiplication.
8. , i.e., the '<' operator is transitive.
9. , i.e., the '<' operator is irreflexive.
10. , i.e., the ordering satisfies trichotomy.
11. , i.e. the ordering is preserved under addition of the same element.
12. , i.e. the ordering is preserved under multiplication by the same positive element.
13. , i.e. given any two distinct elements, the larger is the smaller plus another element.
14. , i.e. zero and one are distinct and there is no element between them. In other words, 0 is covered by 1, which suggests that these numbers are discrete.
15. $\backslash forall\; x\; \backslash \; (\; x\; \backslash ge\; 0\; )$, i.e. zero is the minimum element.

The theory defined by these axioms is known as PA⁻. It is also incomplete and one of its important properties is that any structure $M$ satisfying this theory has an initial segment (ordered by $\backslash le$) isomorphic to $\backslash N$. Elements in that segment are called standard elements, while other elements are called nonstandard elements.

Finally, Peano arithmetic PA is obtained by adding the first-order induction schema.

According to Gödel's incompleteness theorems, the theory of PA (if consistent) is incomplete. Consequently, there are sentences of first-order logic (FOL) that are true in the standard model of PA but are not a consequence of the FOL axiomatization. Essential incompleteness already arises for theories with weaker axioms, such as Robinson arithmetic.

Closely related to the above incompleteness result (via Gödel's completeness theorem for FOL) it follows that there is no algorithm for deciding whether a given FOL sentence is a consequence of a first-order axiomatization of Peano arithmetic or not. Hence, PA is an example of an undecidable theory. 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.

{{Main|Non-standard model of arithmetic}}

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.{{sfn|Hermes|1973|loc=VI.4.3|ps=, presenting a theorem of Thoralf Skolem}} The upward Löwenheim–Skolem theorem shows that there are nonstandard models of PA of all infinite cardinalities. This is not the case for the original (second-order) Peano axioms, which have only one model, up to isomorphism.{{sfn|Hermes|1973|loc=VI.3.1}} This illustrates one way the first-order system PA is weaker than the second-order Peano axioms.

When interpreted as a proof within a first-order set theory, such as ZFC, Dedekind's categoricity proof for PA shows that each model of set theory has a unique model of the Peano axioms, up to isomorphism, that embeds as an initial segment of all other models of PA contained within that model of set theory. In the standard model of set theory, this smallest model of PA is the standard model of PA; however, in a nonstandard model of set theory, it may be a nonstandard model of PA. This situation cannot be avoided with any first-order formalization of set theory.

It is natural to ask whether a countable nonstandard model can be explicitly constructed. 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.{{sfn|Kaye|1991|loc=Section 11.3}} This result shows it is difficult to be completely explicit in describing the addition and multiplication operations of a countable nonstandard model of PA. There is only one possible order type of a countable nonstandard model. Letting ω be the order type of the natural numbers, ζ be the order type of the integers, and η be the order type of the rationals, the order type of any countable nonstandard model of PA is {{nowrap|ω + ζ·η}}, which can be visualized as a copy of the natural numbers followed by a dense linear ordering of copies of the integers.

A cut in a nonstandard model M is a nonempty subset C of M so that C is downward closed (x < y and y ∈ C ⇒ x ∈ C) and C is closed under successor. A proper cut is a cut that is a proper subset of M. Each nonstandard model has many proper cuts, including one that corresponds to the standard natural numbers. However, the induction scheme in Peano arithmetic prevents any proper cut from being definable. The overspill lemma, first proved by Abraham Robinson, formalizes this fact.

{{math theorem|name=Overspill lemma{{sfn|Kaye|1991|pages=70ff.}}|math_statement= Let M be a nonstandard model of PA and let C be a proper cut of M. Suppose that $\backslash bar\; a$ is a tuple of elements of M and $\backslash varphi(x,\; \backslash bar\; a)$ is a formula in the language of arithmetic so that

:$M\; \backslash vDash\; \backslash varphi(b,\; \backslash bar\; a)$ for all b ∈ C.

Then there is a c in M that is greater than every element of C such that

:$M\; \backslash vDash\; \backslash varphi(c,\; \backslash bar\; a).$

}}

{{Portal|Philosophy|Mathematics}}

• Foundations of mathematics
• Frege's theorem
• Goodstein's theorem
• Neo-logicism
• Non-standard model of arithmetic
• Paris–Harrington theorem
• Presburger arithmetic
• Skolem arithmetic
• Robinson arithmetic
• Second-order arithmetic
• Typographical Number Theory

{{NoteFoot}}

{{Reflist}}

{{refbegin}}

• {{cite book

|last= Davis

|first= Martin

|author-link= Martin Davis (mathematician)

|year= 1974

|title= Computability. Notes by Barry Jacobs.

|publisher= Courant Institute of Mathematical Sciences, New York University

}}

• {{cite book

|last= Dedekind

|first= Richard

|author-link= Richard Dedekind

|year= 1888

|title= Was sind und was sollen die Zahlen?

|trans-title= What are and what should the numbers be?

|publisher= Vieweg

|url= http://digisrv-1.biblio.etc.tu-bs.de:8080/docportal/servlets/MCRFileNodeServlet/DocPortal_derivate_00005731/V.C.125.pdf

|access-date= 4 July 2016

|archive-date= 20 October 2016

|archive-url= https://web.archive.org/web/20161020135148/http://digisrv-1.biblio.etc.tu-bs.de:8080/docportal/servlets/MCRFileNodeServlet/DocPortal_derivate_00005731/V.C.125.pdf

|url-status= dead

}}

• Two English translations:
• {{cite book

|last= Beman

|first= Wooster, Woodruff

|year= 1901

|title= Essays on the Theory of Numbers

|publisher= Dover Publications

|url= http://www.gutenberg.org/files/21016/21016-pdf.pdf

}}

• {{cite book

|last= Ewald

|first= William B.

|year= 1996

|title= From Kant to Hilbert: A Source Book in the Foundations of Mathematics

|url= https://books.google.com/books?id=Nt_uAAAAMAAJ

|publisher= Oxford University Press

|pages= 787–832

|isbn= 978-0-19-853271-2

}}

• {{cite book

|last= Fritz

|first= Charles A. Jr.

|year= 1952

|title= Bertrand Russell's construction of the external world

|publisher= New York, Humanities Press

|url= https://archive.org/details/bertrandrussells0000frit

|url-access= registration

}}

• {{cite journal

|last= Gentzen

|first= Gerhard

|author-link= Gerhard Gentzen

|year= 1936

|title= Die Widerspruchsfreiheit der reinen Zahlentheorie

|journal= Mathematische Annalen

|volume= 112

|pages= 132–213

|doi= 10.1007/bf01565428

|others= Reprinted in English translation in his 1969 Collected works, M. E. Szabo, ed.

|s2cid= 122719892

}}

• {{cite journal

|last= Gödel

|first= Kurt

|author-link= Kurt Gödel

|year= 1931

|title= Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I

|journal= Monatshefte für Mathematik

|volume= 38

|pages= 173–198

|url= http://www.w-k-essler.de/pdfs/goedel.pdf

|doi= 10.1007/bf01700692

|others= See On Formally Undecidable Propositions of Principia Mathematica and Related Systems for details on English translations.

|s2cid= 197663120

|access-date= 2013-10-31

|archive-url= https://web.archive.org/web/20180411113347/http://www.w-k-essler.de/pdfs/goedel.pdf

|archive-date= 2018-04-11

}}

• {{cite journal

|last= Gödel

|first= Kurt

|year= 1958

|author-link= Kurt Gödel

|title= Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes

|journal= Dialectica

|volume= 12

|pages= 280–287

|others= Reprinted in English translation in 1990. Gödel's Collected Works, Vol II. Solomon Feferman et al., eds.

|issue= 3–4

|publisher= Oxford University Press

|doi= 10.1111/j.1746-8361.1958.tb01464.x

|doi-access= free

}}

• {{cite book

|last= Grassmann

|first= Hermann Günther

|author-link= Hermann Grassmann

|year= 1861

|title= Lehrbuch der Arithmetik für höhere Lehranstalten

|publisher= Verlag von Theod. Chr. Fr. Enslin

|url= https://books.google.com/books?id=jdQ2AAAAMAAJ

}}

• {{cite book

|last= Gray

|first= Jeremy

|author-link= Jeremy Gray

|year= 2013

|title= Henri Poincaré: A scientific biography

|chapter= The Essayist

|chapter-url= https://books.google.com/books?id=w2Tya9gOKqEC&pg=PA133

|page= 133

|publisher= Princeton University Press

|isbn= 978-0-691-15271-4

}}

• {{cite book

|last= Harsanyi

|first= John C.

|author-link= John C. Harsanyi

|year= 1983

|title= Methodology, Epistemology, and Philosophy of Science

|chapter= Mathematics, the Empirical Facts, and Logical Necessity

|editor1-last= Hempel

|editor1-first= Carl G.

|editor2-last= Putnam

|editor2-first= Hilary

|editor3-last= Essler

|editor3-first= Wilhelm K.

|pages= 167–192

|doi= 10.1007/978-94-015-7676-5_8

|isbn= 978-90-481-8389-0

|s2cid= 121297669

}}

• {{cite book

|last= Hatcher

|first= William S.

|date= 2014

|orig-date= 1982

|title= The Logical Foundations of Mathematics

|url= https://books.google.com/books?id=wf3iBQAAQBAJ&pg=PP1

|publisher= Elsevier

|isbn= 978-1-4831-8963-5

}} Derives the Peano axioms (called S) from several axiomatic set theories and from category theory.

• {{cite book

|last= Hermes

|first= Hans

|year= 1973

|issn= 1431-4657

|isbn= 3-540-05819-2

|title= Introduction to Mathematical Logic

|publisher= Springer

|series= Hochschultext

}}

• {{cite journal

|last= Hilbert

|first= David

|year= 1902

|title= Mathematische Probleme

|trans-title= Mathematical Problems

|journal= Bulletin of the American Mathematical Society

|volume= 8

|issue= 10

|pages= 437–479

|url= https://www.ams.org/journals/bull/1902-08-10/S0002-9904-1902-00923-3/home.html

|translator-first= Maby

|translator-last= Winton

|doi= 10.1090/s0002-9904-1902-00923-3

|doi-access= free

}}

• {{cite book

|last= Kaye

|first= Richard

|year= 1991

|title= Models of Peano arithmetic

|publisher= Oxford University Press

|isbn= 0-19-853213-X

}}

• {{cite book

|last= Landau

|first= Edmund

|author-link= Edmund Landau

|year= 1965

|title= Grundlagen Der Analysis

|publisher= AMS Chelsea Publishing

|others= Derives the basic number systems from the Peano axioms. English/German vocabulary included.

|isbn= 978-0-8284-0141-8

}}

• {{cite book

|last= Mendelson

|first= Elliott

|author-link= Elliott Mendelson

|date= December 1997

|orig-date=December 1979

|title= Introduction to Mathematical Logic (Discrete Mathematics and Its Applications)

|edition= 4th

|publisher= Springer

|isbn= 978-0-412-80830-2

}}

• {{cite book

|last1= Meseguer

|first1= José

|last2= Goguen

|first2= Joseph A.

|date= Dec 1986

|url= https://courses.engr.illinois.edu/cs576/sp2017/readings/background/initiality-induction-computability.pdf

|contribution= Initiality, induction, and computability

|pages= 459–541

|isbn= 978-0-521-26793-9

|editor= Maurice Nivat and John C. Reynolds

|title= Algebraic Methods in Semantics

|location= Cambridge

|publisher= Cambridge University Press

}}

• {{cite book

|last1= Partee

|first1= Barbara

|last2= Ter Meulen

|first2= Alice

|author2-link= Alice ter Meulen

|last3= Wall

|first3= Robert

|year= 2012

|title= Mathematical Methods in Linguistics

|publisher= Springer

|url= https://books.google.com/books?id=d5xrCQAAQBAJ

|isbn= 978-94-009-2213-6

}}

• {{cite book

|last= Peano

|first= Giuseppe

|author-link= Giuseppe Peano

|year= 1908

|title= Formulario Mathematico

|edition= V

|page= 27

|publisher= Turin, Bocca frères, Ch. Clausen

|url= https://archive.org/details/formulairedemat04peangoog

}}

• {{cite journal

|last= Peirce

|first= C. S.

|author-link= Charles Sanders Peirce

|year= 1881

|title= On the Logic of Number

|url= https://archive.org/details/jstor-2369151

|journal= American Journal of Mathematics

|volume= 4

|issue= 1

|pages= 85–95

|doi= 10.2307/2369151

|mr= 1507856

|jstor= 2369151

}}

• {{cite book

|last= Shields

|first= Paul

|year= 1997

|title= Studies in the Logic of Charles Sanders Peirce

|url= https://archive.org/details/studiesinlogicof00nath

|url-access= registration

|chapter= 3. Peirce's Axiomatization of Arithmetic

|chapter-url= https://books.google.com/books?id=pWjOg-zbtMAC&pg=PA43

|editor1-last= Houser

|editor1-first= Nathan

|editor2-last= Roberts

|editor2-first= Don D.

|editor3-last= Van Evra

|editor3-first= James

|publisher= Indiana University Press

|isbn= 0-253-33020-3

|pages= 43–52

}}

• {{cite book

|last= Suppes

|first= Patrick

|author-link= Patrick Suppes

|year= 1960

|title= Axiomatic Set Theory

|publisher= Dover Publications

|isbn= 0-486-61630-4

|url-access= registration

|url= https://archive.org/details/axiomaticsettheo00supp_0

}} Derives the Peano axioms from ZFC

• {{cite book

|last1= Tarski

|first1= Alfred

|author-link1= Alfred Tarski

|last2= Givant

|first2= Steven

|year= 1987

|title= A Formalization of Set Theory without Variables

|series= AMS Colloquium Publications

|volume= 41

|publisher= American Mathematical Society

|isbn= 978-0-8218-1041-5

|url-access= registration

|url= https://archive.org/details/formalizationofs0000tars

}}

• {{cite book

|last= Van Heijenoort

|first= Jean

|author-link= Jean van Heijenoort

|year= 1967

|title= From Frege to Godel: A Source Book in Mathematical Logic, 1879–1931

|publisher= Harvard University Press

|isbn= 978-0-674-32449-7

}}

• Contains translations of the following two papers, with valuable commentary:
• {{cite book

|last= Dedekind

|first= Richard

|author-link= Richard Dedekind

|year= 1890

|title= Letter to Keferstein.

|pages= 98–103

|others= On p. 100, he restates and defends his axioms of 1888.

}}

• {{cite book

|last= Peano

|first= Giuseppe

|author-link= Giuseppe Peano

|year= 1889

|title= Arithmetices principia, nova methodo exposita

|trans-title= The principles of arithmetic, presented by a new method

|pages= 83–97

|url= https://archive.org/details/arithmeticespri00peangoog

|others= An excerpt of the treatise where Peano first presented his axioms, and recursively defined arithmetical operations.

|publisher= Fratres Bocca

}}

• {{cite web

|last= Van Oosten

|first= Jaap

|date= June 1999

|title= Introduction to Peano Arithmetic (Gödel Incompleteness and Nonstandard Models)

|url= https://webspace.science.uu.nl/~ooste110/syllabi/peanomoeder.pdf

|publisher= Utrecht University

|access-date= 2 September 2023

}}

• {{cite journal

|last= Wang

|first= Hao

|author-link= Hao Wang (academic)

|date= June 1957

|title= The Axiomatization of Arithmetic

|journal= The Journal of Symbolic Logic

|volume= 22

|issue= 2

|pages= 145–158

|doi= 10.2307/2964176

|publisher= Association for Symbolic Logic

|jstor= 2964176

|s2cid= 26896458

}}

• {{cite journal

|last= Willard

|first= Dan E.

|author-link= Dan Willard

|year= 2001

|doi= 10.2307/2695030

|issue= 2

|journal= The Journal of Symbolic Logic

|mr= 1833464

|pages= 536–596

|title= Self-verifying axiom systems, the incompleteness theorem and related reflection principles

|url= https://www.cs.albany.edu/~dew/m/jsl1.pdf

|volume= 66

|jstor= 2695030

|s2cid= 2822314

|archive-date= 2020-11-09

|access-date= 2018-06-30

|archive-url= https://web.archive.org/web/20201109033211/http://www.cs.albany.edu/~dew/m/jsl1.pdf

|url-status= dead

}}

{{refend}}

• {{cite book

|last= Buss

|first= Samuel R.

|date= 1998

|editor-last= Buss

|editor-first= Samuel R.

|chapter= Chapter II: First-Order Proof Theory of Arithmetic

|title= Handbook of Proof Theory

|publisher= Elsevier Science

|location= New York

|isbn= 978-0-444-89840-1

}}

• {{cite book

|last= Mendelson

|first= Elliott

|author-link= Elliott Mendelson

|date= June 2015

|orig-date= December 1979

|title= Introduction to Mathematical Logic (Discrete Mathematics and Its Applications)

|edition= 6th

|publisher= Chapman and Hall/CRC

|isbn= 978-1-4822-3772-6

}}

• {{cite book

|last= Smullyan

|first= Raymond M.

|author-link= Raymond M. Smullyan

|title= The Gödelian Puzzle Book: Puzzles, Paradoxes and Proofs

|url= https://books.google.com/books?id=xUapAAAAQBAJ

|date= December 2013

|publisher= Dover Publications

|isbn= 978-0-486-49705-1

}}

• {{cite book

|last=Takeuti

|first=Gaisi

|author-link= Gaisi Takeuti

|date=2013

|title=Proof theory

|location=Mineola, New York

|isbn=978-0-486-49073-1

|edition=Second

}}

• {{cite IEP |poincare |title=Henri Poincaré |first=Mauro |last=Murzi}} Includes a discussion of Poincaré's critique of the Peano's axioms.
• {{cite book |first=Karlis |last=Podnieks |chapter=3. First Order Arithmetic |title=What is Mathematics: Gödel's Theorem and Around |date=2015-01-25 |url=https://dspace.lu.lv/dspace/handle/7/5306 |pages=93–121 }}
• {{springer|title=Peano axioms|id=p/p071880}}
• {{MathWorld | urlname=PeanosAxioms | title=Peano's Axioms}}
• {{cite web |url=http://www.math.uwaterloo.ca/~snburris/htdocs/scav/dedek/dedek.html |title=What are numbers, and what is their meaning?: Dedekind |first=Stanley N. |last=Burris |year=2001 |access-date=2007-03-23 |archive-date=2022-10-26 |archive-url=https://web.archive.org/web/20221026225838/https://www.math.uwaterloo.ca/~snburris/htdocs/scav/dedek/dedek.html |url-status=dead }} Commentary on Dedekind's work.

{{PlanetMath attribution|urlname=pa|title=PA}}

{{Mathematical logic}}

Category:1889 introductions

Category:Mathematical axioms

Category:Formal theories of arithmetic

Category:Logic in computer science

Category:Mathematical logic

hu:Giuseppe Peano#A természetes számok Peano-axiómái