FOM: modeling PRA in the physical world

[Raatikainen Panu A K]

Concerning my suggestion:
>> 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).

Simpson wrote:
>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.

Well, in real life, I agree completely - I have no sympathy for
polylogism, nor do the intuitionistic arguments against LEM convince
me of the claim that intuitionistic logic is the true logic. However,
I think there is still some interest in considering what one could say
in answer to a passionate intuitionistic critic of the ordinary
classical mathematics (I think this was, in some part, Hilbert's aim, 
i.e. to reply to Brouwer and Weyl) - and for such a line of defence, 
PRA is unnecessarily weak (and this was something Hilbert et al did 
not realize). What I suggested that one can, a la Hilbert's program, 
show that one can freely use, say, full Konig's lemma, or ACA_0 (i.e. 
what I called "the ordinary mathematics"), for being conservative 
over HA, for Pi-0-2-sentences, these cannot prove any 
intuitionistically false "real" statements.  I see here a further 
important philosophical application of Reverse Matematics and related 
research (assuming that my line of reasoning is correct - is it ? for 
som further details, see the end of my earilier posting (11 March)).

Further, Simpson writes:
>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.

I agree that actual infinity is needed to justify the least element
principle (and hence PA). However, also intuitionists - who also
accept only potential infinity - do accept induction scheme and nested
quantification (in HA);  the least element principle follows from 
induction only with classical logic.  Well, my point here may be 
rather trivial; I merely want of underline the role of the choice of 
logic (classical/intuitionistic).

My point about Robinson Arithmetic was that your eariler claim ("
nested quantification over a domain ... requires an ontological
commitment to the (actual) existence of that domain") is problematic -
for I presume that you do not think that Robinson Arithmetic requires
such an ontological commitment ??? And there is nested quantification
over domain in it. (Do we agree here?) Your  later emphasize on the
least element principle seems to me, on the other hand, to justify
your basic claim.

Anyway, these are matters of detail - I agree completely about the
fundamental difference between  PRA and PA (potential/actual
infinity). It just seems to be less easy to state simply what aspect
of PA explains this difference ... Perhaps one should say that it is
only the interplay of  addition and multiplication (compare decidable
theories such as Presburger Arithmetic), full induction sheme (compare
PRA) and classical logic  (compare HA) together ...

- Panu Raatikainen