Mathematical induction's fixpoint

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

(0)          〈 ∀x :: [x ⇒ r ; x] &#x21D2 [ 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)          [x ⇒ r ; 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}
               [x ⇒ r ; x ∨ r ; ( x ∧ ¬ ( r ; x ))]
≡               { ; monotonic in 2nd argument}
               [x ⇒ r ; x]

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

---