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

[Harvey Friedman]

Thanks to Richard Heck for this reply if 5/20/18.

I was hoping that it would be left to others to work out such detailed
fine points, and it looks like Richard has got the ball rolling.

I offer this proof at the semiformal level - the level at which big
intellectual advances really take place - which is all anyone cares
about except for weird nerdy specialists like you and me. E.g., for
non advanced courses, for general philosophers, for mathematicians who
don't want logic details, for mathematical logicians who don't like
proof theory - and for that elusive but crucial group known as
"general intellectuals".

So I'm offering this up, in the above sense, as an apparent major
improvement - e.g., over G1/G2 you allude to, and so forth.

PROOF: Well, have people actually teach - or explain it to
professional colleagues (maybe in logic related areas) - in this way.
Including not giving the proof of the clearly stated separated
structural elementary recursion theory, which is of clear independent
interest. In fact, we may find that the number of teachers interested
in teaching it (even in courses broader than math logic) is
substantially increased. (Another big advantage of this for some
audiences over G1/G2 is how mathematically clean the structural
recursion theory is - and how it is of clear independent interest).

Incidentally, I still find GSIT completely mysterious, and I do not
believe that we have the "right" proof of it, and something
fundamental and unexpected will come out of the right proof. I think
what I did here is a step in the right direction, but there is
something deeper going on and I can at least assure you that you will
hear about it if and when I figure it out.

LITTLE SPINOFF SUBJECT? Given a natural family of mathematical
objects, ask whether there is one that agrees with all others
somewhere, or even substantially. Important examples of where this
works and where it doesn't? And when can we "point to" a place or
places of agreement?

Harvey Friedman

On Wed, May 23, 2018 at 12:15 AM, Richard Kimberly Heck
<richard_heck at brown.edu> wrote:
> 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