Mathematical induction's fixpoint

Let r be a left-founded relation, i.e. let

(0)          〈 ∀x :: [xr ; x] ⇒ [ x ⇒ false ]  〉     ;

an appeal to what is called "mathematical induction" means that a proof obligation of the form

(1)          [ x ⇒ false ]

is replaced by the formally weaker obligation

(2)          [xr ; x]      or      [ x ∧ ¬ ( r ; x ) ⇒ false ] .

Proving (2) by mathematical induction leads to the (subsequently simplified) obligation

(3)          [ x ∧ ¬ ( r ; x ) ⇒ r; ( x ∧ ¬ ( r ; x ))]
≡               {shunting}
               [xr ; xr ; ( x ∧ ¬ ( r ; x ))]
≡               { ; monotonic in 2nd argument}
               [xr ; x]

i.e. (2)! The decision to prove by mathematical induction is idempotent. With thanks to the ETAC.

Nuenen, 17 December 1996

prof.dr. Edsger W.Dijkstra
Department of Computer Sciences
The University of Texas at Austin
Austin, TX 78712-1188, USA