A methodological remark on mathematical induction

A methodological remark on mathematical induction

This note is for the record: I know that I have shown the following during several lectures, but cannot remember that I ever wrote it down.

In the following, $x$ and $y$ range over the elements of a well-founded set $\left( {C, < }\right) ;\;\left( {C, < }\right)$ being well-founded means that for any predicate $P$ on $C$

(a) $\left( {\underline{A}x\because P.x}\right) \equiv \left( {\underline{A}x\therefore P!\cdot x}\right)$ ,

where ${P}^{\prime }$ is given in terms of $P$ by

$\left( 4\right) \;\left( {A \times : P}^{\prime }\right. x = P \times V\left( {E \cdot y : y < x : ?P.y}\right) )$

This is what mathematical induction is about: instead of computing the left-hand side of (0), we can compute its right-hand side, and, if the value is true, the latter computation is "easier" because - see (1) - $P^{\prime}$ is formally weaker than $P$ . Indeed, we deduce from (1) immediately (2) $\left( {A \times : P \cdot X \Rightarrow {P}^{\prime } \cdot X}\right)$

The right-hand side of (0) is of the same form as its left-hand side, so, why don't we make life still easier by repeating the trick, since

$$ (\underline {{A}} x: P ^ {\prime} x) \equiv (\underline {{A}} x: P ^ {\prime \prime} x) $$

where according to (1) with ${P}^{\prime } = {P}^{\prime } -$

(3) $\left( {\underline{A}x\because {P}^{\prime }\because x \equiv {P}^{\prime }x}\right. \vee \left( {{E}_{y} : y < x : {n}^{\prime }{P}^{\prime }y}\right) )$

should we continue, and derive $P^{\prime \prime}$ to make life even easier? No, we can stop at $P^{\prime}$ , for we observe

for any $x$

$$ \begin{array}{l} P ^ {\prime \prime}. x \ = {(3) } \ P ^ {\prime} x \vee (E y: y < x: \neg P ^ {\prime} y) \ = {(1) } \ P _ {x} v (\exists y: y < x: \neg P. y) v (\exists y: y < x: \neg P ^ {\prime}. y) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ P _ {x} \vee (\mathrm {E} y: y < x: \neg P. y, \vee \neg P. y) \ = {(2) \mathrm {a n d} p r e d i c a t e c a l c u l u s } \ P _ {x} \vee (E y: y < x: \neg P _ {y}) \ = {(1) } \ p _ {x} ^ {\prime} \ \end{array} $$

In other words, the decision to demonstrate the truth of $\left( {\underline{A}x : P.x}\right)$ by mathematical induction is idempotent: if can be taken once, but then the proof obligation has reached a fixpoint.

Austin, 22 March 1987

prop. dr. Edsger W. Dyksbra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712 - 1188

USA