Well founded induction attributed to Noether

Question

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 I have translated. 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.

Answer 1

It seems to me to be much more than merely an analogy, because (assuming DC) the ascending chain condition is exactly equivalent to asserting that the collection of ideals is well-founded under (reverse) inclusion. Thus, one can make arguments by induction on ideals, where each instance reduces to the instances in larger ideals, if any, and it seems that Noether did this quite well. For example, under the ACC, every nonempty set of ideals must contain a maximal element, and this is simply another way of stating the induction principle: to prove $\phi(I)$ for every ideal, simply prove that if $\phi(J)$ for all $J\supsetneq I$, then $\phi(I)$, since this will rule out a maximal element of the set $\{I\mid \neg\phi(I)\}$, which must therefore be empty. When the ACC holds, therefore, one may assign an ordinal rank to every ideal, in the manner that any well-founded relation supports such ranks, namely, the maximal ideals get rank 0, and penultimate ideals get rank 1 and so on, with the rank of an ideal equal to the supremum of the ranks+1 of the ideals properly containing it.

So my perspective is that the ACC is a quite robust and important instance of well-foundedness, rather than merely analogous to it.

Concerning the history of the terminology, I noticed that the Wikipedia entry on Noetherian induction redirects to the page on well-founded relations, and Wikipedia cites "Bourbaki, N. (1972) Elements of mathematics. Commutative algebra, Addison-Wesley" specifically in connection with this terminology. So perhaps Bourbaki is the origin of the terminology? (See ACL comments below.) Transfinite recursion itself certainly pre-dates Noether, tracing back to Cantor's use of it in the Cantor-Bendixson theorem, which is also the theorem that led Cantor to the ordinals. Meanwhile, the Wikipedia entry on the axiom of foundation asserts that "the concept of well-foundedness and rank of a set were both introduced by Dmitry Mirimanoff (1917)."

Lastly, let me add that one doesn't generally much see this Noetherian terminology used for well-foundedness or well-founded induction in the parts of logic or set theory with which I am familiar, where the use of well-foundedness is pervasive and often a central concern. But I suppose it wouldn't be surprising to find this terminology more commonly used in algebra, because of Noether's successful use of it there.