Proof of the Principle of Backwards Induction

Question

I'm trying to prove the following proposition, where "++" denotes the successor function (i.e., 2++ = S(2) = 3).

Let $n$ be a natural number, and let $P(m)$ be a property pertaining to the natural numbers such that whenever $P(m++)$ is true, then $P(m)$ is true. Suppose that $P(n)$ is also true. Then $P(m)$ is true for all natural numbers $m \leq n$.

I'd be thankful if someone could check my proof and also clarify a particular step. The proof is quite verbose, but I like it that way. I'll post an image, because it gives me less headache to post my attempt:

I'm most worried about (5) of the induction step. It's obvious that it's correct, but at this point it's of course all about showing things rigorously that are "obviously true". But I'm failing at giving an explicit argument for why this step holds. I'm thankful for all feedback, especially concerning this precise issue.

Answer 1

You are right that step 5 in the inductive step proof is not a purely logical step.

But note that step 4 of the inductive base is likewise also not purely logical, given that line $3$ refers to $\geq$ and line $4$ to $\leq$. So, if you don’t want to accept this step 4 on purely mathematical grounds, then you need to point out some connection between $\leq$ and $\geq$.

For example, we could add something like $\forall x \forall y ((x \leq y \land x \geq y) \to x=y)$ (Lemma1)

Then once we have $P(0)$ and $\forall x \ x \geq 0$, we can do for the Inductive Base:

$1. P(0)$

$2. \forall x \ x \geq 0$

$3. \forall x ((x \leq 0 \land x \geq 0) \to x=0)$ (Instance of Lemma1)

$4. \forall x (x \leq 0 \to x=0) \ (2,3)$

$5. \forall x (x \leq 0 \to P(x)) \ (1,4)$

You'd need to do something similar for the step 5 in the inductive Step part of the inductive proof, because you are right: going from 1 to 4 is obvious mathematically, but it doesn't follow purely logically. So you'd need to provide some further Lemma, definition, or what have you. And that's what Mark Saving tried to do in their Answer: Mark proposed to use

$\forall x \forall y (x \leq y++ \to (x \leq y \lor x = y++))$ (Lemma2)

And hopefully you can see how line 5 is the logical result of lines 2, 4, and Lemma2.

Now, of course you can ask where these Lemmas come from ... and don't you need to prove those? Well, that all depends on what we consider our very axioms and definitions. I see that in your posted proof of the Inductive Base there is a reference to 'Definition 2' and 'Definition 4', so that might give you a clue.

Answer 2

To justify step 5, you would have to prove $\forall x \forall y (y \leq x ++ \to y \leq x \lor y = x++)$. This would need to follow from a definition of $\leq$, which you did not provide in your question. Without details of this definition, we cannot proceed further.

Here is one way of proving what you wish to show. We define $x \leq y$ as $\exists z (x + z = y)$.

We want to show that $\forall x \forall y (y \leq x \land P(y) \to P(x))$. This is equivalent to $\forall x \forall y (y \leq x \to P(y) \to P(x))$. Substituting the definition of $\leq$ gives $\forall x \forall y (\exists z (x + z = y) \to P(y) \to P(x))$, which is equivalent to $\forall x \forall y \forall z (x + z = y \to P(y) \to P(z))$, which is in turn clearly equivalent to $\forall x \forall z (P(x + z) \to P(x))$.

Now we’ve finally gotten to a form we can prove using induction. Fix $x$, and proceed by induction on $z$.

Base case: we must show $P(x + 0) \to P(x)$. This is trivial, since $x + 0 = x$.

Inductive step: suppose $P(x + k) \to P(x)$. Now suppose $P(x + k++)$. That is, $P((x + k)++)$. Then $P(x + k)$. Then $P(x)$. And we’re done.