FOM: modeling PRA in the physical world

[Raatikainen Panu A K]

In 5 March Simpson wrote:
>One can argue that nested quantification over a domain (i.e.
>locutions such as `for all x in the domain D there exists y in the
>domain D such that ...') requires an ontological commitment to the
>(actual) existence of that domain.  I think Quine has argued this
>way.

According to Quine, this commits one to the existence of the numbers,
not to the existence of the SET of natural numbers (as Tennant pointed
out, without reference to Quine) - compare the situation in set theory
without and with the axiom of infinity. Also, 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 (?).

>One can argue that PRA is implicit in the physical fact
>that many kinds of discrete acts can be repeated a potentially
>infinite (or at least an unlimitedly large finite) number of times.

I wonder whether one could extend this to Heyting Arithmetic HA, i.e.
I doubt that mere Induction Scheme as such (especially without
classical logic) commits one to actual infinity (??)

Earlier (1 March) Simpson wrote:
>One approach to (b) would be to argue that PRA is consistent because
>the physical world provides a model of it, and then to justify at
>least a significant fragment of mathematics by reducing it to PRA, a
>la Hilbert's program of finite reductionism.

I have always thought that this line of reasoning is extremely
interesting. However, I would like to suggest that it could be easily
generalized. First, 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. 
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).

Now by the result of Kreisel and Friedman, PA is conservative over HA
for Pi-0-2 sentences, and Friedman's ACA_0 is in turn conservative
over PA. Hence ACA_0 cannot prove any real (Pi-0-1) sentences that are
not provable already in HA. Thus the use of ACA_0 (or eg. the full
Konig's lemma) is is this sense harmless (but efficient).

Moreover, thanks to Friedman and Simpson we now know that (more or
less) all the ordinary mathematics can be developed in ACA_0. (Can one
really put the issue this strongly? But at least to me it appears that
all the stronger theorems belong to descriptive set theory...)

Finally, as one can (Gentzen -36, Goedel -58) give an
intuitionistically acceptable consistency proof for HA (although
obviously not in HA), one can give a Hilbert-like justification for
all the ordinary mathematics, assuming one takes intuitionist instead
of finistist methods as basic. (???)

This is how I have started to see this field, rightly of wrongly ...

Comments ?


Panu Raatikainen
Assistant Professor
University of Helsinki
P.O. Box 24
FIN-00014 University of Helsinki
Finland

E-mail: panu.raatikainen at helsinki.fi