[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.
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=
More information about the FOM
mailing list