[FOM] consistency of PA?

[Randall Holmes]

Dear FOMers (cc NF list):

I hereby (and thankfully) retract the purported proof of ~Con(PA).  I
found the error myself, but I thank Bob Solovay for thinking about it
(and asking the right question, which put me on the track of where the
error in my intuition was).  I also thank other FOM members whose mail
I didn't see until after I found the mistake.

It's a consequence of spending too much time thinking about this
(I lost sleep tracking down the error in Bryan Ford's proof, and lack
of sleep and contemplation of unspeakable horrors probably caused my
subconscious to produce this :-)

I should know better: I once spent a lot of time trying to disprove
Con(NF) by developing a truth definition in ambiguous type theory with
negative types; even with the added information that shifting types
couldn't change the values of formulas, one couldn't do too much
(though one could prove amusing things about the structure of the tree
of iterated inverse images of the cardinality of a type under the
exponential map).  So I do know something about how these kinds of
arguments fail.

There are two interesting questions:

1.  is it even possible for ~Con(PA) to hold?

I would normally say not (I prefer to think that second-order logic is
non-problematic, and so the notion of the set of natural numbers is
definable in logic; the existence of a model depends on the premise
that there are infinitely many objects, which is not a logical truth
but does not seem at all problematic).

There are those who entertain doubts about the natural numbers (and
more who entertain doubts about analysis or higher set theory) on
grounds of impredicative reasoning ("defining" sets in terms of
collections of sets to which they themselves belong: N is defined, for
example, as the intersection of all inductive sets, but it is itself
an inductive set); but I wonder how many of these to expect
predicative reasoning to become _obligatory_; ~Con(PA) would be the
result which would say essentially that all impredicative reasoning is
not just dangerous but wrong.  As I say above, I don't normally fall
into the category even of those who have doubts, though I find
predicative systems technically interesting (there's a subsystem of NF
related to predicative type theory, which is known to be consistent,
unlike NF itself).

Can one form an intuitive picture of what the world would be like if
PA were not consistent?  It seems uncontroversial that N is there: if
we have an object to be 0 and a universally applicable "successor
relation" (both are available in predicative set theories) it would
seem that we should be able consistently to contemplate the
intersection of all inductive sets (or even the intersection of all
inductive classes, if our set theory is known not to have a set which
is the intersection of all inductive sets.)  If the intersection of
all inductive classes is a class and we can define (proper!) classes
in a suitable way, then there is a copy of N.  

But there is a way in which this could seemingly fail to happen: if
one could prove that inductive collections form an inconsistent
totality -- specifically that from any collection A of inductive
collections one can form an inductive collection properly included in
every element of A but not itself an element of A, then the
"intersection of all inductive classes" would become logically
impossible.  (I am not proposing a program to look for such a
construction; I'm just trying to imagine a situation in which
intuition could be trained not to "see" N).  This would mean that our
ability to define classes would be impaired: we could not define
even proper classes using quantification over all proper classes, as
otherwise we could develop a proper class N satisfying PA.

With regard to N as a set or class there would be two possibilities:
one could restrict the conditions that can define sets in logical
complexity, and one might retain the notion that N is the intersection
of all inductive sets (some theories based on computability might look
like this).  In a predicative set theory (such as the ramified theory
of types) one would be able to define intersections of all inductive
sets of a given order, which would turn out to be an inductive set of
a higher order.  Such a set "N" would be a good approximation to the
ideal N, but it would contain nonstandard elements which even higher
order inductive sets would exclude.  Similar things would happen to R;
in such a theory nonstandard analysis might be popular, because
unavoidable :-)

2.  A mathematical program: are there interesting consequences of
~Con(PA) over a predicatively acceptable base theory?  (Note that this
is NOT a program to look for a proof of ~Con(PA)).

First of all, what does ~Con(PA) mean?  If one is working in predicative
type theory, where one loses a unique notion of N if PA is
inconsistent, one also loses a unique notion of "proof" (the
collection of proofs is defined as a closure in much the same way that
N is).  One would have multiple "notions of proof" (classes of
formulas closed under one's inference rules) which would (on my
intuitive picture) form an inconsistent totality just as the inductive
sets would...  One could formulate the assertion ~Con(PA) as "every notion
of proof for PA includes "false" ", but quantification over an inconsistent
totality should cause qualms in a predicative context (though I'm
not using it to define a set or even a class).  What is known about
predicative proof and model theory?  This sounds like something that
people who do reverse mathematics might know about...

Does the theory "ramified theory of types plus ~Con(PA)" (or something
with a more notationally convenient predicative set theory in place of
RTT) have interesting consequences over and above the obvious fact
that any approximations to the set of natural numbers turn out to have
extraneous elements?

--Randall Holmes