[FOM] Convincing Edward Nelson that PA is consistent

Mon Jun 25 15:03:16 EDT 2018

I hope that this paper would convince Edward Nelson (of course, if he
lived) that Peano's Arithmetic is consistent: T. J. Stępień, Ł. T.
Stępień, „On the Consistency of the Arithmetic System", _Journal of
Mathematics and System Science_, vol. 7, No. 2, 43 - 55 (2017);
arXiv:1803.11072 . 

                                                Łukasz 

---

Lukasz T. Stepien

The Pedagogical University of Cracow
Institute of Computer Science,
ul. Podchorazych 2
30-084 Krakow
Poland

tel. +48 12 662-78-54, +48 12 662-78-44

The URL  http://www.ltstepien.up.krakow.pl

On 2018-06-19 05:56, Timothy Y. Chow wrote:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180625/1124bd0d/attachment.html>