[FOM] Forward: Provability of Consistency

Tue Mar 26 20:48:21 EDT 2019

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. This is a semantical analysis of (3) which I mean. Cf. the PoC paper and my previous posting to Tim Chow in which I analyze with an algebraic example why this means that Con(PA) misrepresents Hilbert’s consistency definition “no PA-derivation S contains a contradiction.”

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. Mathematically, PH is true in the standard model in which all quantifiers range over standard numbers. So, in the standard model, PH is “about (standard) natural numbers.” However, in the context of provability PH in PA we have to consider nonstandard models of PA as well: there is a nonstandard model M in which PH is false. The same reasoning as in RH1 shows that nonstandard elements of M are essential for determining the truth value of PH in M. One can say that in M, PH is about both standard and nonstandard natural numbers, not just “about natural numbers.”

RH3. > One of the difficulties that I (and perhaps some others)
> have is that every instance of
>
> (*)    If S is a PA-derivation, then S is not a proof of 0=1.
>
> is already provable in R. (These are \Delta_1, and they are all true.)
> But the proof that *all* the instances of (*) are provable in R will
> involve resources that go beyond PA. What you are adding, I take it, is
> a proof that PA-proofs of instances of (*) can be made to be uniform in S. 

Not really. Every instance of (*) is provable in PA, but the traditional proof of this fact which you have just presented relies on the soundness of PA w.r.t. the standard model and this is not a finitary argument required by Hilbert. I am making sure that for every instance of (*) there is a  mathematical proof of this instance and this proof is formalizable in PA. Please check out section 4 and 5 on the PoC paper. Uniformity is not the point. 

Best, 
Sergei

________________________________________
From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] on behalf of Richard Heck [richard_heck at brown.edu]
Sent: Monday, March 25, 2019 10:40 PM
To: Foundations of Mathematics
Subject: Re: [FOM] Forward: Provability of Consistency

Let me ask a few naive questions that (I hope) might help to clarify
what is going on here.

On 3/25/19 9:27 AM, Artemov, Sergei wrote:
> ...a formal string, e.g., Con(PA), has exact semantics, which we should know and take into account. There are at least three relevant levels of understanding of an arithmetical formula F:
>
> 1. “Naive” mathematical reading F as a mathematical statement about natural numbers.
>
> 2. Semantics in the standard model of arithmetic. This is actually a glorified version of (1) for logicians.
>
> 3. Provability in PA. This one is quite relevant in the context of Goedel’s Second Incompleteness Theorem, G2.
>
> Con(PA) is an adequate formalization of consistency of PA in the standard model (2), and, perhaps, that is why “general” mathematicians have been willing to accept Con(PA) as in (1). No problems here.
>
> 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? (I take it that the issue of Gödel
numbering is agreed to be irrelevant. We can reformulate all of this in
terms of a theory of expressions, a la Grzegorczyk.) Is your view that
Con(PA) means different things depending upon what theory of the natural
numbers I accept? E.g., it means something different for Nelson or
Hilbert or Feferman or Shapiro? If not, what precisely is the project
you describe at (3)?

> By Goedel’s Completeness Theorem, a formula F is derivable in PA iff F holds in all PA-models, most of them nonstandard. ...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.

Similarly, the statement of the Paris-Harrington theorem (PH) is
provable in PA iff PH holds in all models of PA, which it does not, even
though it does hold in the standard model. Does that also show that PH
is not really about the natural numbers, as its understood within the
context of PA?

Let me ask if you would accept the following reformulation of what you
are claiming. One of the difficulties that I (and perhaps some others)
have is that every instance of

(*)    If S is a PA-derivation, then S is not a proof of 0=1.

is already provable in R. (These are \Delta_1, and they are all true.)
But the proof that *all* the instances of (*) are provable in R will
involve resources that go beyond PA. What you are adding, I take it, is
a proof that PA-proofs of instances of (*) can be made to be uniform in
S. (It's a nice question whether that can be extended to weaker
systems.) But it's still obscure to me why uniformity should matter as
much as you seem to insist it does.

Another question: Is your view that PH could be shown to be provable "in
PA" by showing that its instances can be proven uniformly in n?Maybe
that is your view, and you think that PH could be shown to be provable
in PA by showing that its instances can be proven uniformly. If so, then
that'd be an interesting claim, but not one that has much to do with
Con(PA) specifically.

Riki

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

Pronouns: they/them/their

Email:           rikiheck at brown.edu
Website:         https://urldefense.proofpoint.com/v2/url?u=http-3A__rkheck.frege.org_&d=DwIF-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=QbQy3GplJ55mI5mse0AzJ3SH2CxaIXVk-l9KgZmi7kE&s=7vsG-8nn71nmoxJmeCqh9q69rBjfAiHROnnRJQQZ8rQ&e=
Blog:            https://urldefense.proofpoint.com/v2/url?u=http-3A__rikiheck.blogspot.com_&d=DwIF-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=QbQy3GplJ55mI5mse0AzJ3SH2CxaIXVk-l9KgZmi7kE&s=l5uGymakV7XRSi_DS4fJKC3laENLdBdCxZDsKHKd5mY&e=
Amazon:          https://urldefense.proofpoint.com/v2/url?u=http-3A__amazon.com_author_richardgheckjr&d=DwIF-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=QbQy3GplJ55mI5mse0AzJ3SH2CxaIXVk-l9KgZmi7kE&s=4DLMqDj5uB1l5M899l3C_nKiDE_NcnayJhk7vcF8GKQ&e=
Google Scholar:  https://scholar.google.com/citations?user=QUKBG6EAAAAJ
ORCID:           https://urldefense.proofpoint.com/v2/url?u=http-3A__orcid.org_0000-2D0002-2D2961-2D2663&d=DwIF-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=QbQy3GplJ55mI5mse0AzJ3SH2CxaIXVk-l9KgZmi7kE&s=6XO0Uui04r3fucheAALAiOMY-cmRXiiqzWL0g4XQ8AA&e=
Research Gate:   https://urldefense.proofpoint.com/v2/url?u=https-3A__www.researchgate.net_profile_Richard-5FHeck&d=DwIF-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=QbQy3GplJ55mI5mse0AzJ3SH2CxaIXVk-l9KgZmi7kE&s=19VrLwA-k8AXoYPn0VJTN-YID6JwkIjz2gW1lcNm9zQ&e=

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
https://urldefense.proofpoint.com/v2/url?u=https-3A__cs.nyu.edu_mailman_listinfo_fom&d=DwIF-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=QbQy3GplJ55mI5mse0AzJ3SH2CxaIXVk-l9KgZmi7kE&s=czGU3S_II0j0z1qRGemxmmDzjHV_cKq4SBtuPqnh7wU&e=