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!