[FOM] 810: Goedel's Second Reworked/2

[Harvey Friedman]

Continuation from
https://cs.nyu.edu/pipermail/fom/2018-May/020996.html Also see Richard
Heck, 5/23/18.

REMARK ON THE STRUCTURAL FACT

The Structural Fact is really just a convenient particularly friendly
positive way of talking about the classic

*some r.e. set does not have an r.e. complement"

That is a perfectly fine formulation, though not very positive. When
we go to the sharper form, the "negativity" gets more annoyingly
unfriendly.

So here is a slightly expanded form of the Structural Fact.

STRUCTURAL FACT. 1. There is an r.e. set whose complement is not r.e.
2. 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.)
3. 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: The standard proof of 1) uses A = {e: the e-th TM halts at e}.
2) is trivially equivalent to 1), for if A,B don't agree anywhere then
B is the complement of A. The standard proof of 1),2) also establishes
3) without change. QED

MORE COMMENTS ON THE PROOF OF GSIT
https://cs.nyu.edu/pipermail/fom/2018-May/020996.html

This proof is (as it stands now) offered up as a major improvement on
the known semi formal proofs of GSIT. I have not been addressing how
this proof may fit into research on formal proofs of GSIT, issues that
are of major concern to proof theorists.

At the practical level, I would be curious how using this semi formal
proof would fare in these contexts:

non advanced logic courses
general philosophers
mathematicians not generally interested in math logic
mathematical logicians not generally interested in proof theory
general intellectuals

As observed by Heck, 5/23/18, the usual proof with G1/G2 corresponds
to using G1 instead of Structural Fact. However, I am suggesting that
there are major advantages to using Structural Fact instead of G1
here. E.g.,

1. It makes much more sense for the teacher to blackbox the Structural
Fact (i.e., emphasize its meaning but omit its (easy diagonal) proof),
than to similarly blackbox G1. An accurate statement of G1 is
incomparably more involved than an accurate statement of Structural
Fact (the latter not using any trace of predicate calculus, formal
systems, etcetera).
2. It has the advantage of pointing to a very fundamental "other
subject" that is very robustly clean mathematically. So in this sense,
my proof puts the purely mathematical part of general mathematical
interest, at the beginning, going as far as I can, before even
touching the math logic concepts and arguments. The interface between
the two parts is particularly clean.

OBVIOUSLY THE BEST TEST OF HOW GOOD THIS PROOF (IN THE SENSE INTENDED
HERE) IS TO ACTUALLY TRY IT OUT ON VARIOUS AUDIENCES!
I COULD BE QUITE WRONG (or quite right)

LITTLE SPINOFF SUBJECT? AGREEMENT THEORY?

Given a natural family of mathematical
objects, ask for agreement phenomena.

EXAMPLE. Any two homeomorphisms of the closed unit interval agree
somewhere. Three homeomorphisms of the closed unit interval either all
agree at a common point or two of them agree at a common intermediate
point. Any two distinct lines in the plane have 0 or 1 points in
common. These of course behave very differently than the r.e. sets.

PROJECTS: Give a decision procedure (and complete axiomatizations) for
all such elementary statements about various classes of mathematical
objects. What are some very natural fundamental classes of
mathematical objects that behave more like the r.e. sets? I sort of
recall that maybe enumeration operators are relevant here, and if so,
can they be further integrated into the fabric of standard
mathematical environments?

THE GREAT MYSTERY OF GSIT

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 (perhaps more than you want to hear) about it if and when I figure it out.

Incidentally, we are much closer to the "right" proof of the weaker
(and somewhat more technical) GSIT: No reasonable system can prove its
1-consistency. Much much clearer... I'd like to see a proof of GSIT
that is (almost) as good as what we have for this weaker GSIT.

************************************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 810th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

800: Beyond Perfectly Natural/6  4/3/18  8:37PM
801: Big Foundational Issues/1  4/4/18  12:15AM
802: Systematic f.o.m./1  4/4/18  1:06AM
803: Perfectly Natural/7  4/11/18  1:02AM
804: Beyond Perfectly Natural/8  4/12/18  11:23PM
805: Beyond Perfectly Natural/9  4/20/18  10:47PM
806: Beyond Perfectly Natural/10  4/22/18  9:06PM
807: Beyond Perfectly Natural/11  4/29/18  9:19PM
808: Big Foundational Issues/2  5/1/18  12:24AM
809: Goedel's Second Reworked/1  5/20/18  3:47PM

Harvey Friedman