[FOM] extramathematical notions and the CH

[Nik Weaver]

Sam Sanders asked "what are weak systems still sufficient to formalize
the Math used in Physics?"

I think it is hard to do "reverse physics" because what math is actually
used in physics is open to interpretation.  The point I try to make is
that impredicative mathematics is totally unrelated to anything that
would normally arise in mathematical physics.  But if you try to pare
it down to the minimal foundational system that would support physics
you enter a grey area.  Do we really need the exists of solutions to
ODE's with continuous initial data?  Or should we be willing to impose
some regularity condition on the data that weakens the strength of the
existence theorem?  Etc.

Joe Shipman writes

> With careful coding one can formalize all of the physics in some
> subsystem of second order arithmetic, but when so formalized the
> physics becomes opaque and all intuition is lost. It makes much more
> sense to allow real numbers, functions on real numbers, operators on
> such functions, and so on for some finite number of levels.

This is a fair point (though probably not what Sam was asking), but
I can answer it.  All you need to do is add third order variables
to your second order subsystem.  You can make a conservative extension
in which sets of reals can be represented directly, without special
coding.  And you don't have to keep adding levels, once you have sets
of reals all the standard Banach spaces are available.  We don't need
to accomodate crazy spaces of nonmeasurable functions and so on.

Such an extension is quite natural from the predicative point of view.
First order variables are numbers, second order variables are sets,
third order variables are classes.  It's analogous to passing from
ZFC to NBG.  I did this in my paper about axiomatizing mathematical
conceptualism which I already referred to in a recent post (and went
into some detail about how much analysis can be straightforwardly
formalized).

Criticizing subsystems of second order arithmetic as being "opaque"
is a bit of a straw man, because the point of the reverse math program
is to make technical calibrations, not to provide intuitive foundations.
If that's what you want, add third order variables.

Nik