Strong induction in logical symbols

Question

I found the following definition of strong induction in Analysis 1 (Amann/Escher, third print).

Let $n_0\in\mathbb{N}$ and $\mathcal{A}$ is predicate defined over all integers $n\geq n_0$. Suppose the following two statements are true:

1. $\mathcal{A}(n_0)$ is true.
2. For all $n\geq n_0$, if $\mathcal{A}(k)$ is true for all $n_0\leq k\leq n$, then $\mathcal{A}(n+1)$ is true.

Then the statement $\mathcal{A}(n)$ is true for all $n\geq n_0$.

On Wikipedia there is representation of mathematical induction in logical symbols. And I want to know how to formalize the strong induction (the given theorem above) in logical symbols?

Answer 1

Assuming your domain is the natural numbers, and you want to prove it is true for all natural numbers, it is simply this:

$$\forall n (\forall k (k < n \rightarrow P(k)) \rightarrow P(n)) \rightarrow \forall n \ P(n)$$

I prefer to use $<$ instead of $\le$. That way, you don't need an explicit base case, since for the $n=0$ 'base' case the $\forall k (k < n \rightarrow P(k))$ statement is trivially true, and hence if you can prove $\forall n (\forall k (k < n \rightarrow P(k)) \rightarrow P(n))$ then you have thereby automatically proven $P(0)$

If you want it to be true for all numbers $n \ge n_0$, you can use:

$$\forall n \ge n_0 (\forall k (n_0 \le k < n \rightarrow P(k)) \rightarrow P(n)) \rightarrow \forall n \ge n_0 \ P(n)$$

Again, no explicit base needed, since for the $n=n_0$ case the $\forall k (n_0 \le k < n \rightarrow P(k))$ statement is trivially true, and hence if you can prove $\forall n (\forall k (n_0 \le k < n \rightarrow P(k)) \rightarrow P(n))$ then you have thereby automatically proven $P(n_0)$

Answer 2

$$[\mathcal{A}(n_0) \land [\forall n[n \ge n_0 \implies [[\forall k[(n_0 \le k \le n) \implies \mathcal{A}(k)]] \implies \mathcal{A}(n+1)]]]] \implies [\forall n[\mathcal{A}(n)]]$$