[FOM] Notes on "Artemov Consistency"

Wed Apr 10 11:55:43 EDT 2019

A brief correction, not a separate posting. I hope the esteemed moderator posts it. 

> T is "Artemov consistent" iff ∀n[Bew_T("~Pf(n,0=1)")]

Sadly, this is a misunderstanding, hence the whole analysis of this notion, though correct, is misplaced. 

What is here called "Artemov consistency” was used in my PoC paper as a technical notion which was compared NEGATIVELY with the real consistency proposal, cf. Section 4.2 “Provability of CConPA in PA is not an answer either” (and many other comments throughout the paper). My real proposal was formulated for T=PA and it is different from ”Artemov consistency”, cf. section 5.  

A real professional discussion on my real consistency proposal is actively going on through personal communications. I am working on the new version of PoC paper in which this and some other misconceptions will be specifically addressed. 

I am truly grateful for your interest.

Sergei 
________________________________________
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: Tuesday, April 9, 2019 1:18 PM
To: Foundations of Mathematics
Subject: [FOM] Notes on "Artemov Consistency"

FOMers,

I've been thinking further about the discussion sparked by Sergei Artemov and have come to the conclusion that I may have misinterpreted him. There is, it seems to me, a natural proposal in the vicinity that is immune to at least some of the objections I offered. But there are further results in this area that also seem to me to call the interest of this proposal into doubt.

Let T be some recursively axiomatized theory. Let Pf_T(x,y) be a 'reasonable' formula representing that x is a T-proof of y, and let Bew_T(y) be ∃x[Pf_T(x,y)]. Then:

T is "Gödel consistent" iff ∀n[~Pf(n,0=1)]

T is "Artemov consistent" iff ∀n[Bew_T("~Pf(n,0=1)")]

I.e., T is Gödel consistent if there is no proof of 0=1; T is Artemov consistent if T proves, for each n, that n is not a proof of 0=1.

I take Artemov's first point to be that some theory might *prove* that T is Artemov consistent without proving that it is Gödel consistent. And, indeed, as Artemov shows, PA proves that it is Artemov consistent, even though it does not prove that it is Gödel consistent.

One objection that I and others made had the following form. Consider, say, the ternary Goldbach conjecture: Every odd number >5 is the sum of three primes. (Thanks to Tim Chow for the example.) This has apparently now been proved. Hence, we know that PA (and even Q) proves all instances of this conjecture, since it is Π_1. But we do NOT have any reason to believe that PA proves:

    ∀n>5∃xyz<n[Bew_PA("Prime(x) & Prime(y) & Prime(z) & x + y + z = n")]

I.e., the truth of ternary Goldbach does not assure us that PA *proves that* it proves all the instances. This is a genuine difference.

However, Artemov consistency is a very weak notion. It is, indeed, comparable to Rosser consistency. Recall that, in his strengthening of the first incompleteness theorem, Rosser used a gerry-mandered notion of 'provability' to weaken the requirement of omega consistency to simple consistency. That notion may be taken to be:

    RPf_T(p,s) iff Pf_T(p,s) & ∀x<p[~Pf_T(x,neg(s))]

i.e.: p is a Rosser proof of s iff p is a proof of s and no 'prior' proof is a proof of s's negation. Now we can define:

T is Rosser consistent iff ~∃p[RPf_T(p,0=1)]

It turns out that many theories can prove their own Rosser consistency, even though they cannot prove their own Gödel consistency. But this notion is too weak to be useful: For any consistent theory T, we already have that Robinson's Q proves that T is Rosser consistent. In fact, Q proves the Rosser consistency of many *inconsistent* theories. We just need the first T-proof of 0≠1 to precede the first T-proof of 0=1.

Similarly, it can be shown that IΣ_1 proves the Artemov consistency of *every* theory that contains Q, whether or not that theory is consistent. For example, IΣ_1 proves the Artemov consistency of PA + 0=1.

Here is the argument. Reason in IΣ_1. Suppose T contains Q. We want to show that, for any n:

(*)    Bew_T("~Pf_T(n, 0=1)")

So let n be arbitrary. Now either T is Gödel consistent or it is not. If it is not, then certainly (*). If it is, then ~Pf_T(n,0=1), since T is Gödel consistent. But then by provable Σ_1 completeness (for Q, but T contains Q), we have (*). Note that we need provable Σ_1 completeness as a generalization here:

    ∀x[Tr_{Σ_1}(x) → Bew_Q(x)]

and not, as one sometimes sees it, just as a schema. But that's provable in IΣ_1. So the full argument is: Since ~Pf_T(n,0=1), also Tr_{Σ_1}("~Pf_T(n,0=1)"), so Bew_Q("~Pf_T(n, 0=1)"), so (*), since T contains Q.

With sufficiently careful formulation (I'm assured), this argument can be carried out in EFA and (for sufficiently 'simple' theories T) even in Buss's system S^1_2. With careful attention to where excluded middle is applied, the argument can be carried out in intuitionistic versions of those systems. The change is just to consider, at the outset, whether Pf_T(n,0=1) and run the argument on the two cases of that claim. That's decidable, so the application of excluded middle is constructively acceptable.

Along these same lines, it is worth noting also that PA proves, in a similar sense, that it proves its own reflexivity ("verifiable reflexivity") although it does not prove its own reflexivity. I.e., PA proves:

    ∀n[Bew_PA("Con(IΣ_n)")]

although it does not (unless it is inconsistent) prove:

    ∀n[Con(IΣ_n)]

This argument too (I am assured) can be carried out in EFA.

Riki

NOTE: Thanks to Albert Visser for helping me sort through all this. Most of the technical facts that I've mentioned I learned from him. Responsibility for the formulations is of course my own.

--
----------------------------
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=DwMDaQ&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=T4AXZuTffLA9NgoaOdBKAU7lCn0ryVx36mASgpCxSPI&s=jTH90sqoUhpf40cLc_mWawR3rOUoQaUzkYORsY9fR04&e=>
Blog:            http://rikiheck.blogspot.com/ [rikiheck.blogspot.com]<https://urldefense.proofpoint.com/v2/url?u=http-3A__rikiheck.blogspot.com_&d=DwMDaQ&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=T4AXZuTffLA9NgoaOdBKAU7lCn0ryVx36mASgpCxSPI&s=2unkZpT5gJIxkGp44ncZ3WuK-r2K7DG_iFytlF33s30&e=>
Amazon:          http://amazon.com/author/richardgheckjr [amazon.com]<https://urldefense.proofpoint.com/v2/url?u=http-3A__amazon.com_author_richardgheckjr&d=DwMDaQ&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=T4AXZuTffLA9NgoaOdBKAU7lCn0ryVx36mASgpCxSPI&s=U4698ymQkEYmYgqZ86bNcXH3ZE6ategoMh1PUg9-ikg&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=DwMDaQ&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=T4AXZuTffLA9NgoaOdBKAU7lCn0ryVx36mASgpCxSPI&s=GCUFqIXIZfTefJ8C9trZQvXX4DRlZ-yvIP8ULWkryFU&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=DwMDaQ&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=T4AXZuTffLA9NgoaOdBKAU7lCn0ryVx36mASgpCxSPI&s=P3OrAT-WNkX05NVn1duFgjjvtT-vonrTal9ersyxblQ&e=>