[FOM] extramathematical notions and the CH
sasander at cage.ugent.be
Wed Feb 6 14:44:45 EST 2013
> 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. )
More information about the FOM