[FOM] Godel's Second

[Harvey Friedman]

We began a discussion of Godel's incompleteness theorems in
http://www.cs.nyu.edu/pipermail/fom/2006-March/010258.html

Here we start a discussion of what might be a new treatment of Godel's 2nd
incompleteness theorem, with perhaps some clear advantages over present
treatments. 

My understanding of the present situation is as described by Feferman in

[1] S. Feferman, Finitary inductively presented logics, in: Logic Colloquium
'88 (R. Ferro, et al., eds.), North-Holland, Amsterdam (1989) 191-220.

I quote some excerpts:

"Where an exact notion of formal system is particularly needed in our
subject is in the formalization of metamathematics, beginning with G¨odel¹s
Second Incompleteness Theorem. As we know, this is very sensitive to how the
formal systems dealt with are presented (cf. Feferman [1960], Kreisel
[1965], 153­154). While the two-line informal argument for G¨odel¹s theorem
is very convincing, there is no really satisfactory presentation which is
both detailed and sufficiently general. But, as anyone knows who has gone
into proof theory at all, this is just the tip of the iceberg. For a number
of other examples, see the concluding section of this paper.

Pedagogical. ... A good conceptual framework is necessary to explain the
formalization of metamathematics in a reasonable and convincing way without
excessive hand-waving. Students gain confidence when they see that various
steps can be worked out systematically and in detail. This does not mean
that the subject must be presented entirely at such a level, just that
the mechanics of the details are at hand when confidence falters. As
intuition and experience take over, the need for such recedes, but the
existence of a manageable underlying framework is always reassuring."

*******************************************************

There seem to be two overriding approaches to a fully rigorous treatment of
Godel's Second.

1. Use the Hilbert Bernays derivability conditions for proof predicates.
This was sharpened by Jerosolow in

[2] R. Jerosolow, Redundancies in the Hilbert-Bernays Derivability
Conditions for Godel's Second Incompleteness Theorem, J. Symb. Log., vol.
38, no. 3, 1973, 359-367.

But then the difficulty is that one still has to present a natural proof
predicate for common systems like PA and ZFC, and verify that the natural
proof predicate obeys the Derivability conditions. Even presenting a natural
proof predicate fully is an extended mess, and then the problem of verifying
the derivability conditions is even worse. And then there is the problem of
explaining fully why the proof predicate presented is chosen.

2. Use the approach in [2]. Here one tries to get at what a good predicate
is, based on the idea that the given formal system has a kind of inductive
presentation. Then one can prove quite generally that the Derivability
conditions hold for proof predicates based on inductive generation. Or one
can avoid the Derivability conditions entirely and just go for Godel's
Second.

There are two problems with this approach. One is that it turns out to be
very complicated - just look at the size of this treatment. As a
consequence, even in [2], there is a declaration that there is no intention
of providing proofs.

Another drawback is that this approach only gives Godel's Second for systems
with a fair amount of induction. In fact, PRA is built in. We know that
various forms of Godel's Second hold in rather weak systems - far weaker
than PRA. 

#######################################################

We think that we might have some novel approaches that address a lot of
these difficulties. They are of two quite different kinds.

1. A version for set theories, that is of a semantic nature, rather than a
syntactic nature. Let T be a consistent finitely axiomatized set theory
containing a SURPRISINGLY weak set of axioms.  We assume that the language
is one sorted with only epsilon,=. Then T does not prove the existence of a
pair (A,R), A nonempty, R a set of ordered pairs from A, satisfying all
axioms of T. This does NOT require any definition of truth. One simply needs
to define the formula

(A,R) satisfies phi

in the language of set theory, for phi is any sentence in the language of
set theory. This is a trivial definition made outside the system.

A novelty here is just how SEVERELY weak the set of axioms can be taken to
be, with clever argumentation.

2. A purely syntactic version for systems of arbitrary kind. Here what we
seem to have found is some new set of derivability conditions that does NOT
include anything like "it is provable that provability implies provable
provability", and also NOT including provability of any form of induction.
In fact, the derivability conditions are rather simple, and EASILY verified
to hold in standard systems WITHOUT handwaving.

I am still thinking about the details of these two approaches.

The reason I am posting this NOW, is that I would like to hear from people
what they think about these issues and semi-claims 1,2, before I invest the
time for a full treatment with formal claims. After all, a very many readers
have worked with Godel's Second.

Harvey Friedman