[FOM] Expository article on consistency of PA

[Timothy Y. Chow]

A expository paper of mine on the consistency of arithmetic that I 
mentioned here on FOM a few months ago---

    https://cs.nyu.edu/pipermail/fom/2018-August/021163.html

---has now appeared in the Mathematical Intelligencer, or at least on its 
website in the "Online First" section:

    http://timothychow.net/consistent.pdf

In my opinion, the two most novel features of my exposition are:

1. the extra effort that I put into trying to make Gentzen's proof 
accessible to the "mathematician in the street," and

2. the explicit articulation of what a "strict formalist" is.

During the FOM discussion in August, José Manuel Rodriguez Caballero 
introduced the term "factually true," although I do not think that he 
responded to requests to clarify the exact meaning of this term.  Roughly 
speaking, I think that Caballero wanted to distinguish between 
mathematical statements X that one accepts "at face value" and those which 
one might pretend to accept at face value but secretly accepts only in the 
modified form "X is a theorem of formal system S."  For example, there is 
a certain kind of skeptic who might nod politely during a lecture in 
analysis where it is proved that "every differentiable function is 
continuous" but secretly only believes that "`every differentiable 
function is continuous' is a theorem of ZFC" whereas the same skeptic 
might accept "ZFC is inconsistent with Reinhardt cardinals" as "factually 
true" without first secretly appending "is a theorem of..."

I try to present Gentzen's proof in a way that I feel maximizes the 
chances that a skeptic will accept it as "factually true."  Existing 
accounts, I think, often make Gentzen's proof seem more infinitary than it 
actually is.  Caballero has denied that the conclusion of Gentzen's proof 
is "factually true" and I am curious as to whether this skepticism is 
based on a misapprehension of what exactly is entailed in the proof.

I introduce the term "strict formalist" in order to give a name to a point 
of view that (as I see it, anyway) takes formalism to its logical extreme. 
I have found that when I talk with someone who has formalist leanings, 
they often lack a clear concept of what (to borrow Caballero's term again) 
they accept as "factually true" and what they do not.  I often have to 
engage in an extended discussion before I can pinpoint where they stand. 
The virtue of giving the name "strict formalist" to an extreme position is 
that it helps speed up the "binary search" for the factual truth boundary. 
I can start by asking if they espouse strict formalism and do not even 
accept as factually true that "if you repeatedly apply `prepend an S' to 
the string `0' then you will never get a string with an `X' in it."  If 
they deny being this extreme, then we can work our way up gradually to see 
at what point they stop accepting mathematical theorems as being factually 
true.

Note that Ed Nelson was not a strict formalist by my definition.  In his 
article on taking formalism seriously, he spoke about the possibility of 
formal systems that are "demonstrably consistent."  In my article I argue 
that a strict formalist can never demonstrate the consistency of any 
system.  Sadly, of course, we can no longer discuss with Nelson exactly 
what principles he would accept in a valid demonstration of consistency, 
but perhaps when the next "Nelson" comes along, the term "strict 
formalist" will be a useful tool for clarifying his (or her) views.

Tim