Talk:Well-Founded Induction

Am I correct in thinking that well-founded induction is the most general form of induction, or at least the most commongeneral standard form? If so, we (I?) should probably undertake to prove the other forms from it. Also, I don't think we have well-founded recursive definition here. --Dfeuer (talk) 21:17, 24 December 2012 (UTC)

It appears so, yes. At least it incorporates ordinal, natural numbers and structural induction (which are the most common forms I've seen). However, this part of the site (set up by Asalmon last summer) is still quite a mess, with uncommendable notations and a partial attempt to use class theory. It needs a thorough reworking but I'm currently working in a twice-nested sub-thread (Awodey -> Halmos/Givant -> Lattice theory) so it will be quite a long time before I can go over it. Prime.mover doesn't like the field so it's unlikely he'll take it up.

Nonetheless, let such considerations not deter you from attempting to link the various induction theorems. Posting a recursion theorem in this generality would also be nice but I fear that the preliminaries are still a bit wobbly at the least, so it'll be a challenge. --Lord_Farin (talk) 21:27, 24 December 2012 (UTC)

As long as you take whatever pains are needed to ensure compatibility with the existing Principle of Mathematical Induction and so on. IMO we really don't need as many expositions of induction as we have unless there is an attempt to bring them all under one banner and provide an indication that they are all saying "sort of the same thing" just in slightly different language and from a slightly different context. --prime mover (talk) 22:23, 24 December 2012 (UTC)

This line looks real funny

Suppose $\forall x \in A: \left({ \left({ A \cap \prec^{-1} \left({ x }\right) }\right) \subseteq B \implies x \in B }\right)$. (1)

Isn't $\prec^{-1}(x) \subseteq A$? Or was my last edit (to try to pin $x$ down) somehow mistaken? --Dfeuer (talk) 21:34, 24 December 2012 (UTC)

You were right. Fixed. --Lord_Farin (talk) 21:38, 24 December 2012 (UTC)