[FOM] Forward: Provability of Consistency

[Richard Kimberly Heck]

On 3/26/19 8:48 PM, Artemov, Sergei wrote:
> Dear Riki, 
>
> Thank you for your interest and meaningful questions. Here are the answers.
>
> RH1. >> 3. Provability in PA. This one is quite relevant in the context of Goedel’s Second Incompleteness Theorem, G2. 
>>> However, our goal is to make a semantic sense out of (3), to understand what is really going on in G2. 
>> I do not understand this, and I strongly suspect that it is confused.
>> What does "understanding" Con(PA) mean if it does not mean understanding
>> it as standardly interpreted?
> Con(PA) is the first-order formula \forall x(~Proof(x,0=1)) in the language of PA. Its interpretation (and truth values) depend on a specific model of arithmetic we are considering. There is one standard model and infinitely many nonstandard models of PA. Con(PA) is interpreted and gets a definitive truth value in each of these models. In the standard model, the truth value of Con(PA) is “true.” However, when we study the question of whether a given formula F is derivable in PA, PA|-F(?), we may wish to consider this provability condition in an equivalent semantic form as “F is true in all models of PA,” for example, in order to compare this with the interpretation of F in the standard model. Having said this, take F to be Con(PA), Hence
>
> PA|- Con(PA)    iff    Con(PA) holds in each model of PA. 
>
> Since, by G2, PA|-/- Con(PA), there is a model M (of PA) in which Con(PA) is false i.e., there is an element \alpha in M such that Proof(\alpha,0=1) is true in M. Furthermore, as you mention in your post, for each specific n, PA|- ~Proof(n,0=1), hence Proof(n,0=1) is false in model M for each n=0,1,2,… . Therefore, \alpha is different from each of n=0,1,2,…, hence \alpha is a nonstandard number in M. We have thus proved a small lemma that Proof(x,0=1) can be false only for nonstandard x’s. 

I'm not sure I needed you to explain elementary logic to me, but thanks
anyway.

What I am objecting to is the claim that the//*meaning* of the formal
string abbreviated here as Con(PA) depends upon anything to do with
non-standard models. I.e., to put it in your terms: Whether Con(PA) is
an 'adequate representation' of the informal statement that PA is
consistent *has nothing to do* with non-standard models. Whether Con(PA)
is provable in PA has (in the sense you explain) to do with what happens
in non-standard models (by the completeness theorem). But that is a
wholly different matter. Whether Con(PA) is an adequate formalization of
the informal statement turns only on what the interpretation of Con(PA)
is over the standard model. Con(PA) is true, in the standard model, iff
PA is consistent, in exactly the same sense in which (say) the obvious
formalization of Goldbach is true in the standard model iff every even
number greater than 2 is the sum of two lesser primes. That is why the
obvious formalization of Goldbach is 'adequate', and it is also why the
usual formalization of Con(PA) is 'adequate'.

To put it somewhat differently: I think the question whether Con(PA) is
an adequate representation of the informal statement is one we could
have answered before Gödel proved the completeness theorem, and that
that question would have had the same answer even if the completeness
theorem failed. I don't think that fact that provability is equivalent
to truth in all models is at all relevant to that question.

I could go on at greater length, but what I'd say would just parrot what
George Boolos has to say about this matter in /The Logic of
Provability/, pp. 32-5.

The problem in your argument arises here:

> ...[W]hen we study the question of whether a given formula F is derivable in PA, PA|-F(?), we may wish to consider this provability condition in an equivalent semantic form as “F is true in all models of PA,” for example, in order to compare this with the interpretation of F in the standard model.
You can, if you like, think about what F *would mean* if it were
interpreted with respect to a non-standard model. And certainly, if
Con(PA) is so interpreted, then it is not an 'adequate representation'
of the informal statement. But the fact that Con(PA) can be so
interpreted simply does not show that, as it is *actually* interpreted
(with respect to the standard model), it is not an 'adequate
representation' of the informal statement. The fact that whether the
formal string Con(PA) is provable in PA is equivalent to the question
whether that same formal string is true in all models of PA is simply
irrelevant.


> RH2. > Does that also show that PH is not really about the natural numbers, 
> as its understood within the context of PA?
> “About natural numbers” is not mathematical statement. 

Let me rephrase, then: Do you or do you not think that the formal
statement PH is an 'adequate representation' of the informal statement
of the Paris-Harrington theorem? If not, then I myself think that
completes a reductio of your view. If so, however, then how is this case
different from that of Con(PA)? You argue that Con(PA) is not a proper
formalization of "PA is consistent" on the ground that, in non-standard
models, it can be false, etc. But PH is false in some models of PA, too,
even though it is true.

The only difference I can see here is that Con(PA) does, whereas PH does
not, 'talk about' (or purport to talk about) provability in PA itself.
But the 'problem' you are raising has to do with the unbounded universal
quantifier in Con(PA)---or in the provability 'predicate' Bew(x)---not
with anything in the provability *relation* Bew(x,y). So the fact that
Con(PA) happens to contain Bew(x,y) once again looks to be irrelevant.
If so, however, then it's hard to see what the difference is, from your
point of view, between Con(PA) and any other true but unprovable \Pi_1
formula.

Let me note explicitly that, for all I know, there's a great deal of
*formal* interest to the results proven in this paper. I'm arguing that
they lack *philosophical* interest of the sort you claim for them.

Riki


-- 
----------------------------
Richard Kimberly (Riki) Heck
Professor of Philosophy
Brown University

Pronouns: they/them/their

Email:           rikiheck at brown.edu
Website:         http://rkheck.frege.org/
Blog:            http://rikiheck.blogspot.com/
Amazon:          http://amazon.com/author/richardgheckjr
Google Scholar:  https://scholar.google.com/citations?user=QUKBG6EAAAAJ
ORCID:           http://orcid.org/0000-0002-2961-2663
Research Gate:   https://www.researchgate.net/profile/Richard_Heck


-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190328/4693a792/attachment-0001.html>