Is it possible to derive the axiom of induction from a construction of the natural numbers?

Question

If I start by constructing the natural numbers formally in a reasonably standard way...

Type: NaturalNumber
Constructors: zero:NaturalNumber;successor(NaturalNumber):NaturalNumber

...rather than axiomatising them, then it is straightforward to derive the first eight Peano axioms as theorems, in the sense that it would be relatively easy to write a verifier to do it. I asked myself then why it isn't possible to derive the ninth axiom, namely the axiom of induction?

My motivation for this is that, if you axiomatise the natural numbers rather than construct them, then as I understand it the axiom of induction is necessary in order to exclude the possibility of non-standard sets of natural numbers. Put simply, it rules out the circle of dominoes and allows only the straight line of dominoes in the following picture:

Wikipedia: Domino effect visualizing exclusion of junk term by induction axiom.jpg

I'm aware of, although can hardly claim to be fully versed in, results such as Dedekind's, namely that with the axiom of induction stated using second order logic the Peano axioms define the natural numbers up to isomorphism. And I'm wondering whether these kinds of meta-logical arguments are needed at least to prove that such a proof as this isn't possible, perhaps?

Answer 1

So, at last, I have what I think is an acceptable answer. I'll write out the vernacular and explain as I go along.

Firstly, the construction of the natural numbers (which would be imported from elsewhere):

Type NaturalNumber

Constructors zero:NaturalNumber;successor(NaturalNumber):NaturalNumber

Next, some abbreviations and declarations:

Abbreviations z for zero,s for successor,Nat for NaturalNumber

Metavariables R,S,T(Nat)

Contexts ρ,σ,τ(Nat)

Next, the rule itself, which you would need if you wanted to prove things by Induction. I'll leave off the proof for a moment:

Rule (Induction)
  Premises
    ρ ⊢ R::P(z)
    σ ⊢ S::P(k)=>P(s(k))
  Conclusion
    τ(n) ⊢ T(n)::P(n)

The first premise ρ ⊢ R::P(z) reads 'given a context ρ, the theorem R proves P(z)'. This is the propositions as types paradigm in action, if you like. The context is the axioms and proven theorems that are referenced by the theorem. Similarly for the second premise. So we are taking as premises for the rule the base case and the induction step. The conclusion τ(n) ⊢ T(n)::P(n) states that for each natural number n, a theorem T(n) can be constructed that proves P(n), given a context τ(n).

So the job is to define these contexts τ(n) and to construct the theorems T(n). I'll give the theorems first:

Theorem (T(z))
  P(z)
Proof
  P(z) from T

Theorem (T(s(k)))
  P(s(k))
Proof
  P(k)=>P(s(k)) from S
  P(k) from T(k)
Therefore
  P(s(k)) by ModusPonens

These are worth a few comments. They would not verify standalone, so to speak, because they both rely on contexts that won't be in the main context. The verifier might return something like the following message (recall that this question is about how to implement a verifier as much as anything):

Theorem T(z) verified but the conclusion P(z) has not been added to the 
main context because T is not in the main context.

These are generic theorems that are structurally correct but do not hold standalone. It should be clear that the context needed for the first to verify fully is just going to be ρ. Similarly for the second theorem. The context that it needs is going to be σ,T(k)::P(k). This leads to the recursive definition of the contexts, which is the crucial bit and comes at the top of the proof that follows:

let τ(z)=T
let τ(s(k))=S,T(k)::P(k)

After the above definitions the proof of the Induction rule itself is broken down into the cases n=z and n=s(k). I'll leave out the derivations which prove the implications for the moment, so as to get across the gist of the proof as a whole:

Proof
  ...
  n=z ∨ n=s(k)
  Suppose
    n=z
  Then
    ...
  Hence
    ρ(n) ⊢ T(n)::P(n)
  n=z => ρ(n) ⊢ T(n)::P(n)

  Suppose
    n=s(k)
  Then
    ...
  Hence
    ρ(n) ⊢ T(n)::P(n)
  n=s(k) => ρ(n) ⊢ T(n)::P(n)

Therefore 
  ρ(n) ⊢ T(n)::P(n) by ProofByCases

Now I'll write out the derivations themselves. Firstly for the case n=z:

  Suppose
    n=z
  Then
    ρ ⊢ R::P(z)
    τ(z) ⊢ R::P(z)
    τ(z) ⊢ T(z)::P(z)
  Hence
    τ(n) ⊢ T(n)::P(n)

In the derivation we begin by re-stating the first premise and then, since we have defined τ(z) to be ρ, the next line follows. And now note that the next line verifies. It reads 'theorem T(z) is a proof of P(z) given τ(z). Well, it verifies! Because given ρ we can prove R, whatever R happens to be, and since our own generic theorem T(z) relies on nothing but R, the assertion τ(z) ⊢ T(z)::P(z) holds. And since n is just z, we are done. For the case n=s(k), the reasoning is along similar lines.

Update: The complete proof is now here.

Answer 2

Put simply, it rules out the circle of dominoes and allows only the straight line of dominoes...

Induction does not rule out such a circular structure on the natural numbers. In fact, induction can be shown to hold even on the set $M=\{0\}$ with $S(0)=0$. We would have:

$$\forall P\subset M:[0\in M \land \forall x\in P: S(x)\in P \implies P=M]$$

In Peano's axioms, it is the axiom $\forall x\in N: S(x)\ne 0$ that ensures an infinite, straight-line structure starting at $0$. Induction simply rules out the possibility of not being able to reach any particular number by repeated succession if we start at $0$.

I asked myself then why it isn't possible to derive the ninth axiom, namely the axiom of induction.

If you want to derive Peano's Axioms including the principle of induction, you can start by assuming the existence of an arbitrary Dedekind infinite set $X$. From any such set, we can extract at least one "copy" of the set of natural numbers. For any such set, there exists $x_0\in X$ and an injective but non-surjective function $f:X\to X$ such that $\forall x\in X: f(x)\ne x_0$.

It can then be shown that there exists a subset $N\subset X$ with $x_0 \in N$ such that $(N,f,x_0)$ satisfies Peano's axioms with $f$ being the usual successor function and $x_0$ being the "first element" of set $N$.

Informally, we would have $N=\{x_0, f(x_0), f(f(x_0)\cdots \}$.

Answer 3

Yes, it is possible to prove that a "natural numbers type structure" satisfies the induction axiom. The proof will be carried out in the same set theory that is used to form the natural number type structure. The only challenge is to formalize the structure appropriately. There are many ways of specifying a "natural numbers type structure".

However, even though there are several ways to formalize inductively defined sets such as the one mentioned in the question, as long as care is taken to do it appropriately the nature of the inductive definition will ensure that the resulting structure satisfies induction. This is because, by nature, an inductive definition forms the smallest set possible. If the resulting set $S$ failed to satisfy the induction axiom because of some proper inductive subset, this would show that the resulting set $S$ is not actually as small as possible, leading to a contradiction.

For example, in the proof at the end of the question, we would look at the set $\{n : P(n)\}$. This would be a set that contains $0$ and is closed under successor. By the inductive definition of the construction, that set has to contain every number in the structure that was constructed - there is no need to worry about a least element or anything like that.