[FOM] Forward: Provability of Consistency (Artemov, Sergei)
Timothy Y. Chow
tchow at math.princeton.edu
Mon Mar 25 23:18:24 EDT 2019
Sergei Artemov wrote:
> The proof of G2 states that Con(PA) is not derivable in PA which,
> semantically, is equivalent to existing of a model M of PA in which
> Con(PA) fails. So, there is an element \alpha in M for which
> Proof(\alpha, 0=1) is true. It is easy to observe that \alpha cannot be
> from the standard initial segment (there are many ways to show that
> ~Proof(n,0=1) for any standard n, pick the one you like). The
> conclusion: Con(PA) indeed fails in some models of PA (hence is not
> PA-provable), but ONLY on nonstandard elements which do not correspond
> to real derivations in PA. This sketch of the semantic analysis of G2
> shows that G2 is not about real PA-derivations, each of which is in fact
> not a proof of 0=1.
>
> The traditional connection of G2 to consistency of real PA-proofs is
> actually a sophisticated logical error. Here is a simple example to
> explain this logical error to a mathematician. Suppose you want to check
> whether the following (true) statement is formally provable: R = ?no x
> is a real root of x^2+1.? We pick a rich relevant theory of complex
> numbers C and note that R is not provable in C by the following
> reasoning: take an evaluation x=i and get x^2+1=0. Conclusion: R is true
> but not provable. A simple mistake here was to accept a fake witness for
> x^2+1=0, which is not a real number. The same reasoning error occurs in
> interpreting G2 as an impossibility of real PA-proofs of consistency: we
> tacitly accept a fake witness \alpha for Proof(x,0=1), the one which
> does not correspond to a real PA-derivation. I repeat, there is nothing
> wrong with G2, but its ?impossibility? reading for real PA-derivations
> is plain erroneous.
I don't feel like responding to everything you've written in your long
post, but I will try to respond to this part, which is the part that I
feel makes the least sense.
I don't understand what you mean when you say, "G2 is not about real
PA-derivations." In particular, I don't understand what you mean by the
word "about." G2 says that if PA is consistent, then Con(PA) is not
derivable in PA. Note that I am carefully distinguishing between "PA is
consistent" and "Con(PA)". This distinction is necessary in order to
state G2. In the actual statement of G2, the string Con(PA) is purely a
syntactic string. I don't know what you're trying to say with your
allusion to cargo cults, but the assertion I just made, that in the
statement of G2, Con(PA) is just a string that does not have to be
assigned a meaning, is about as uncontroversial a statement as one gets in
this subject. Furthermore, in the clause "Con(PA) is not derivable in
PA," the word "derivable" refers to real PA-derivations. By any normal
standards of English usage, G2 is therefore "about" real PA-derivations.
Given the way this discussion has been going, I hesistate to put words in
your mouth, but since I'm not understanding the words that are actually
coming out of your (figurative) mouth, I have no choice---I think what
you're trying to say is that G2 is *not about the unprovability of the
consistency of PA*. If that is what you're trying to say, then I'm fine
with that. I say that G2 is about real PA-derivations, and it is about
the unprovability of Con(PA), but it is *not* about the unprovability of
the consistency of PA. To draw conclusions about the unprovability of the
consistency of PA, one has to bring in other assumptions, such as the
statement (*) from my previous message. Note that to conclude that G2 is
not about the unprovability of the consistency of PA, there is no need for
any fancy observations about nonstandard models and such. All one has to
do is look at G2 and see that it's a statement about the unprovability of
Con(PA) and not about the unprovability of the consistency of PA.
If you agree with me this far, then the other thing I would say is that I
don't see that nonstandard models have any bearing on whether Con(PA)
adequately represents the consistency of PA (for the purposes of drawing
philosophical conclusions about the unprovability of consistency). Let's
take a simpler formal string S as an example:
S := "NOT exists x exists y exists z : x*x*x + y*y*y + z*z*z = 42"
(Here x and y and z are supposed to range over integers, not just
nonnegative integers.) It happens to be an unsolved problem whether the
sum of three cubes can ever equal 42. We can now raise the question: Is
the above string S an adequate representation of the statement that the
sum of three cubes can never equal 42, in the sense that we believe that
any finitistic proof that the sum of three cubes can never equal 42 can be
mimicked by a formal PA-proof of S?
One could attempt to argue that the answer is no, for the following
reason: For all we know, S might be true when interpreted in the standard
model, but unprovable in PA. In that case, there would some nonstandard
model in which not-S holds---i.e., there would be three *nonstandard*
integers whose cubes sum to 42. S therefore "states the unsolvability of
the equation in both standard and nonstandard integers." (I don't think
that this last clause I wrote, in quotation marks, makes any sense, but
I'm trying to imitate the way you've phrased things.) Hence S is not an
adequate representation of the statement that the sum of three cubes can
never equal 42, which is after all a statement about standard integers
only.
Obviously, you can concoct an argument like this for any arithmetic
statement of this general form. For that reason I don't find it to be a
convincing argument for the inadequacy of S. If we accept this kind of
argument then virtually no formal string can adequately represent
number-theoretic statements of interest ("adequately" meaning for the
purposes of investigating provability issues). I'm just not prepared to
be that skeptical.
Tim
More information about the FOM
mailing list