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.  I have made an [English translation](http://paultaylor.eu/trans/) of this paper.

- 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*, Mirimanoff 1917 uses the idea without naming it, but otherwise the earliest I could find was:

Ernst Zermelo, [*Grundlagen einer allgemeinen Theorie der mathematischen Satzsysteme*](http://matwbn.icm.edu.pl/ksiazki/fm/fm25/fm25114.pdf), Fundamenta Mathematicae 25 (1935) 135--146, with an English translation in volume I of his *Collected Works*, edited by Heinz-Dieter Ebbinghaus et al.