I noticed that there is an axiom that says that if $S(n)\implies S(n+1)$, and $S(1)$ is true, then $\forall n \in \Bbb N, S(n).$

My question is why is this an axiom? why can't we derive this from the other axioms?

Bram28 06/12/2018.

If you're looking at the Peano axioms for Arithmetic, and by 'the other axioms' you mean:

$1. \bf{\forall x \ \neg s(x) = 0}$

$2. \bf{\forall x \forall y (s(x) = s(y) \rightarrow x = y)}$

$3. \bf{\forall x \ x+0=x}$

$4. \bf{\forall x \forall y \ x+s(y)=s(x+y)}$

$5. \bf{\forall x \ x\cdot0=0}$

$6. \bf{\forall x \forall y \ x\cdot s(y)=(x \cdot y) + x}$

then no, we can't derive the axiom of induction, which I'll formalize as:

$\bf{(S(0) \land \forall x (S(x) \rightarrow S(s(x))))\rightarrow \forall x \ S(x)}$ (I include $0$ in $\mathbb{N}$, so base is $\bf{S(0)}$)

Here is a counterexample:

Take $\bf{S(x): s(x) \not = x}$

By axiom $1$, we have $\bf{\neg s(0)=0}$, and hence we have $\bf{S(0)}$

Also, if we have $\bf{S(k)}$, i.e. if we have $\bf{s(k) \not = k}$, then if it would be true $\bf{s(s(k)) = s(k)}$, then by Axiom 2 we have $\bf{s(k)=k}$, which contradicts $\bf{S(k)}$, and so we have $\bf{s(s(k)) \not = s(k)}$, i.e. $\bf{S(s(k))}$

OK, so with this $S(x)$, we have $\bf{S(0) \land \forall x (S(x) \rightarrow S(s(x)))}$ simply by virtue of Axioms 1 and 2 alone.

But, we do not necessarily have $\bf{\forall x \ S(x)}$

Consider a model with domain $\mathbb{N} \cup \{ q \}$, i.e. the natural numbers together with some 'extra' element $q$.

Interpret the $\bf{0}$ constant symbol as $0$

Interpret the $\bf{s}$ function symbol as a function $f$ for which $f(n)=n+1$ for any $n \in \mathbb{N}$, and for which $f(q)=q$

Interpret the $\bf{+}$ function symbol as a function $g$ for which $g(m,n)=m+n$ and $g(m,q)=g(q,n)=g(q,q)=q$ for any $m,n \in \mathbb{N}$

Interpret the $\bf{\cdot}$ function symbol as a function $h$ for which $h(m,n)=m\cdot n$ for any $m,n \in \mathbb{N}$, for which $h(0,q)=h(q,0)=0$, and for which $h(m,q)=h(q,n)=q$ for any $m, n \in \mathbb{N}\setminus \{ 0 \}$

Then it is easily verified that all $6$ axioms are satisfied, and hence under this interpretation it is true that $\bf{S(0) \land \forall x (S(x) \rightarrow S(s(x)))}$. But, since $f(q)=q$, it is false that $\bf{\forall x \ s(x) \not = x}$. Hence, it is false that $\bf{S(0) \land \forall x (S(x) \rightarrow S(s(x))))\rightarrow \forall x \ S(x)}$, i.e. the axiom of induction would not hold under this interpretation. Therefore, the axiom of Induction does not follow from axioms $1$ through $6$.

Noah Schweber 06/12/2018.

Ultimately the way we prove (usually) that a given axiom $\alpha$ isn't already a consequence of a set of axioms $T$ is by constructing a **model** *(I've linked to a formal definition, but you should skip it at first read - just think of a model informally, as "a thing satisfying the axioms")* of $T$ in which $\alpha$ fails. The most famous example of this is the parallel postulate, which was proved to be independent of the remaining postulates of Euclid via the construction of non-Euclidean geometries.$^1$

Now in our case - I presume you're talking about the theory PA - our theory has two parts:

An "algebraic" part, asserting that the natural numbers form a discrete ordered semiring.

The induction axioms (a "set-theoretic" part).

It's not trivial to construct a model of the former in which the latter can fail, but they exist; see e.g. here or here.

