[FOM] extramathematical notions and the CH

[Sam Sanders]

> I think it is hard to do "reverse physics" because what math is actually
> used in physics is open to interpretation.

I give such an interpretation below.

>  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.

Agreed.  Minimal would be extremely difficult.

>  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.

Physicists will generally tell you that they will assume whatever mathematical condition
that is somehow necessary to make the problem approachable (e.g. C^\infty for functions).
In this way, one does not use Peano's Existence Thm (which is equivalent to WKL_0 given RCA_0) in physics,
but the weaker Picard Thm (or something similar provable in RCA_0).

I propose an alternative way out:  The Peano existence thm "For all f such that …, there is a function y such that y'= f (x , y )" 
is not arithmetical or Pi_1^1.  However, physicists would be happy with "For all e>0 and  f, there is a function y such that | y' - f (x , y ) | < e ", 
as there is always some finite measurement error in practice.  Furthermore, the latter statement can be made Pi_1^1:  

"For all e>0 and  f, there is a polynomial y such that for all *rational* x, we have  | y' - f (x , y ) | < e "
 
By Harrington's thm, the previous is then also provable in RCA_0 and for the practice of 
physics, it is as good as Peano's theorem.  The theory is of course a different story.  

(The *rational* above may be replaced by "all computable reals", I think.  )

Best,

Sam