An axiom schema is used to generate the axioms, which inductively define the natrual numbers using the empty set and the successor function $S$.

I don't understand why you have to define this set as part of the axioms or at least why this is how it's done. If you define the successor function in the axioms, can't you just then define $1,2,3,4...$ and so on whithin the theory?


I believe that you are talking about a popular first order axiomatization of some fragment of the theory of natural numbers, known as Peano Arithmetic.
First order means that the language only allows quantification over elements of the structure, in this case the natural numbers, but not over subsets of the structure.

If you allow quantification over subsets, finitely many axioms suffice to axiomatize the natural numbers. The tricky part here is induction, which is axiomatized in second order logic, i.e., with quantification over subsets, by saying:

For all sets $A$, if $A$ contains $0$ and is closed under taking successors, then $A$ is the set of all natural numbers.

It is impossible to formalize this is first order logic.
However, there is an approximation of this axiom: Essentially you say that every definable set of natural numbers has the property that if it contains $0$ and is closed under successors, then it consists of all natural numbers.

This can however not be expressed by a single axiom and requires an axiom schema consisting of infinitely many axioms. Namely, you need an extra axiom for each definition of a definable set.

Note that writing down an axiom schema usually requires a recursive definition of formulas. Since you want to define the natural numbers in order to be able to do recursion (for example) you might be unhappy with this.
But we need to base our development of formal mathematics on something, and in this case we base it on the fact that we know how to manipulate finite strings. I hope this clarifies things.

  • $\begingroup$ Of course in a specific sense it is possible to quantify over subsets in first-order logic; "second-order arithmetic" is a first-order theory, and ZFC is a first-order theory. The key point for the finite axiomatization is not the axioms, its the special (non-first-order) semantics that are used to make those axioms categorical. The same axioms are (syntactically) fine in first-order logic, they just aren't categorical. This isn't to disagree with the content of the post; I just think this issue tends to be misunderstood in populatizations. $\endgroup$ Jul 20 '12 at 0:25

The natural numbers are often defined as a model of some basic axioms in the language in which there is a function $S(x)$ and a constant $0$.

We define the axioms to be:

  1. $\forall x.S(x)\neq 0$.
  2. $\forall y\exists x.y=S(x)\lor y=0$.
  3. $\forall x\forall y.S(x)=S(y)\rightarrow x=y$.

In the informal level with can think of $S(x)=x+1$, this function is such that no natural number has $0$ as a successor, it is an injective function and every nonzero number is a successor of someone.

The axiom schema is to add the inductive properties of the natural numbers. This can be seen under the definition of an inductive set:

Let $A\subseteq\mathbb N$. We say that $A$ is an inductive set if:

  • $0\in A$,
  • If $n\in A$ then $S(n)\in A$.

What we would like to have that every inductive set equals to $\mathbb N$. This would be formalized as: $$\forall A.(0\in A\land \forall n.(n\in A\rightarrow S(n)\in A))\rightarrow \forall x.x\in A$$

The above says that for every subset of the universe, if it is inductive then it is equal to $\mathbb N$. However quantification over subsets is forbidden in first-order logic. We can only quantify over elements of the universe.

This is solved by an axiom schema, we say that if $P(x)$ is a predicate and $A=\{n\mid P(n)\}$ is an inductive set then $A=\mathbb N$. Since we cannot quantify over all the formulae either this becomes a schema instead (which we can "compute" whether or not an axiom is from the schema or not).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.