User talk:Lord Farin/Backup/Principle of Finite Induction

"As $S$ is well-ordered, and $T' \subseteq S$, it follows that $T'$ has a minimal element. Call this minimal element $x$." Should this just be based on the well ordering principle? --cynic 23:19, 30 September 2008 (UTC)

Not the way I see it, as the Well-Ordering Principle specifically refers to the set $\N$ of natural numbers. The Principle of Finite Induction is demonstrated on the naturally ordered semigroup before we've gone anywhere near defining what the natural numbers are, and in fact is used in the construction of the proofs that establish that $\N$ is a naturally ordered semigroup in the first place. To assume the well-ordering principle would make the argument circular.

The fact that the natural numbers are mentioned at the bottom is an explanatory amplification which is not germane to the proof itself but follows a lot later down the line after the set of natural numbers has been defined and proven to be a naturally ordered semigroup. --Prime.mover 06:09, 1 October 2008 (UTC)

On the proposed merge

L_F: I would be against a merge here, as the principles are effectively saying different things.

The page Principle of Finite Induction is defining the properties of a set: that if the first element is in the set then they all are.

The page Principle of Mathematical Induction is a higher level: it specifically discusses elements of the natural numbers for which a property holds.

The way this set of pages got crafted originally was that Principle of Finite Induction was used in order to develop the structure of the Natural Numbers (either from Naturally Ordered Semigroups or the Peano Axioms -- or both) and then having done so, showing that $\N$ had those same properties.

Then Principle of Mathematical Induction takes that principle as a proven entity and uses it to allow the proof of propositions which have elements of $\N$ as a parameter.

I thought it was a good idea to divorce the set-theoretical version of this from the more general mathematical version, so as to allow "conventional" mathematical work to progress without getting the user bogged down in the specialised set-theoretical jargon that exists in Principle of Finite Induction. --prime mover (talk) 22:33, 19 April 2014 (UTC)

I understand that. However I do think it's wrong to have different names for what is essentially the same thing, looked at from different axiomatisations.

The whole concept of a "proof" of induction is void when taking PA as axiomatic. OTOH, it is evidently necessary for other axiomatisations and constructions.

Invariably the induction pages will be part of the exercise I'm going through, so in the mean time, please just read the merge request as a reminder for me that the two pages are actually talking about the same thing.

In the end, I predict the usual paradigm: modularity and transclusion. I can see it crystallize already in my mind, but I'll have to spend more time on preparing the various approaches to $\N$ for the exercise. — Lord_Farin (talk) 22:50, 19 April 2014 (UTC)

Okay no worries, treat the above as an explanation for the original structuring. Yes I know that PoI is already built into PA, but when I first attacked this I came in via the Natural Ordered Semigroup direction, because that was what my at the time limited library yielded. --prime mover (talk) 23:03, 19 April 2014 (UTC)