[FOM] Forward: Provability of Consistency

Fri Mar 29 00:26:39 EDT 2019

RK: < 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’.>

If your default is the standard model, then both Goldbach in its usual formulation and Con(PA) are `adequate.’ Then the solution would sound: Goldbach conjecture holds (in the standard model, as a default). 

When speaking about provability rather then truth, the standard model is no longer a default and, to keep the formulation `adequate,’ one has to add the domain condition `for (standard) natural numbers.’ We are excused from this bureaucracy in the case of Goldbach since we are interested in its solution in the standard model. The domain condition can be sometimes omitted in loose formulations, but it is present, don’t make a mistake. 

For consistency, the situation is different since the answer for the standard model is known, and we are interested only in provability. Here the domain condition is absolutely necessary: the adequate Hilbertian formulation of consistency would be 

(#) “for all standard natural numbers x, ~Proof(x,0=1).” 

There are no any indications that Hilbert was interested about nonstandard proof codes. 

(#) is equivalent to the ‘usual’ formalization Con(PA) in the standard model, but not “in general.” In G2, Con(PA) is the consistency-loose, without domain condition which is, of course, stronger than consistency with the proper domain condition. So, the fact that PA|-/- Con(PA) only states that without the domain condition, consistency is not provable and the unprovability occurs exactly when the domain condition is violated. This theorem is of interest for logicians, but is not as an answer to Hilbert’s question about consistency with the domain condition. 

The same holds for PH. It is true in the standard model, i.e. with the domain condition. If we consider PH-loose which is PH without the domain condition, then PA|-/- PH-loose. This is an impressive result in logic, which does not alter the validity of PH with the domain condition. 

Here is my example: in some models of infinite computations, the Halting Problem HP gets a solution at some infinite steps. Does this alter the classical result that the HP is undecidable? Definitely not. So, the “solution” of HP at infinite steps is mostly a curiosity. 

G2, perhaps because the role of nonstandard models was not properly revealed, has projected a more serious image of having to do with the real consistency problem. But at the end of the day, this is the same type of curiosity about what happens if you allow proofs to be infinite. Well, then you can prove 0=1. So what? 

________________________________________
From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] on behalf of Richard Kimberly Heck [richard_heck at brown.edu]
Sent: Thursday, March 28, 2019 1:37 PM
To: Foundations of Mathematics
Subject: Re: [FOM] Forward: Provability of Consistency

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<mailto:rikiheck at brown.edu>
Website:         http://rkheck.frege.org/ [rkheck.frege.org]<https://urldefense.proofpoint.com/v2/url?u=http-3A__rkheck.frege.org_&d=DwMD-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=dR7WTqvNOse_KXpq6s7Ni-sDotaViCPcE_Q69PH1BiQ&s=gUJ0dGuPGFOzM92wiZJKYZOSV1cZplBZnPmu-PU5BW4&e=>
Blog:            http://rikiheck.blogspot.com/ [rikiheck.blogspot.com]<https://urldefense.proofpoint.com/v2/url?u=http-3A__rikiheck.blogspot.com_&d=DwMD-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=dR7WTqvNOse_KXpq6s7Ni-sDotaViCPcE_Q69PH1BiQ&s=CMNO_ooH9tpk-QzleFQx2_nJGCINAboz17XEG4mLG58&e=>
Amazon:          http://amazon.com/author/richardgheckjr [amazon.com]<https://urldefense.proofpoint.com/v2/url?u=http-3A__amazon.com_author_richardgheckjr&d=DwMD-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=dR7WTqvNOse_KXpq6s7Ni-sDotaViCPcE_Q69PH1BiQ&s=KM1yHeeKpChHAXf7VkiqeMBjLw_Vk2U46A-oeoF-IXU&e=>
Google Scholar:  https://scholar.google.com/citations?user=QUKBG6EAAAAJ
ORCID:           http://orcid.org/0000-0002-2961-2663 [orcid.org]<https://urldefense.proofpoint.com/v2/url?u=http-3A__orcid.org_0000-2D0002-2D2961-2D2663&d=DwMD-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=dR7WTqvNOse_KXpq6s7Ni-sDotaViCPcE_Q69PH1BiQ&s=hmlDt3VRP4qVCUCbFgZDgfHGZad5lrdbVoVzXCm4qtw&e=>
Research Gate:   https://www.researchgate.net/profile/Richard_Heck [researchgate.net]<https://urldefense.proofpoint.com/v2/url?u=https-3A__www.researchgate.net_profile_Richard-5FHeck&d=DwMD-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=dR7WTqvNOse_KXpq6s7Ni-sDotaViCPcE_Q69PH1BiQ&s=brrZtC67W5neTvl8FP1-LaDeLz9Ye-bWWffU7QYK_ec&e=>