FOM: modeling PRA in the physical world

[Stephen G Simpson]

Commenting on a Hilbert's-program-like idea of formalizing
mathematical physics in conservative extensions of PRA (10 Mar 1999
13:26:50), Joe Shipman (11 Mar 1999 01:37:18) writes:

 > The problem is that some of the "ideal" elements "conservatively"
 > introduced in the *mathematical* type theory identified with
 > *physically meaningful entities* in the physical theory.  If you
 > "eliminate them" your ontology excludes not only infinite sets but
 > also wave functions, electrons, gravitational fields, and other
 > elements of reality.

Yes, I see your point.  But I don't see this as a fatal objection.  On
the contrary, it seems to me that the setup with T would be a good
framework for further foundational progress.  For example, if we later
decide to ontologically commit to waves, we can at that time move the
waves from the realm of the `ideal' into the realm of the `real',
i.e., instead of T being conservative over PRA we would now have T
being conservative over PRA + a theory of waves.  This might even be
better, because maybe the waves would help to axiomatize PRA in an
elegant way (infinite iteration ...).

Raatikainen 11 Mar 1999 13:10:58 writes:
 > According to Quine, this commits one to the existence of the
 > numbers, not to the existence of the SET of natural numbers ...

OK, I have probably misread Quine.  Let me restate my point more
sharply and without reference to Quine.

My point was that, although potential infinity is enough to justify
PRA, actual infinity may be needed to justify PA.  What's the
difference?  Well, the naive considerations leading to the PA
induction scheme or least element principle

  (Ex)Px -> (Ex)(Px & ~(Ey)(y < x & Py))

seem to apply only when P is a *definite* property of natural natural
numbers.  (E.g., it doesn't apply when Px is the property that x
grains of sand make a heap of sand.)  If the natural numbers don't
form a completed totality N, then an arbitrary property P defined by
nested quantification over N may not be sufficiently definite in this
sense, so the least element principle for P may not be justified.

PRA on the other hand assumes induction only for definite properties,
viz. primitive recursive ones, so this problem is avoided, and
potential infinity seems to be enough.

 > consider Robinson Arithmetic: even there one can prove
 > (x)(Ey)(x<y), but as a subtheory of PRA, it presumably can't make
 > stronger ontological commitments than PRA (?).

Well, yes, but Robinson arithmetic doesn't include any induction or
least element scheme.  (Also, as a possibly relevant technical point,
let me mention that PRA can be set up as a quantifier-free theory, and
then Robinson arithmetic is not strictly speaking a subtheory of it.)

 > recall that at least according to Bernays, Hilbert and his school
 > did not, before Goedel's 1933 result (Con(HA) --> Con(PA)), clearly
 > distinguish finitist and intuitionist mathematics.  

But now we understand this much better, and we sharply distinguish
finitistic arithmetic(= PRA) from intuitionistic arithmetic (= HA).

 > One may thus wonder what happens to Hilbert's program if one takes
 > HA instead of PRA as the unproblematic basic theory (as Bernays has
 > explicitly suggested).

A good question.  But here you are getting into the realm of
non-classical logics, or polylogism as I have been calling it lately.
Intuitionistic logic rejects some basic classical laws such as
either-or (tertium non datur).  Thus there are real questions about
whether intuitionistic logic is compatible with a broad view of
f.o.m. as being concerned with the place of mathematics in human
knowledge as a whole.  (What would intuitionistic physics look like?)
We can avoid these problems by sticking to PRA.

-- Steve