[FOM] Reverse mathematics in two dimensions
Paul Budnik
paul at mtnmath.com
Mon Aug 31 10:56:41 EDT 2009
There are two dimensions that characterize the complexity of a
mathematical statement: definability and provability. It takes a certain
level of mathematical language to make the statement and it requires
induction up to a specific ordinal to prove or refute the statement. The
existing, very successful, reverse mathematics project combines these
two dimensions by looking for the simplest formal system that decides
the statement.
This tends to obscure a problematic aspect of the ordinal hierarchy. The
ordinal hierarchy provably definable in any finite (or recursively
enumerable) formal system strong enough to include the ordinal of the
recursive ordinals, is full of holes. In particular it cannot include
all recursive ordinals.
This leads to results such as Harvey Friedman's recent post
(http://cs.nyu.edu/pipermail/fom/2009-August/013979.html) that includes
an "explicitly Pi03" statement (Proposition 1.1) that is "provable in
SMAH+ but not in any consistent fragment of SMAH"
'SMAH+ = ZFC + "for all k there is a strongly k-Mahlo cardinal". SMAH =
ZFC + {there is a strongly k-Mahlo cardinal}_k.'
For any Pi03 statement S, there is a recursive ordinal notation O, such
that S is provable in second order arithmetic + the axiom that O is the
notation for a recursive ordinal. This must be true because the set of
all recursive ordinal notations is a Pi11 complete set.
Large cardinal axioms are needed to decide proposition 1.1 only because
existing mathematics does not define sufficiently many recursive
ordinals. Large cardinal axioms implicitly define large recursive
ordinals and I would speculate that is how they are able to decide such
problems. I think it is premature to suggest that such results establish
the relevance of large cardinal axioms to core mathematics.
I am not aware of any work that is at all close to developing an
explicit notation for a recursive ordinal large enough to prove the
consistency of ZF and this problem would require a significantly larger
ordinal. However my expectation is that such notations will eventually
be developed probably using the computer as a research tool.
Paul Budnik
www.mtnmath.com
More information about the FOM
mailing list