(Incidentally, once we include induction it becomes very difficult to construct models other than the usual one - we can see this, for example, in Tennenbaum's theorem. With Tennenbaum in mind, we actually have a very easy recipe for cooking up discrete ordered semirings where induction fails: simply pick any "easily describable" discrete ordered semiring not isomorphic to $\mathbb{N}$!)

$^1$I don't want to give the wrong impression here: independence results can be extremely difficult to establish, since the more complicated a theory is the harder its models are to describe in general. For example, at a much more advanced level this is also how we show that the continuum hypothesis is independent of the usual axioms of set theory, assuming the latter are consistent of course. Godel constructed the inner model $L$ and showed that it satisfied CH; later, Cohen developed forcing and showed that it could produce models where CH fails *(as well as models where CH holds, but the former is more impressive: besides being the remaining missing piece, one consequence of Godel's work was that establishing the consistency of the failure of CH is in a precise sense harder than establishing the consistency of CH)*. However, unlike non-Euclidean geometry and slightly unusual discrete ordered semirings, models of set theory are hideously complicated and there's no good way to describe these results without *lots* of technical work.

I. J. Kennedy 06/12/2018.

The Peano Postulates describe what we want the natural numbers to look like. One thing we want is for the natural numbers to be one continuous stream

`0, 1, 2, 3, ...`

and not made up of several infinite sequences like

`0, 1, 2, 3, ..., 0', 1', 2', ...`

where every number has a successor and arithmetic works fine, but if you start counting somewhere in the first sequence you'll never arrive at any number in the second (primed) sequence.

The induction axiom forbids this situation by saying that for every number N, if you start counting from 0 you'll eventually reach N.

Arnaud Mortier 06/12/2018.

The short answer is that without an axiom, there is a difference between

$$\text{You can have as many apples as you want.$^*$}$$ and $$\text{You can have infinitely many apples.}$$

$^*$$\scriptsize\text{(finite amount implied)}$

Mark Wildon 06/12/2018.

It is maybe helpful to think in terms of formal proofs. For each particular $n$, a formal proof of $S(n)$ looks something like this:

$$\begin{align*} S(1), S(1) &\implies S(2)\\ S(2), S(2) &\implies S(3)\\ &\vdots \\ S(n-1), S(n) &\implies S(n) \end{align*}$$

which we use *modus ponens* to go from each line to the next, and $S(i) \implies S(i+1)$ is short-hand for a formal proof of this statement, using the other (non-inductive) axioms in your chosen system.

But although we can give a formal proof of $S(n)$ for each $n \in \mathbb{N}$, there is nothing above that comes close to a formal proof of the formula $(\forall n \in \mathbb{N}) S(n)$.

To put it another way: formal proofs are finite objects, so there is no sense in which we can 'roll-up' the proofs for each particular $n$ into a single formal proof dealing with all $n$ at once. Instead we need the axiom of induction.

- Why do we take the axiom of induction for natural numbers (Peano arithmetic)?
- Induction as Peano Axiom
- What constitutes an axiom - Spivak Calculus ch. 1
- When is first order induction valid?
- Why is the Generalization Axiom considered a Pure Axiom?
- The necessity of the axiom of induction
- Peano axioms-Mathematical Induction
- Does Axiom of Power Set implies Axiom of Subset?
- Why is induction an axiom?
- Axiom of Choice — Why is it an axiom and not a theorem?
- How does induction fail in computable nonstandard models?
- Is Induction Independent of the Other Axioms of PA?

- Is it always better to use the whole dataset to train the final model?
- Why am I getting "Received fatal alert: protocol_version" or "peer not authenticated" from Maven Central?
- Generate a deck of cards
- The right using of Lightning helpers
- Should I let my former undergraduate advisor know that my PhD advisor was abusive?
- Can capybaras spread to Louisiana from Venezuela and populate it in less than 1000 years?
- What are the software logos in MORICONS.DLL?
- Handling critical hits easily when using average damage
- HR is asking for verification of a degree I lied about. What can I do?
- How to ask WolframAlpha to find 'x such that p=32*x+1 is prime'
- Responding to people questioning my single status?
- Funny and simple exam questions
- Don't confuse me with the one about chickens!
- How can one make multiple opportunity attacks during one round?
- What is the best way to transfer $100 into a family member's US bank account on a daily basis?
- Mosquito Armageddon
- Saints: sanctus or divus?
- Using TikZ spy in 3D
- Bitcoin public keys from uncompressed to compressed version with code sample
- Open my mouth and twist my ear
- What is Canada's case for applying tariffs on US dairy?
- Writing a Satisfying Ending
- What to do / tell guests when you don't have enough food for all of them?
- ASCII art uncompression from a base-n number