[FOM] 284: Godel's Second

Tue May 9 10:02:28 EDT 2006

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

This is a continuation of
http://www.cs.nyu.edu/pipermail/fom/2006-April/010324.html

We begin with something between Godel's first and Godel's second.

INTERPRETATION THEOREM. Let T be a consistent finitely axiomatized system in
ordinary predicate calculus. There is a consistent finitely axiomatized
system T' in ordinary predicate calculus, whose language is a single binary
relation symbol, such that T' is interpretable in T but T is not
interpretable in T'. There is a consistent finitely axiomatized extension
T'' of T in ordinary predicate calculus with equality, whose language
extends that of T, such that T'' is not interpretable in T.

INTERPRETATION THEOREM (extension). Let T be a consistent finitely
axiomatized system in ordinary predicate calculus, in which Robinson's Q is
interpretable. There is a consistent finitely axiomatized extension of T in
the same language as T, which is not interpretable in T.

I stated some closely related Theorems some time ago on the FOM.

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

We now deal directly with Godel's Second.

A lot of underlying issues discussed earlier in
http://www.cs.nyu.edu/pipermail/fom/2006-April/010324.html

of a conceptual and educational nature can be addressed, directly and
indirectly, through the folowing project:

give completely rigorous fully stated versions of Godel's Second which are
very general, at the same time fairly simple to state.

The usual completely rigorous full statements have the following features:

1. They rely on some specific consistency statement, which is very detailed
and very special, with various ad hoc decisions made along the way. This is
not, prima facie, general, and is also obviously not simple. One handwaves
that it makes no difference just how this coding is done. Or

2. One states general conditions on the coding so that, in the presence of
induction, one can prove Godel's Second. This is not done too often, but
when it is done, the number of general conditions needed is quite large, and
the whole presentation is complicated. One has to incorporate conditions
corresponding to virtually all relevant syntactic notions. Or

3. One states general Hilbert/Bernays derivability conditions, or
streamlined versions due to Jerosolow. But then one has the problem of
showing that the ultimate consistency statement for the systems being
treated actually obeys these derivability conditions. This is usually
handwaved with informal to semiformal arguments. Usually no consistency
statement is actually given.

So what we want to do is something that avoids 1-3.

Let us proceed slowly and first talk about Godel's Second in the context of
PA only. PA is the most common single system for which people discuss
Godel's Second. Here the language of PA can be the traditional 0,S,+,x, or
can be infinite, with, say, symbols for each primitive recursive function.

INFORMAL SECOND FOR PA. Let T be a finitely axiomatized system in many
sorted predicate calculus, in a finite language. Assume that PA is
interpretable in T. There is no presentation in PA of a system of objects of
type L(T) which, provably in PA, forms an interpretation of L(T) in which
every axiom of T holds.

HISTORIANS can comment on the following: It would appear to me that the
above version is enough to have deeply affected Hilbert in a particularly
direct and unambiguous way. This is because Hilbert wanted, for instance, to
construct a model of ZFC within PA (of course even much less than PA), and
PA is interpretable in a finite fragment of ZFC. Furthermore, one can
explicitly give this interpretation.

Now how does this formulation of Godel's Second for PA avoid 1-3 above?

There is no arithmetization of syntax needed, whatsoever. One only needs to
make the following definition of a model theoretic nature, which is just
formalized relativization:

Let T be any theory in many sorted predicate calculus. Let L* be a finite
language in many sorted predicate calculus. One easily defines the following
with no significant complications.

a. A presentation in T of a system of objects of type L*. This just means
that one has formulas of L(T) carving out the domains of the various sorts
in L*, and appropriate formulas associated with the constant, relation, and
function symbols of L*. There are free variable conditions needed on these
formulas.

b. The sentence of L(T) that expresses that a given presentation in T of a
system of objects of type L*, according to a, actually forms an
interpretation of L*. This sentence is easily constructed from the
presentation, and asserts that i) the formulas in the presentation
corresponding to the domains have nonempty extensions; ii) the formulas in
the presentation corresponding to constant symbols have unique extensions;
iii) the formulas in the presentation corresponding to function symbols are
appropriately total and univalent. (Of course, sorting must be properly
taken into account).

c. The sentence of L(T) that expresses that a given interpretation of L*,
according to b, satisfies a given sentence of L*. This is just formalized
relativization, and is easily defined inductively.

Note that definitions a-c are made outside the system, by fairly simple
inductive definitions of the kind involved in setting up predicate calculus
itself. 

Using a-c, we have converted the above Informal Second for PA

into completely formal Godel's Second for PA.

Of course, this approach is, at least so far, restricted to PA.

However, it immediately extends to many sorted systems whose axioms include
all instances of induction in the full language.

GODEL'S SECOND FOR EXTENSIONS OF INDUCTION. Let S,T be systems in many
sorted predicate calculus. Assume that S is consistent, S has a sort
("reserved for nonnegative integers') with at least 0,S, and that every
instance of induction in L(S) is an axiom of S. Assume that L(T) is finite,
T has finitely many axioms, and S is interpretable in T. There is no
presentation in S of a system of objects of type L(T) which, provably in S,
forms an interpretation of L(T) in which every axiom of T holds.

There is the matter of Godel's Second where S doesn't have all this
induction, where S is finitely axiomatized, and also the matter of infinite
languages, as well as a number of other issues. Some interesting things are
about to happen... 

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 284th 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-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected from
the original.

250. Extreme Cardinals/Pi01  7/31/05  8:34PM
251. Embedding Axioms  8/1/05  10:40AM
252. Pi01 Revisited  10/25/05  10:35PM
253. Pi01 Progress  10/26/05  6:32AM
254. Pi01 Progress/more  11/10/05  4:37AM
255. Controlling Pi01  11/12  5:10PM
256. NAME:finite inclusion theory  11/21/05  2:34AM
257. FIT/more  11/22/05  5:34AM
258. Pi01/Simplification/Restatement  11/27/05  2:12AM
259. Pi01 pointer  11/30/05  10:36AM
260. Pi01/simplification  12/3/05  3:11PM
261. Pi01/nicer  12/5/05  2:26AM
262. Correction/Restatement  12/9/05  10:13AM
263. Pi01/digraphs 1  1/13/06  1:11AM
264. Pi01/digraphs 2  1/27/06  11:34AM
265. Pi01/digraphs 2/more  1/28/06  2:46PM
266. Pi01/digraphs/unifying 2/4/06  5:27AM
267. Pi01/digraphs/progress  2/8/06  2:44AM
268. Finite to Infinite 1  2/22/06  9:01AM
269. Pi01,Pi00/digraphs  2/25/06  3:09AM
270. Finite to Infinite/Restatement  2/25/06  8:25PM
271. Clarification of Smith Article  3/22/06  5:58PM
272. Sigma01/optimal  3/24/06  1:45PM
273: Sigma01/optimal/size  3/28/06  12:57PM
274: Subcubic Graph Numbers  4/1/06  11:23AM
275: Kruskal Theorem/Impredicativity  4/2/06  12:16PM
276: Higman/Kruskal/impredicativity  4/4/06  6:31AM
277: Strict Predicativity  4/5/06  1:58PM
278: Ultra/Strict/Predicativity/Higman  4/8/06  1:33AM
279: Subcubic graph numbers/restated  4/8/06  3:14AN
280: Generating large caridnals/self embedding axioms  5/2/06  4:55AM
281: Linear Self Embedding Axioms  5/5/06  2:32AM
282: Adventures in Pi01 Independence  5/7/06
283: A theory of indiscernibles  5/7/06  6:42PM

Harvey Friedman 