[FOM] 809: Goedel's Second Reworked/1

[Richard Kimberly Heck]

On 05/20/2018 03:47 PM, Harvey Friedman wrote:
> This post concerns the NEWLY SIMPLIFIED PROOF OF GSIT.
>
> ...
>
> STRUCTURAL FACT. 1. There is an r.e. set A such that every r.e. set B
> somewhere agrees with A. (I.e., there exists n such that n in A iff n
> in B.)
> 2. There is an r.e. set A such that every r.e. set B somewhere low
> level provably agrees with A. (I.e., there exists n such that a very
> weak system of arithmetic (fixed in advance, like EFA or much weaker)
> proves n* in A iff n* in B.)
>
> ...
>
> PROOF OF GSIT. Fix an r.e. theory T containing a very weak system of
> arithmetic, which proves Con(T). We will show that T is inconsistent.
>
> Let A be from the Structural Fact. Apply the Structural Fact (sharp
> form) to B = [n: T refutes n in A}. Fix n such that
>
> n* in A iff n* in B
>
> is low level provable. In particular
>
> T proves (n* in A iff n* in B)
>
> I.e.,
>
> 1) T proves (n* in A and n* in B) or (n* notin A and n* notin B)
>
> Now T refutes the first disjunct in the formula in 1). To see this, we
> argue in T (which proves Con(T)) as follows.
>
> Assume n* in A and n* in B
> T proves n* in A
> T proves n* notin A
> T is inconsistent
> T is consistent
> contradiction
>
> Hence T proves the second disjunct in the formula in 1). In
> particular, T proves n* notin A, and so n* in B and T proves n* in B.
> But T proves n* notin B, and so T is inconsistent. QED

One interesting question to ask here, it seems to me, is to what kinds
of theories this result naturally applies. The Löb-ish version requires
that T prove the derivability conditions, and of course the natural
theory in which to do that is I\Sigma_1, though we know from Paris and
Wilkie that this can be pushed down to I\Delta_0 + \omega_1. Anyway, it
seems to be a natural question to what extent Harvey's proof depends
upon the assumption that T proves the derivability conditions.

I'm not totally sure I see how to interpret Harvey's proof in these
terms. The inference, which we are supposed to be making in T, from n* ∈
A, which is an *assumption*, to T ⊢ n* ∈ A seems like it might require
that T prove
    n* ∈ A → Bew(n* ∈ A)
which is precisely where provable \Sigma_1 completeness gets used in the
Löb-ish proof. It is clear that Harvey's proof requires that T is
\Sigma_1 complete. So, if I'm right, then this proof requires the first
and third derivability conditions; and the second is often pretty
trivial, with the third being the hard one. So, in a way, I'm not really
sure how much of an improvement this is, from this point of view. We
still seem to need to do all the messy stuff to prove the third
derivability condition, which raises all the usual questions about
coding and intensionality.

I understand that the motivation here seems to be to avoid
diagonalization, so maybe I'm worrying about something else. But the
usual proof of G2 involves formalizing the proof of G1, and *that* is
where the appeal to diagonalization is; in a way, diagonalization does
not really figure in the proof of G2 itself.

So let me ask: Is there a way of taking a non-diagonalizing proof of G1
and showing how to prove G2 by formalizing it? What resources would that
require, if so? A number of such proofs of are discussed in Chapter 17
of Boolos, Burgess, and Jeffrey, for example. E.g., it can be shown from
the assumption that there is an r.e. set that is not recursive that
every axiomatizable consistent extension of Q fails to prove some true
\Pi_1 sentence (a slightly weaker version of G1). Is there some form of
G2 that can be proven by showing how that can be formalized?

Riki


-- 
-----------------------
Richard Kimberly Heck
Professor of Philosophy
Brown University

Pronouns: they/them/their

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