[FOM] Reverse mathematics in two dimensions

[Paul Budnik]

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