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!


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$ 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$ May 26, 2020 at 8:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .