A proof of the principle of mathematical induction Is there a definition of the natural number in which someone might be able to prove "The Principle of mathematical induction"? 
 A: It is a common misconception that induction over natural numbers can somehow be justified (in a non-circular way). This is simply impossible, and there are two parts to the reason.

Firstly, note that to even talk about induction we need to work within a meta-system. And any reasonable meta-system will already have access to the natural numbers, in the sense that it has an inbuilt assumption that there is a collection $N$ of objects and operations $+,\times$ on $N$ that satisfy first-order PA (or something equivalent to it). PA already includes the induction schema. It just makes absolutely no sense to ask for a justification of induction over natural numbers without first defining natural numbers, but that cannot be done without already using assumptions with PA essentially built into them.
In short, it is like asking whether there is a proof that the English language is a language. Well, in English we have already agreed upon what "the English language" refers to, which is indeed a language!
For example, ZFC set theory does not seem to have the natural numbers as basic objects, but note the axiom of infinity (Inf). It is totally meaningless unless we already believe in the existence of a set that is structure-isomorphic to the natural numbers, besides believing in the other ZFC axioms. Furthermore, it is nothing more than a set-theoretic version of induction! Its modern form states that "an inductive set exists":

(Inf) $∃I ( ( ∀x ( ¬∃y ( y∈x ) ⇒ x∈I ) ∧ ∀x ( x∈I ⇒ ∀y ( ∀z ( z∈y ⇔ z∈x ∨ z=x ) ⇒ y∈I ) ) )$

The other axioms such as specification and union permit ZFC to 'implement' arithmetic operations on the set $N$ given by (Inf), as in any standard textbook, and ZFC can indeed prove that $N$ satisfies induction in terms of the conventional axiomatization of PA.
But of course you can't possibly believe that (Inf) is true unless you already believe in ZFC plus the existence of a set that is inductive (intuitively some set containing all and only the sets that can be obtained from the empty-set by a finite natural number of the successor operation $x \mapsto x \cup \{x\}$).

Secondly, one might still ask whether induction is superfluous, in the sense that any proof using induction can be converted to a proof without induction. No, for any reasonable interpretation of the question. Of course, one could be silly and replace induction by a slightly different axiom (or axiom schema), but as with ZFC's axiom of infinity it would be obvious to any logician that the core notion of induction cannot be justified non-circularly.
The mathematical basis is as follows. PA$^-$ is stronger than PA minus the induction schema. But PA$^-$ is strictly weaker than PA and has a model that everyone agrees is structurally different from natural numbers. Specifically, let $P$ be the collection of polynomials with integer coefficients such that the coefficient of the highest-degree term is non-negative. Then $P$ with the usual polynomial arithmetic and the ordering defined via $x<y \overset{def}\equiv x \ne y \land \exists z\ ( x+z=y )$ satisfies PA$^-$ but does not satisfy induction. This is because PA proves $Q \overset{def}\equiv \forall n\ ( \exists m\ ( n = 2m \lor n = 2m+1 ) )$ but $P$ does not satisfy $Q$, and so $P$ does not satisfy the axiom given by induction that was used in the proof of $Q$ over PA.
A: If your axioms include "The well ordering principle" then you can prove the principal of induction.  Here is an example of how it can be done


*

*0 is a natural number ($ 0 \in \mathbb{N}) $

*Any successor of a natural number is a natural number ($\forall n \in \mathbb{N} . S(n) \in \mathbb{N} $)

*0 is equal to or less then then all natural numbers ($\forall n \in \mathbb{N} . 0 \leq n $)

*Every natural number is less than its successor ( $\forall n \in \mathbb{N} . n < S(n)$)

*Less then is an associative property ( $ \forall \langle a, b, c \rangle \in \mathbb{N}^3. a \leq b \land b \leq c \Rightarrow a  \leq c$)

*Every set of natural numbers has a smallest element ($ \forall s \in \mathcal{P}(\mathbb{N}) . \exists n \in s .\forall m \in s . n \leq m$)


From this you can derive the principle of induction via a proof by contradiction.
Assume that the principle of induction is false.  Therefor there exists a proposition $P$ for which $(P(0) \land P(n) \Rightarrow P(S(n))) \not{\Rightarrow} P(n) $. Construct a set of all numbers for which $P$ is not true $ N = \{ n \in \mathbb{N} : \lnot P(n) \} $.  By the principal of well ordering there must be a minimal element m in $N$. By the definitional of a natural number m must either be 0 or a successor of another natural number.
The minimal element m can't be 0 as $P(0)$ is true.  However if m is not zero then it must be a successor of some other natural number n. If $P(n)$ is true then $P(n) \Rightarrow P(S(n))$ is contradicted but if $P(n)$ is false then m isn't the minimal member of $N$.
All possibilities lead to a contradiction therefore our initial assumption must have been false and the principal of induction holds.
A: Yes, there are a few.
In a type-theoretic setting, you can define the naturals as an inductive type and then prove induction by structural recursion. Here's how you could do it in Coq:
Inductive natural : Set :=
| zero : natural
| succ : natural -> natural.

Definition natural_induction :
  forall P, P zero ->
    (forall n, P n -> P (succ n)) ->
    forall n, P n :=
fun P Pzero Psucc => fix rec n :=
match n return P n with
| zero => Pzero
| succ n' => Psucc n' (rec n')
end.

In a set-theoretic setting, one common way of defining the naturals is as the finite von Neumann ordinals—that is, $0 = \emptyset, 1 = \{0\}, 2 = \{0, 1\}, 3 = \{0, 1, 2\}...$ Let's say that a set $S$ is inductive if $\emptyset \in S$, and for any $x \in S$ we have $x \cup \{x\} \in S$ (that is, the successor of $x$ is in $S$). Then in ZFC, the axiom of infinity tells us that there is at least one inductive set—let's call it $I$. We can define the naturals $\mathbb N$ as the intersection of every inductive subset of $I$. From this, the principle of induction follows almost immediately: Given an inductive subset $S$ of $\mathbb N$, we have $S \subseteq \mathbb N \subseteq I$, and any inductive subset of $I$ contains $\mathbb N$, since $\mathbb N$ is defined as the intersection of all of them. Then we have $S \subseteq \mathbb N$ and $\mathbb N \subseteq S$, so $S = \mathbb N$.
A: A working list of the Peano Axioms defining the natural numbers $\mathbb{N}$ is:


*

*In the set of the natural numbers there is an element named 1.

*For every natural $n$ there is another natural, named successor, denoted by $n+1$.

*There are no natural numbers $n$ for which $n+1 = n$.

*If $n+1 = m+1$ for two natural numbers $n$ and $m$, then $n=m$.

*If $S$ is a subset of the naturals satisfying that $1\in S$ and if $k\in S$ then $k+1\in S$, then $S = \mathbb{N}$.


Since these are axioms, there is nothing to prove. Notice how the last axiom can be rewritten as:


*

*If there is a function $P:\mathbb{N}\rightarrow \{T,F\}$ satisfying that $P(1) = T$ and that if $P(k) = T$ then $P(k+1) = T$, then $P(n) = T$ for every natural $n$.


Which is precisely the Induction Principle.
Consider now the natural numbers defined as ordinals (notice that with these axioms we require the empty set to exist): define $1 = \{\emptyset \}$ and $n+1 = n \cup \{n\}$, and by definition $\mathbb{N} = \{1,2,3,\dots\}$ (one can include $0 = \emptyset$ if it so desires). Notice that under the definition as ordinals, $\mathbb{N}$ is a well-ordered set with respect to the inclusion, namely $n\subset n+1$.
We prove the fifth Peano axiom: suppose we have $S$ a subset of the naturals satisfying that $1\in S$ and if $k\in S$ then $k+1\in S$. If $S = \mathbb{N}$, we are done. Suppose $S \neq \mathbb{N}$, then the set $T = \{n\in\mathbb{N} : n\notin S\}$ is a non-empty subset of a well-ordered set $\mathbb{N}$, meaning that it has a least element, say $m$. Since $1\in S$ we have $m \neq 1$ so $\emptyset,\{\emptyset\}\in m$. By construction $m$ is a well-ordered set and contains only a finite number of sets, thus it contains a maximal set $k$. Again by construction, we have that $m = k\cup \{k\}$ so $m = k+1$. Since having $k\in T$ contradicts that $m$ is the least element in $T$, we have that $k\in S$ and thus by hypothesis $m = k+1\in S$, a contradiction.
