Proof:Weak induction principle with n-1 is equivalent to weak induction

From CS2800 wiki

Suppose you have an inductive proof in the following style:

To prove [math]\href{/cs2800/wiki/index.php/%5Cforall}{\forall} n \href{/cs2800/wiki/index.php/%5Cin}{\in} \href{/cs2800/wiki/index.php?title=Natural_numbers&action=edit&redlink=1}{\mathbb{N}} [/math] by weak induction, you can prove [math]P(0) [/math] and prove [math]P(n) [/math] for an arbitrary [math]n\gt 0 [/math], assuming [math]P(n-1) [/math].

But you are only willing to accept the basic weak induction principle:

To prove "[math]\href{/cs2800/wiki/index.php/%5Cforall}{\forall} n \href{/cs2800/wiki/index.php/%5Cin}{\in} \mathbb{N},P(n) [/math]" using weak induction, you must prove [math]P(0) [/math] (this is often called the base case), and then you must prove [math]P(n+1) [/math] for an arbitrary [math]n [/math], assuming [math]P(n) [/math] (this is called the inductive step).

You can systematically convert from the first style to the second:

Suppose you know the following:
  1. [math]P(0) [/math]
  2. [math]\href{/cs2800/wiki/index.php/%5Cforall}{\forall} n \gt 0, P(n-1) [/math] implies [math]P(n) [/math]
Then you can conclude [math]\href{/cs2800/wiki/index.php/%5Cforall}{\forall} n \href{/cs2800/wiki/index.php/%5Cin}{\in} \href{/cs2800/wiki/index.php/Natural_number}{\mathbb{N}}, P(n) [/math], using only the basic weak induction principle.
Proof: By changing variable names
Assume the statements that are given in the claim; we will show [math]P(0) [/math] and [math]P(n+1) [/math] for an arbitrary [math]n \geq 0 [/math], assuming [math]P(n) [/math].


[math]P(0) [/math] is easy: it was given to us as assumption 1.


To see [math]P(n+1) [/math], choose an arbitrary [math]n \geq 0 [/math], and assume [math]P(n) [/math]. Let [math]m = n+1 [/math]. Then [math]m \gt 0 [/math], and we have assumed [math]P(m-1) [/math]. Thus we can apply assumption 2 given above to conclude [math]P(m) [/math].

But [math]P(m) = P(n+1) [/math], which is what we wanted to prove.