[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
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