[FOM] stopping at ACA_0

[Nik Weaver]

Antonino Drago wrote (quoting me):

> > I like ACA_0 and am genuinely interested in knowing
> > whether it really has a "nice story" so I'll ask again.
>
> In a previous posting I recalled that Feferman's studies
> located the very important Weyl's elementary mathematics
> at the level of ACA_0.

Yes, but Weyl didn't suggest any philosophical reason for
stopping at arithmetic definability.  If I remember right
he was very clear about the possibility of going further
but felt that for his purposes (developing 19th century
real analysis in a predicatively acceptable way) there
was no need to do this.  In other words his criterion for
stopping at ACA_0 was esthetic.  Weyl scholars, please
correct me if I'm wrong about that.

Friedman claimed that it is "child's play" to come up with
a coherent foundational stance corresponding to ACA_0.  I'd
still like to see one.

Nik