I need help regarding the following exercise:
Derive the variant $$[\forall n:((\forall m < n: \varphi (m)) \Rightarrow \varphi (n))] \Rightarrow \forall n: \varphi(n)$$ of mathematical induction from the variant $$[\psi(0) \land \forall n:(\psi(n) \Rightarrow \psi(n+1))] \Rightarrow \forall n:\psi(n)$$ where $n,m \in \mathbb N_0$.
My attempt:
Define $$\psi(n) :\Leftrightarrow \varphi(n-1)\land \forall m < n: \varphi(m)$$
And here's the problem. I can't plug $0$ into $\varphi$ since it is only defined for natural numbers $\geq 0$. However, if I somehow could work around that I think I would get the first variant. Am I correct and how can I fix my attempt?
Update: I tried with $\psi(n) :\Leftrightarrow \forall m < n: \varphi(m)$ but wasn't really able to derive the first scheme.
Try $\psi (n) = \forall m \leq n : \varphi(m)$
With that, the basic proof outline becomes this:
You have the general principle of weak mathematical induction, which says that for any $\psi (n)$ that:
$$[\psi(0) \land \forall n:(\psi(n) \Rightarrow \psi(n+1))] \Rightarrow \forall n:\psi(n)$$
so with $\psi (n) = \forall m \leq n : \varphi(m)$ that becomes:
$$[(\forall m \leq 0 : \varphi(m)) \land \forall n: ((\forall m \leq n : \varphi(m)) \Rightarrow (\forall m \leq n+1 : \varphi(m)))] \Rightarrow \forall n:\forall m \leq n : \varphi(m)$$
OK, so that's the premise of your argument. The conclusion is the general principle of strong mathematical induction:
$$[\forall n:((\forall m < n: \varphi (m)) \Rightarrow \varphi (n))] \Rightarrow \forall n : \varphi(n)$$
OK, since the goal is a conditional, do a conditional proof:
Assume
$$[\forall n:((\forall m < n: \varphi (m)) \Rightarrow \varphi (n))]$$
and try and get to
$$\forall n : \varphi(n)$$
Once you have the above assumption, you want to prove two things:
Base: $$(\forall m \leq 0 : \varphi(m))$$
Step: $$\forall n: ((\forall m \leq n : \varphi(m)) \Rightarrow (\forall m \leq n+1 : \varphi(m)))$$
The base trivially follows from your assumption: since there are no number smaller than 0, the statement $$\forall m < 0: \varphi (m)$$ is trivially true, and hence $\varphi(0)$ is true, and hence the base is true.
For the step, do a general conditional proof, i.e. assume n to be some number, assume $$\forall m \leq n : \varphi(m)$$ and try to get to $$\forall m \leq n+1 : \varphi(m))$$
Again, using the original assumption, this should not be hard.
OK, so now we have the base and the step, so using the premise of your argument, you get $$\forall n:\forall m \leq n : \varphi(m)$$ and from there, your original goal of $$\forall n : \varphi(n)$$ easily follows.