[FOM] Forward: Provability of Consistency (Artemov, Sergei)

[Timothy Y. Chow]

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