FOM: "Does Mathematics Need New Axioms?"

[Stephen G Simpson]

I downloaded Sol Feferman's short paper "Does Mathematics Need New
Axioms?" from

  ftp://gauss.stanford.edu/pub/papers/feferman/

I have some miscellaneous comments.

A. On the whole, I think this is a balanced and reasonable account of
the role of strong axioms in f.o.m. and can serve as background for
discussion of some absolutely crucial f.o.m. issues on the FOM list.

B. Minor criticisms.

  1. Bibliographical references are missing.
  
  2. I can't find "Woodin (1944)" in my library!

  3. (not so minor) My name is misspelled!
  
C. Applicable mathematics and PA.

I tend to concur with Sol's thesis that "a little bit goes a long
way", i.e. most if not all scientifically applicable mathematics ought
to be formalizable in systems of the same proof-theoretic strength as
PA, first order Peano arithmetic.  I would even go farther and replace
PA by something weaker, primitive recursive arithmetic.  See my paper
"Partial Realizations of Hilbert's Program", JSL 53, 1988,
pp. 349-363, or

  http://www.math.psu.edu/simpson/papers/hilbert/

However:

  1. Sol's case is weakened by the fact that he refers only indirectly
  and elliptically to some exceptional situations which might be
  counterexamples to his thesis.  Namely, Sol says:
  
    There are a couple of cases in some approaches to the foundations
    of quantum field theory which have been brought to my attention,
    where it appears one must go beyond the resources of PA; but the
    physical theories that require this additional strength are rather
    speculative.
  
  Sol, in connection with this remark, I have two questions for you.

    a. What specific mathematics and physics are you referring to?
  
    b. When you say "it appears one must go beyond the resources of
    PA", has this been established rigorously, e.g. by an appropriate
    reversal a la Reverse Mathematics?

  2. Sol mentions a slightly artificial finite combinatorial statement
  (due to Friedman-McAloon-Simpson, 1982) that goes beyond PA and
  indeed beyond predicativity.  But he doesn't mention the more
  dramatic independence results regarding Kruskal's theorem etc.  My
  favorite along these lines is that the graph minor theorem goes
  beyond PA and indeed beyond Pi^1_1 comprehension.  This is the
  Friedman-Roberton-Seymour paper in the Logic and Combinatorics
  volume (edited by me), American Mathematical Society, 1987.  For
  those who are unfamiliar with this, the graph minor theorem is one
  of the most important and striking results in combinatorics of this
  century.  It reads as follows.  Say that a finite graph G is a minor
  of a finite graph H if G is obtained from a subgraph of H by
  contracting edges; then there is no infinite set of finite graphs
  that are pairwise incomparable under `minor of'.  This kind of graph
  theory even plays a role in current computer science, e.g. the
  theory behind the design of VLSI chips.
  
D. Large cardinal axioms.

I also tend to agree with Sol's conclusion that, at this moment in
history, there is no compelling reason to accept large cardinal axioms
such as measurable cardinals, supercompact cardinals, etc.  But here
again, I think that Sol's case is not airtight, because he omits
discussion of some recent work that is relevant.

Specifically, Sol mentions the well-known fact from the 60's that
large cardinal axioms don't settle the continuum hypothesis, but he
doesn't discuss Woodin's recent book.  Woodin argues that there is a
natural "maximal" model of set theory, Pmax, in which CH fails.  Large
cardinals play a significant role in this model.  Unfortunately I
haven't read Woodin's book myself, but it seems to be causing a stir
in set-theoretic circles.  I think we need to take account of Pmax.
Provocative question: Is Pmax real, or is it so much hot air?

-- Steve