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!
