Talk:Principle of Mathematical Induction/Well-Ordered Set

Theorem statement

Isn't:

$\forall s \in S: \left({\forall t \in S: t \preceq s \implies t \in T}\right) \implies s \in T$

true for any $T \subseteq S$, since $\forall s \in S: s \preceq s$? Did I make a mistake somewhere? --abcxyz 06:33, 28 June 2012 (UTC)

I've noticed from going back to the initial source that it should in fact be

$\forall s \in S: \left({\forall t \in S: t \prec s \implies t \in T}\right) \implies s \in T$

... I'm going to review this carefully and make sure of it. --prime mover 06:45, 28 June 2012 (UTC)

The second statement appears correct; it is similar to other 'order induction' variants I have seen (eg. for induction on subsets of the reals). --Lord_Farin 06:57, 28 June 2012 (UTC)

This is taking more time to think about than I was expecting. The initial exposition of this theorem from Devlin has that the smallest element of $S$ is an element of $T$, and uses that in the proof (which is minimal). He then states that "condition 1 is superfluous, since it is a consequence of condition (ii)" (the condition given here). My work in the original page was a (flawed) attempt to prove that. However, yours glosses over the detail by saying "By the rule of transposition (and the definition of a smallest element) $\forall t \in S: t \prec s \implies t \in T$" which I'm not sure I can follow.

But it's hot and muggy and I can't think straight (plus I'm a bit fick) so I'm probably talking utter shite as usual. --prime mover 07:20, 28 June 2012 (UTC)

Ok, if $t \in S$ then $t \in S \setminus T$ or $t \in T$. If $t \prec s$, then as $s$ is smallest for $S \setminus T$, $t \notin S \setminus T$. Thus $t \in T$. That clear your mind? --Lord_Farin 07:39, 28 June 2012 (UTC)

I'll give it a think - currently supposed to be working on some automatic regression test software and my head's a mush. Bu tit occurs to me that this could / should be used as "the" fundamental result from which all the other similarly-crafted results should reference: Principle of Mathematical Induction, for example. In fact, it's practically the same as PoFI as it stands. I'll address this in due course. --prime mover 10:08, 28 June 2012 (UTC)

This ought to be merged with Well-Ordered Induction --Andrew Salmon 22:10, 28 July 2012 (UTC)

On second thought, they should not be. But they should be linked. --Andrew Salmon 22:12, 28 July 2012 (UTC)