[FOM] Expository article on consistency of PA
Timothy Y. Chow
tchow at math.princeton.edu
Sun Nov 11 17:38:41 EST 2018
A expository paper of mine on the consistency of arithmetic that I
mentioned here on FOM a few months ago---
---has now appeared in the Mathematical Intelligencer, or at least on its
website in the "Online First" section:
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
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.
More information about the FOM