[FOM] Provability of Consistency

Artemov, Sergei SArtemov at gc.cuny.edu
Thu Mar 28 23:34:42 EDT 2019

Indeed, I did not have time to comment on all your remarks; there were many. But you did not comment on my x^2+1 example either, and if you would, there would be no need for you to reiterate the current question since it is conceptually covered by the x^2+1 example.

Let me parse your “three cubes” example. 

< Do you consider S to be a satisfactory formalization of the statement, "the sum of three cubes is never equal to 42"? >

Of course NOT, since in its syntactic form, S allows x,y,z to be positive integers, rationals, reals, etc. And this is not a forgotten default, but a principal game-changing feature. A better formulation would be S* which is S with additional condition “x,y,z are integers” (there is also a default that x,y,z are standard integers). 

At this very point you are losing your syntactic paradise. Insisting that S “as is” is the proper syntactic formulation of the three cubes problem would be unprofessional since without specifying the domain of x,y,z, S is a plain wrong formulation.  Or you say “sorry, of course I meant S for (standard) integers x,y,z.” And then the real life storms into your syntactic paradise because you have to invoke infinite sets, evaluations, Tarsi’s definition of truth in a model, etc. which makes S* not a syntactic condition any more.  

In real life, people are usually loose and trend to omit the domain condition. However it is always present. So, 

a) S is a WRONG formulation of the three cubes problem, since the domain condition for x,y,z is missing. In particular, quantifiers in S are allowed to range over different domains: integers, nonstandard integers, rationals, reals, etc.

b) S* (with some other defaults) is the right formulation, but it is not purely syntactic.  

In principle, we could stop here since your question of whether a purely syntactic S is a correct formulation of the three cubes problem is answered negatively. 

Let us see what happens with your examples. As you suggest, imagine

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

No problem with understanding Th.1, this is a genuine solution of the problem, sincere congratulations to Kate.

Th.2 is not directly related to the three cubes problem since it claims unprovability of S which is a sloppy formulation of the three cubes problem (cf. the above). Hypothetically, the better version of Th.2 would be Th.3 “If PA is consistent, then PA does not prove S*,” but I am afraid that even Kate Goddard’s genus could not do it since S* is not in the language of PA due to the built-in notion of a standard integer. 

Th.2 alone would be a logician delight, as proving independence of a formula which is the three cubes problem without the domain condition. However, its mathematical significance would be limited. Imagine Kate proved only Th.2 and counterexamples to S are all nonstandard integers; would this bring us closer to a solution of the three cubes problem? Not really. Here is my example: in some models of infinite computations, the Halting Problem gets a solution at some infinite steps. Does this alter the classical result that the Halting Problem is undecidable? Definitely not. This shows the real value of Th.2. 

From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] on behalf of Timothy Y. Chow [tchow at math.princeton.edu]
Sent: Wednesday, March 27, 2019 9:58 PM
To: fom at cs.nyu.edu
Subject: Re: [FOM] Provability of Consistency

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.

FOM mailing list
FOM at cs.nyu.edu

More information about the FOM mailing list