[FOM] induction and reducibility

[Robert Black]

Well, yes, but it's a drastic case. What Myhill shows is (roughly: I 
haven't studied his paper with the care it deserves, because ramified 
type theory makes my eyes go funny) that if without reducibility we 
define N as the set of all the objects possessing every level-k 
property possessed by 0 and inherited under succession then we don't 
get induction for properties of level >k, and thus in particular we 
don't get it for properties defined via a quantification over N, i.e. 
most of the arithmetical properties we might be interested in. I 
don't think this is a surprising result, but it can't be trivial, or 
Goedel wouldn't have left it (as he did) as an open question.

Robert

>I am interested to hear Robert's contribution - particularly the
>historical detail. However we mustn't infer from this any particular
>significance about reducibility.  The point is that reducibility functions
>as a set existence axiom, and - since we define the naturals inductively
>as the intersection of all *sets* containing 0 and closed under S - each
>time we prove the existence of a new *set* we obtain the use of another
>instance of the induction scheme.
>
>
>So it's an instance of a perfectly general phenomenon, and not really a
>specific fact about reducibility.