[FOM] Set theory with Inf and ~Con(PA)?

[Timothy Y. Chow]

Let me try to translate some of the recent philosophical discussion about 
the inconsistency of PA into more precise mathematical questions.

Mathematicians are unlikely to give up set theory, even in the face of
an inconsistency in PA, unless they're forced to.  So, how might they
go about reformulating set theory?

An explicit derivation of a contradiction in PA should, I believe, be
straightforwardly translatable into a contradiction in ZF - Inf.  Suppose
that we nevertheless want to keep as much of ZFC as possible, and in
particular we want to keep Inf.  What options are available?

My guess is that the most promising approach would be to throw away a
bunch of instances of the separation/comprehension axiom schema.  (This
corresponds to my informal proposal to retain N but to discard some of its
"properties.")  Are there any known results about the equiconsistency, or
at least the relative consistency, of

     "PA minus such-and-such instances of the induction schema"
and  "ZFC minus such-and-such instances of the comprehension schema"?

Note: I'm primarily interested in ZFC surrogates that are still strong
enough to prove "N exists and is unique" or something to that effect.

The idea is that if PA is found to be inconsistent then we could shift to 
a suitable surrogate of ZFC and retain most set-theoretic language---even
infinitary language---without change.

--------------------------------------------------------------------------

On a different but related note, let me repeat two other questions about
fast-growing functions that I raised earlier but which may have gotten
buried in all the traffic.  They are motivated by the suggestion of David 
Isles that the notion that N is closed under primitive recursive functions 
is an assumption over and above the notion that N is closed under tamer
functions.

1. Is it provable in a weak system that "If PA is inconsistent, then
   such-and-such a fast-growing function is not total"?

2. PA doesn't prove that "the length of the nth Goodstein sequence" is
   a total function.  Is there an analogous arithmetical statement
   that is unprovable in ZFC?

Tim