[FOM] Notes on "Artemov Consistency"

[Richard Kimberly Heck]

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
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/20190409/e9aecab4/attachment-0001.html>