What I know as **well founded induction**, namely the rule
$$ \big(\forall y.(\forall z.z\lt y\Rightarrow\phi z)\Rightarrow\phi y\big)\Longrightarrow\big(\forall x.\phi x\big), $$
whose validity is the definition of well-foundedness of the relation $\lt$,
I have recently heard called **Noetherian induction**. In fact Wikipedia includes this attribution.

With Excluded Middle and Dependent Choice, $\lt$ is well founded iff it has no infinite descending sequence $$ x_0 \gt x_1 \gt x_2 \gt x_3 \gt \cdots $$

This suggests at least an analogy with the **ascending chain condition** that
any sequence
$$ I_0 \subset I_1 \subset I_2 \subset \cdots $$
of ideals in a Noetherian ring is eventually constant.

Does the attribution of this idea to Emmy Noether amount to more than this analogy? Did she identify the principle at the top as one of logic? Or is this simply a case of the common phenomenon that names of concepts in Mathematics get transferred to more general or simply analogous situations without very much sound historical basis?

Thanks in particular to Joel Hamkins and Antoine Chambert-Loir (ACL) for their comments. Whilst it would be nice to fill in the small gap between Noether and Bourbaki, we have a plausible explanation of the connection between Emmy Noether the algebraist and this logical idea.

Generally speaking, I am a great admirer of Emmy Noether as a **conceptual mathematician** and rarely have much to say in favour of set theory. However, on this occasion, it would appear that the latter has a much better historical claim to this idea than algebraists do.

The work of Dimitry Mirimanoff that Joel mentions is in the paper *Les antinomies de Russell et de Burali-Forti: et le problème fondamental de la théorie des ensembles*, which appeared in *Enseignement mathématique* in 1917 but seems not to be available online. As Joel says, it defines the rank of the $\in$ relation of a set and uses induction in the form of infinite descent.

However, infinite descent in algebra goes back to Euclid: Book 7, Proposition 31 proves that **any composite number is measured by some prime number**, saying in the proof that "if the prime number is not found, **an infinite series** of numbers will measure the number $A$, each of which is less than the other: **which is impossible in numbers**".

The well founded relation $x\lt y$ in Euclid is that $x$ is a proper divisor of $y$. Algebraists from Kummer to Noether generalised divisibility to inclusion of ideals, $(y)\subset(x)$, which accounts for the reversal of the order. Noether generalised Euclid's arguments about prime factorisation from numbers to ideals.

Another thing that bugs me, both as a conceptual and constructive mathematician, is that the principle of **well founded induction** that I stated at the top is **not the same thing** as infinite descent. Quite apart from priority, it seems to me that one should take account of how ideas are formulated when naming or attributing them. I don't know who first wrote down the principle above, but Gentzen seems plausible.

In fact, the place where I recently heard well founded induction attributed to Noether was neither in the context of algebra nor logic: it was at a workshop on induction in automatic theorem provers.

I am not sure which rule Joel is labelling "well founded induction" in his further comments below. The rule at the top that I gave that name is an appropriate style to use as a proof rule in a constructive setting, whereas using infinite descent as a formulation of induction depends on an ambient logic with Excluded Middle and Dependent Choice.

One can also generalise the principle at the top by restricting the class of $\phi$s to which it is applicable. For example if the domain has an order with directed joins and $\phi$ is required to be closed under them then we have **Scott induction**. This proves properties of fixed points, in particular in the semantics of recursion in programming languages. I imagine that this idiom might be adapted to finitary constructive algebra too.

irreflexive, whilst I write $\subset$ and not $\subseteq$ for (reflexive) inclusion of sets etc. $\endgroup$ – Paul Taylor Nov 24 '13 at 22:19algebraist) identified this as a general principle oflogic. $\endgroup$ – Paul Taylor Nov 24 '13 at 22:21