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 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, Fundamenta Mathematicae 25 (1935) 135--146, with an English translation in volume I of his Collected Works, edited by Heinz-Dieter Ebbinghaus et al.
