FOM: finitist prejudices

[Stephen G Simpson]

Joe Shipman 09 Mar 1999 09:39:48
 > > What if we could develop the requisite functional analysis in a
 > > subsystem of second order arithmetic that is conservative over PRA?
 >
 > ... the functional analysis still has an ontology involving
 > uncountable sets

Joe, you seem to be saying that by writing down these conservative
extensions of PRA we are ipso facto committing ourselves to a certain
ontology involving uncountable sets.  I disagree.  I think you are not
giving due consideration to Hilbert's ideas in his Hilbert's program
paper.  My suggestion above is very much in the spirit of Hilbert's
program.  See also my paper
<http://www.math.psu.edu/simpson/papers/hilbert/> and my book
<http://www.math.psu.edu/simpson/sosoa/>.

Hilbert's point (as I read him) is that it's OK to introduce new
mathematical entities conservatively over old ones, and this does not
increase our ontological commitments.  Hilbert views this as a variant
of a well established mathematical procedure, the `method of ideal
elements'.  The new entities are not `real'; they are `ideal', i.e.,
instrumentalities that we introduce for our convenience.
Conservativity implies that we can freely use the new entities to
prove theorems about the old entities, and the new entities can always
be `eliminated' if we want.  A simple example is the conservative
introduction of the complex numbers as ordered pairs of real numbers.
These ordered pairs don't have to correspond to anything in reality;
they are mere instruments, and they can be eliminated.

 > If the coding of the functional analysis into second-order
 > arithmetic is straightforward and preserves meaning (by this I mean
 > that "physically meaningful" entities in the original theory have
 > manageable representations as sets of integers) ...

The coding into Z2 and PRA is reasonably nice, but I don't think it
has the properties that you want.  For instance, real numbers, Banach
spaces, operators on Banach and Hilbert spaces, etc, would be coded as
sets of non-negative integers.  This does not seem to be physically
meaningful.

However, that doesn't matter, because the coding in question is merely
a technical device used to prove the relevant conservation results.

Here's the situation.  There is a big, many-sorted theory, call it T,
containing many kinds of entities: natural numbers, integers,
rationals, reals, complex numbers, separable Hilbert spaces, separable
Banach spaces, operators on separable Banach spaces, countable
algebraic structures, etc etc.  Many theorems of functional analysis
can be proved in T, yet T is conservative over PRA for Pi^0_2
sentences, via the obvious interpretation of PRA into it.  

This is a far-reaching partial realization of Hilbert's program.  It
seems to go a long way toward answering your implicit question.  I
take your question to be, how can we make mathematical sense out of
functional analysis used in quantum physics, without ontologically
committing ouselves to uncountable sets?  I think T shows how to do
that.

 > What do you think of my proposed test for finitists?  (The test is
 > whether one is more bothered by the unsolvability of Diophantine
 > equations or the undecidability of the Continuum Hypothesis.)

I don't think it's a good test, because it's too touchy-feely, too
subjective.  The issue of finitism versus non-finitism is an objective
scientific issue.  To formulate it as an issue of who is bothered by
what seems misleading.

-- Steve