[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 
> follow suit.

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 
adequate formalization, then it should remain an adequate formalization in 
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.


More information about the FOM mailing list