[TYPES] Statement of structural induction

[Frédéric Blanqui]

Le 14/01/2018 à 02:18, Richard Eisenberg a écrit :
> Indeed, some responses have pointed out that because structural induction is equivalent in power to transfinite induction, it might be easier to teach the latter by reference to the former.

Hi. I would perhaps not say that it is equivalent but, for sure, 
structural induction can be justified by transfinite induction, which 
itself is a particular case of and is equivalent to well-founded 
induction. By the way, let me recall that the idea that well-founded 
induction should be preferred to transfinite induction and that, indeed, 
transfinite induction can be replaced by well-founded induction, is 
quite old. I believe that the oldest work about this is Kuratowski's 
1922 paper (in French) on "Une méthode d'élimination des nombres 
transfinis des raisonnements mathématiques" (A method of elimination of 
transfinite numbers in mathematical proofs) in Fundamenta Mathematicae 
(see https://eudml.org/doc/213282).

Best regards, Frédéric.