I have changed the title in the hope of attracting the attention of someone who knows about the history of set theory as well as intuitionistic logic:

Who was the first to state the definition of well-foundedness intuitionistically as the induction scheme?

$$ \forall \phi.\quad\frac{\forall x.(\forall y. y\prec x\Rightarrow \phi y)\Rightarrow \phi x}{\forall x.\phi x} $$

While I'm here, are the following historically correct?

  • Euclid's Elements Book VII Proposition 31 (the Euclidean algorithm for prime factorisation) says that an infinite descending sequence is impossible amongst the natural numbers.

  • What other forms of induction and recursion were stated before the 17th century?

  • Fermat, Pascal and Wallace in the 1650s stated induction in the form of the base case and induction step.

  • Cantor 1897 (earlier?) proved that, for any two well ordered sets, one is uniquely equivalent to an initial segment of the other.

  • Mirimanoff 1917 was the first to recognise the importance of the absence of infinite descending sequences in the consistency of set theory.

  • von Neumann 1925 proposed the first version of the axiom of foundation, that the system of set theory is the minimal one.

  • Zermelo 1930 first asserted the axiom of foundation as the lack of infinite descending sequence of elements.

  • Zermelo 1935 was the first to study well-foundedness in the abstract, as a tool for proof theory.

  • von Neumann 1928 was the first to prove the recursion theorem for ordinals.

I am currently working on the categorical reformulation of von Neumann's recursion theorem, for well founded coalgebras: http://www.paultaylor.eu/ordinals This includes the full bibliographical details of the above references.

I can read French and Italian reasonably fluently, but unfortunately not German.

Even some guesses would be appreciated!

Postscript: There is a historical introduction in my papers Well Founded Coalgebras and Recursion, which is now with referees and can be found on the webpage mentioned above, along with follow-up work on Ordinals as Coalgebras and infrastructural work on Pataraia's fixed point theorem.

As for the first person to state well-foundedness as opposed to well-ordering, the earliest I could find was:

Ernst Zermelo, Grundlagen einer allgemeinen Theorie der mathematischen Satzsysteme, Fundamenta Mathematicae 25 (1935) 135--146, with an English translation in volume I of his Collected Works, edited by Heinz-Dieter Ebbinghaus et al.

  • $\begingroup$ What about Dedekind arithmetic (1888), which states induction for the natural numbers with successor, and Peano's (1889) subsequent beautiful and popular use of it to develop the basics of number theory. Also, Cantor made essential use of transfinite recursion in the Cantor-Bendixson theorem (1872), and indeed, these ideas are what led him to the ordinals. $\endgroup$ Commented Sep 6, 2023 at 14:18
  • 1
    $\begingroup$ @JoelDavidHamkins. Yes of course. But I was looking specifically for the abstract notion well founded relation, as classically stated. There's another question about who first stated it intuitionisticallly, ie just as the induction scheme. However, that is much more difficult because of the habit of intuitionists to state classical definitions and then argue at length about why they're wrong, instead of just giving the correct constructive definition. $\endgroup$ Commented Sep 6, 2023 at 14:25
  • $\begingroup$ I was thinking it gives a somewhat fuller historical picture, since not everything on your list is about that abstract well-founded concept. In particular, Dedekind's 1888 categoricity result for arithmetic (basically, any two inductive successor operations are isomorphic) amounts to a precursor and special case of the comparability result you mention of Cantor. And Cantor's earlier use of transfinite recursion in the Cantor-Bendixson theorem is the first nontrivial use of transfinite recursion, which I think of as absolutely central and indeed seminal in the history of well-foundedness. $\endgroup$ Commented Sep 6, 2023 at 14:29
  • 1
    $\begingroup$ It would be better to tell the story backwards. You would be sure to finish at some point. $\endgroup$
    – PseudoNeo
    Commented Sep 6, 2023 at 14:56
  • 3
    $\begingroup$ @PseudoNeo I saw what you did there. $\endgroup$ Commented Sep 6, 2023 at 15:32

1 Answer 1


Emmy Noether must fit in there somewhere. Computer Scientists always mention her when talking about the foundations for making sure that iterative and recursive algorithms terminate. Unfortunately, I don't know of any translations of her work from the German. Bibliography at https://enacademic.com/dic.nsf/enwiki/9878553 where the only relevant work that I see has the note "By applying ascending and descending chain conditions to finite extensions of a ring, Noether shows that the algebraic invariants of a finite group are finitely generated even in positive characteristic.".

  • $\begingroup$ Oh. I see you're way ahead of me on that. $\endgroup$ Commented May 25, 2020 at 0:03
  • 1
    $\begingroup$ Welcome to MO. My other question attracted a lot of discussion about Noether, but the relationship is still a historical blur to me. In this question I was looking for the reference for a very specific formulation. It might have been one of her German contemporaries, such as Goedel or Gentzen. $\endgroup$ Commented May 26, 2020 at 8:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.