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!


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$ – George S Cowan May 25 '20 at 0:03
  • $\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$ – Paul Taylor May 26 '20 at 8:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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