FOM: arithmetic, geometry, natural science, formal systems, ...

[Stephen G Simpson]

Harvey Friedman writes:
 > 1. Arithmetic as motivated by casual considerations of physical reality.
 > 1'. Arithmetic taken as statements about physical reality.
 > 2. Geometry as motivated by casual considerations of physical reality.
 > 2'. Geometry taken as statements about physical reality.

Robert Tragesser writes:
 > One standard view of PRA (or in any case finitist mathematics) is
 > that it be fundamental for nature/physics (Hilbert; Simpson in
 > Partial Realizations of HP especially).  ....

Yes, I do take the view that PRA or finitism is fundamental.  Harvey's
distinctions are relevant.  

Let me now elaborate a little bit on my viewpoint or working
hypotheses in my paper on partial realization of Hilbert's program.

The following is only a rough sketch, and I don't claim that my ideas
are fully worked out or in final form.  I'm putting this stuff out
there for people to pick holes in if they want to, and maybe some good
will come of it.  I do claim that my ideas are based on some thought
and experience in f.o.m.

science -- systematic study of subjects.

logic -- the science of correct inference.  

natural science -- the study of nature, i.e. the real world.

[ Digression: I want to suggest that the correct logic for natural
science is classical rather than intuitionistic.  Identity,
non-contradiction, excluded middle: these are bedrock for me, because
reality is real, independent of our understanding of it.
Intuitionistic logic may be useful for other purposes, e.g. as a
description of *our understanding of reality at a given point in
time*, because if we are not now in a position to confirm or deny X,
then neither X nor not X is now known.  But natural science is the
study of what's real, not the study of *our current understanding of*
what's real.  That's why I focus on classical rather than
intuitionistic logic. ]

mathematics -- the science of quantity, i.e. quantitative aspects of
reality.  

There are two kinds of quantities that immediately present themselves
to us in nature: *numbers* (or, perhaps, finite sets?) and *shapes*.
Thus two key branches of mathematics are arithmetic (finite set
theory?) and geometry.  Of course arithmetic applies to finite sets of
objects other than 3-dimensional physical entities, and geometry also
applies to situations other than 3-dimensional shapes, e.g. the
geometry of physical systems with n degrees of freedom.

physics -- the science of matter and energy.  It's a mistake to assume
that all natural science can be reduced to physics.

mathematical physics -- mathematical developments that are suggested
by physical considerations, especially by some of the more speculative
parts of quantum mechanics and cosmology.  A lot of the modern
developments (string theory etc) may or may not apply to real-world
matter and energy.

foundations of mathematics -- the study of the most basic concepts and
logical structure of mathematics, with an eye to the unity of human
knowledge.

What is the proper approach to f.o.m. in the present historical era?

Well, modern physics (relativity, quantum theory, ...) has succeeded
in casting doubt on basic geometrical concepts such as straight line
and continuity, but in my opinion nobody has succeeded in casting
doubt on the concept of number in any serious way.  Therefore, at the
present time, it may be appropriate to take an arithmetical approach
to f.o.m. rather than a geometrical approach.  This is admittedly a
debatable point, but I accept it in my own f.o.m. research, as do many
other f.o.m. researchers.

>From this perspective, let's look at some of the commonly considered
formal systems for mathematics.  The ones I know best, in order of
increasing logical strength:

  feasible or PTIME arithmetic, EFA, PRA, RCA_0, WKL_0, ...

  PA or 1st order arithmetic, ACA_O, predicative analysis, ATR_0, ...

  Pi^1_1-CA_0 and other subsystems of 2nd order arithmetic

  type theory, Zermelo set theory, ZFC, ZFC + large cardinals

I think that each of these formal systems can be coherently motivated
in terms of some ontological commitments or philosophical assumptions
about numbers, sets of numbers, sets in general.  Naturally the
stronger systems are going to get more and more debatable or
questionable in terms of their applicability to nature, i.e. the real
world.

feasible or PTIME arithmetic -- this seems to be more about what we
can practically compute.  It's part of what is real, but not all of
it.  PTIME f.o.m. is for you if you want to argue that everything in
mathematics is or can be or should be computable in a practical sense.

EFA -- elementary function arithmetic.  The natural numbers, zero,
successor, plus, times, exponentiation.

I would argue that exponentiation of natural numbers, x^y, is fairly
realistic, at least in terms of the Aristotelean potential infinity.
For instance, consider a sheet of paper or a computer terminal screen,
80 characters wide by 66 lines high.  There are 95 ASCII characters,
so we can describe the list of all 95^(80*66) potential pages, the
list of 2^(95^(80*66)) potential sets of potential pages, etc.  Is
this feasible?  I don't know, but it seems real to me, because as
Aristotle said, potential existence is a kind of existence, and
therefore it's within the scope of natural science.

PRA -- primitive recursive arithmetic.  The Ackermann hierarchy,
A_1(x) = 2x, A_{n+1}(x) = A_n...A_n(1) where A_n is iterated x times.
It's a bit of a stretch, but I think we can justify this as a natural
extension of EFA describing aspects of the real or natural world,
e.g. iteration.  (It's known that EFA has the same strength as
*bounded* primitive recursive arithmetic.)  See also Tait's paper on
finitism, J Phil 1981.

RCA_0 -- a formalized version of computable or recursive mathematics.
No ontological commitments beyond the recursive functions, which form
the smallest omega-model of it.  It can be shown that RCA_0 is
conservative over PRA for Pi^0_2 sentences.

WKL_0 -- RCA_0 plus a compactness principle, saying that there are
"enough points".  This allows many non-constructive mathematical
theorems to be proved.  The existence of non-computable sets and
functions is explicitly provable in WKL_0.  Like RCA_0, WKL_0 is
conservative over PRA for Pi^0_2 sentences, but not in such a nice
way.  For instance, there is no minimum (or even minimal) omega-model
of WKL_0.

The conservation results for RCA_0 and WKL_0 justify a lot of standard
results in analysis, geometry, etc, in the weak or indirect sense of
Hilbert's program, i.e. finitistic reductionism.  Applying this
directly to shapes of physical objects and other natural science
applications is not so easy, but I think there is a way.

PA, ACA_0, predicative systems -- now it's getting murkier.  The
arguments that PA et al apply to the real world seem to depend on
accepting the natural numbers as an actual infinity, N or omega, not
just a potential infinity.  And by Aristotle this seems questionable
from the natural science viewpoint.

Of course ACA_0 is conservative over PA, and some people may decide to
declare (with apologies to the finitist Kronecker) that the completed
totality N is God's creation and the rest of mathematics is the work
of man.  In this way we "recover" many mathematical theorems that are
provable in ACA_0 but not in weaker systems.

By working out additional consequences of the commitment to N, it may
even be possible to justify some predicative systems on this basis.
See Feferman's writings on predicative analysis.  However this does
not seem to give many mathematical results beyond ACA_0.  On the other
hand, ATR_0 is conservative over predicativity for Pi^1_2 sentences,
and this does give some significant additional mathematical results,
especially in descriptive set theory, Borel sets, etc.

Pi^1_1-CA_0 et al -- murkier still.  People have explained Pi^1_1
comprehension as conservative over ID(<omega) for a certain class of
sentences.  Here ID(<omega) is a theory of iterated inductive
definitions.  Not very convincing in terms of natural science.

Type theory and set theories -- murkier still.  What does aleph_2
refer to in reality?  Aleph_omega?  The first measurable cardinal?

I'll stop here for now.

-- Steve