0

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?

Hölderlin
  • 105

2 Answers2

3

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)$

Bram28
  • 100,612
  • 6
  • 70
  • 118
  • You do need the first statement, just like you need the base case for normal induction. – Kenny Lau Sep 13 '17 at 20:58
  • Consider $P(n) = \bot$. Then, $\forall k (k<n \implies P(k))$ is false, so $\forall k(k<n \implies P(k)) \implies P(n)$ is true (ex falso quodlibet), so the antecedent of the main clause is true, while the consequent is obviously false. – Kenny Lau Sep 13 '17 at 21:03
  • @KennyLau Assuming we are talking about the natural numbers, if $P(n)=\bot$ then $\forall k (k < n \rightarrow P(k))$ is true in the case of $n=0$ . And for integers in general, and with some $n_0$ as the 'base', the second symbolization in my Answer will likewise work just fine without having to make the base case explicit. – Bram28 Sep 13 '17 at 21:17
  • Sorry, you're right. – Kenny Lau Sep 13 '17 at 21:28
  • @KennyLau No problem. And you are right in so far that in practice you typically do end up having to prove the base case by itself as an edge case. – Bram28 Sep 13 '17 at 21:37
  • @Bram28, I agree and really like your pragmatical way of this theorem (independent of the notation style (logical symbols)). Do you know analysis books, where the wording of theorems is focused in a pragmatical way like yours? – Hölderlin Sep 15 '17 at 07:48
  • @Hölderlin Unfortunately I don't know of any analysis books, but I follow the logic textbook Language Proof and Logic where the rule is implemented this way in the software. – Bram28 Sep 15 '17 at 16:50
0

$$[\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)]]$$

Kenny Lau
  • 25,049