[FOM] Provability of Consistency

[Artemov, Sergei]

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.

Tim
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
https://urldefense.proofpoint.com/v2/url?u=https-3A__cs.nyu.edu_mailman_listinfo_fom&d=DwICAg&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=DaVq92tS8iAoUQjKHt9C4XdoL3d05Dw7WTEtjUYZ-_s&s=LylkM7ygyRiXXSK9p7Ign5z3mfazhR_-bMdBlnAvFM4&e=