[FOM] Provability of Consistency

[Timothy Y. Chow]

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.

Tim