# [FOM] Provability of Consistency

Timothy Y. Chow tchow at math.princeton.edu
Wed Mar 27 21:58:37 EDT 2019

```Sergei Artemov wrote:
> I am glad that you agree with my principal point. I wish others will

Well, I'm not sure exactly what you consider to be your principal point,
because there's at least one thing you said that I strongly disagree with,
which seems to be one of your principal points.  You did not respond to
what I said, so let me restate, and ask a direct question.

As before, let S be the formal string

S = "NOT exists x exists y exists z : x*x*x + y*y*y + z*z*z = 42"

I'm being slightly sloppy here because the above doesn't quite conform to
the usual syntax of the first-order language of arithmetic---I have
omitted parentheses in the right-hand part and I have written 42 in
conventional decimal notation, and most importantly, I am quantifying over
integers (positive and negative) rather than over natural numbers.  But I
think you know what I mean, and could convert to a strictly correct formal
string in the first-order language of arithmetic if desired.

My direct question to you is this: Do you consider S to be a satisfactory
formalization of the statement, "the sum of three cubes is never equal to
42"?  By "satisfactory" I mean, do you believe that if someone comes up
with a correct finitistic proof that the sum of three cubes is never equal
to 42, then that proof can be converted into a formal proof of S from the
axioms of PA?

My own answer to the above question is yes.  Surely one of the main points
of formulating PA is to investigate proof-theoretic questions such as
this.  And surely if any number-theoretic statement can be satisfactorily
represented by a formal string in the first-order language of arithmetic,
"the sum of three cubes is never equal to 42" had better be one of them;
it doesn't get much simpler than that.  And surely if there is a
satisfactory representation of that statement by a formal string, S had
better be it; again, it just doesn't get any simpler than this.

I would hope that you would agree.  But now let me argue, using a slight
modification of your own arguments, that the answer is no.  If S is an
the face of future mathematical discoveries.  As I mentioned before, it
happens to be an open problem whether the sum of three cubes can ever
equal 42.  So now let us perform a thought experiment.  Imagine that a
mathematical genius---let's call her Kate Goddard---proves the following
two theorems.

Theorem 1 (Goddard).  The sum of three cubes never equals 42.
Theorem 2 (Goddard).  If PA is consistent, then PA does not prove S.

For all we know, this could happen.  If it does happen, then it means that
there is a nonstandard model of PA in which there exist nonstandard
integers x, y, and z whose cubes sum to 42.  We now clearly see that S "is
about both standard and nonstandard natural numbers" (I've copied the text
in quotation marks from one of your messages).  Since S is about both
standard and nonstandard natural numbers, whereas "the sum of three cubes
is never equal to 42" is supposed to be a statement about standard
naturals, S does not satisfactorily formalize "the sum of three cubes is
never equal to 42."

My conclusion is that the argument in the above paragraph is bogus.  The
fact that S might be true in the standard model and false in a nonstandard
model *has no bearing on* the question of whether S is a satisfactory
formalization of "the sum of three cubes can never equal 42."  If Goddard
were to prove the above two theorems, I would conclude that *there is no
finitary proof that the sum of three cubes is never 42*.  I would *not*
conclude that S is an unsatisfactory formalization.

For the same reason, I conclude that your argument that Con(PA) does not
satisfactorily formalize "PA is consistent" is bogus.

At the same time, of course, I agree that Con(PA) does not mean that PA is
consistent, for the simple reason that Con(PA) is a formal string and
doesn't mean anything.  It can be interpreted in different models, but
that fact has no bearing on whether it satisfactorily formalizes the
consistency of PA.

Tim
```