[FOM] Convincing Edward Nelson that PA is consistent

[Timothy Y. Chow]

Sadly, of course, Nelson passed away a few years ago so there is no way we 
can literally convince him that PA is consistent.  However, in the process 
of writing an expository article about the consistency of PA, I thought of 
a way that "normal" people could potentially make some progress on the 
project that Nelson was engaged in---though of course in the direction of 
showing that PA is consistent rather than inconsistent.

Since Nelson's views were unusual, I have to give some philosophical 
preamble.  I would like to introduce the term "strict formalist."  A 
strict formalist is able to *follow* prescribed syntactic rules and can 
for example verify that a given mathematical proof (of feasible size) 
follows from given axioms, but takes very seriously the claim that the 
symbols and strings do not *mean* anything.  In particular, the strings 
cannot refer to syntactic objects, and an expression such as "Con(PA)" 
cannot mean anything, let alone mean something about what happens if you 
manipulate the axioms of PA according to the rules of first-order logic. 
This is not just because "Con(PA)" is usually formulated as an 
arithmetical statement; even if we use something like Quine's protosyntax 
that is supposed to directly formalize syntactic reasoning, the strict 
formalist refuses to *interpret* protosyntax as "saying" anything about 
syntax.

It's a pretty good approximation to think of a strict formalist as a 
computerized proof assistant.  To drive home the point that strict 
formalists only *follow* rules and don't *reason* about them, imagine 
starting with the symbol "0" and then repeatedly applying the rule 
"prepend an S."  The results, of course, will look like this: S0, SS0, 
SSS0, SSSS0, ....  You and I look at this and can reason that at no point 
will we obtain a string that contains (say) a "+" sign in it.  However, 
this observation is a piece of *mathematical reasoning* and is unavailable 
to the strict formalist.  The strict formalist can verify on a 
case-by-case basis that "S0 has no + in it," "SS0 has no + in it," etc., 
but that is all.

I introduce the concept of a strict formalist as a "baseline."  The strict 
formalist is able to accomplish the main task that formalists are eager to 
affirm, namely recognizing syntactic objects, manipulating them according 
to certain rules, and verifying that the rules have been correctly 
applied, but is an absolute mathematical dullard.  Implicitly, a strict 
formalist could verify that PA is inconsistent by checking the correctness 
of a PA proof of 0=S0, but would not be able to perk up and say, "Hey, 
look at that---PA is inconsistent!"  It is therefore impossible to present 
an argument to a strict formalist that will get the strict formalist to 
affirm (in English) that "this system is *inconsistent*" let alone the 
more subtle claim that "this system is *consistent*" for the trivial 
reason that strict formalists are not in the business of affirming 
mathematical statements in English.

In practice, I don't think any human being is a strict formalist.  In 
Nelson's paper "Taking Formalism Seriously," he doesn't take formalism as 
seriously as a strict formalist does.  At the end, he talks somewhat 
vaguely about proving that some weak system is consistent in a way that 
will "convince the most skeptical of formalists."  Of course, a strict 
formalist is even more intransigent than what Nelson envisages as "the 
most skeptical of formalists," but the point is that the concept of a 
strict formalist lets us see that Nelson is slipping in some extra 
assumptions.  Namely, Nelson is tacitly allowing the possibility that 
*some kinds of mathematical arguments can provide us with secure knowledge 
about syntactic objects*.  The symbols used to record these mathematical 
arguments are not just meaningless symbols, to be manipulated according to 
certain rules; they *tell us something* about the behavior of syntactic 
entities.

To my knowledge, Nelson was never explicit about exactly what mathematical 
principles "the most skeptical of formalists" would accept.  I would 
presume that Nelson would allow us to conclude "PA is inconsistent" if we 
were presented with an explicit proof of a contradiction from PA.  I would 
also presume that Nelson would allow us to conclude that if all we do is 
repeatedly prepend "S" to "0" then we will never get a "+"---although even 
here, I think we have to be careful what "never" means, because Nelson is 
what I would call an ultrafinitist.  The sequence S0, SS0, SSS0, ... 
gradually fades off into meaninglessness because the strings get 
infeasibly large.  Characterizing this "fading off" in a way that is 
mathematically analyzable is notoriously difficult and probably can't be 
done in a fully satisfactory manner; however, one can try to work around 
it by setting some upper and lower bounds on the fading off point (maybe 
2^1000 and 2^100 respectively, using conventional mathematical notation).

Now here is an important step: I maintain that the most plausible way to 
interpret "PA is consistent" in this context is "There is no *feasible* 
PA proof of 0=S0."  Again, exactly what this means is tricky, but the 
conventional mathematical claim that "There is no PA proof of 0=S0 shorter 
than 2^1000 symbols" should imply it.

We're now in a position to pose a question that makes sense to a 
conventional mathematician: What are the weakest mathematical principles 
that allow us to deduce "There is no PA proof of 0=S0 shorter than 2^1000 
symbols"?

What makes this particularly tricky is that "the most skeptical of 
formalists" isn't going to be happy interpreting "2^1000" the way a 
conventional mathematician does.  So we have to be careful when we deal 
with exponential notation, and perhaps even multiplicative notation.  At 
the same time, if we are to have any hope of making progress, we have to 
allow *some* principles that allow us to prove theorems of length n that 
"say something about" syntactic entities of length N when N >> n. 
Otherwise we can't approach "PA is consistent" other than by direct 
exhaustion.  I'm not sure exactly how to proceed at this point, but if 
this issue can be addressed, then I can imagine that in principle, "the 
strictest of formalists" could become convinced that "PA is consistent," 
by carrying out something like the following:

1. Do a computation with 1000 steps to arrive at a theorem that says
that there is no PA proof of 0=S0 of length 1000000.

2. Do a computation with 1000000 steps to arrive at a theorem that says 
that there is no PA proof of 0=S0 of length 1000000000000.

3. Etc.

Here I've arbitrarily picked an "expansion factor" of n -> n^2.  That 
means that by getting up to the square root of the feasibility bound, the 
"most skeptical of formalists" can become convinced that there is no 
feasible contradiction.  I can imagine developing some kind of sliding 
scale, where progressively stronger mathematical principles give you 
bigger expansion factors.  Very skeptical formalists might have to get up 
to the square root of the feasibility bound to be convinced that PA is 
consistent, while less skeptical formalists might only have to go up to 
polylog.

Tim