[FOM] 285:Godel's Second/more

Wed May 10 17:55:56 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
http://www.cs.nyu.edu/pipermail/fom/2006-May/010524.html

This supercedes the posting #284: Godel's Second, with url just above. We
start over. 

1. BETWEEN GODEL'S FIRST AND GODEL'S SECOND.

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

INTERPRETATION THEOREM (finitely axiomatized). 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,
whose language extends that of T, such that T'' is not interpretable in T.

INTERPRETATION THEOREM (common language, finitely axiomatized). 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.

The above theorems have extensions accommodating recursively axiomatized
systems. 

INTERPRETATION THEOREM (recursively axiomatized). Let T be a consistent
recursively 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,
whose language extends that of T, such that T'' is not interpretable in T.

INTERPRETATION THEOREM (common language, recursively axiomatized). Let T be
a consistent recursively 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.

The latter two theorems are false if we replace 'recursively' by
'co-recursively enumerable'.

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

2. GODEL'S SECOND FOR PA.

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 following 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:

i. 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

ii. 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

iii. 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 i-iii.

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.

GODEL'S SECOND FOR PA. PA is not interpretable in any finite fragment of PA.

Why do I call this Godel's Second for PA?

COROLLARY 1. No finitely axiomatized system in many sorted predicate
calculus, in which PA is interpretable, is interpretable in PA.

Proof: If it was, then it would be interpretable in a finite fragment of PA,
and PA would then be interpretable in a finite fragment of PA. This
contradicts Godel's Second for PA. QED

COROLLARY 2. ZF is not interpretable in PA. ZF\P is not interpretable in PA.
ACA_0 is not interpretable in PA.

Proof: Obviously PA is interpretable in a finite fragment of ZF, or even
ZF\P, using the standard model of PA. Also ACA_0 is finitely axiomatizable.
Apply Corollary 1. QED

HISTORIANS can comment on the following: It would appear to me that
Corollary 2 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).

3. GODEL'S SECOND FOR FULLY INDUCTIVE SYSTEMS.

Let T be a system in ordinary first order predicate calculus with equality.

We say that T is fully inductive if and only if there are formulas phi,psi
such that 

i. phi has at most the free variable x.
ii. psi has at most the free variables x,y,z.
iii. T proves psi implies phi.
iv. T proves (therexists x|phi)(forall y,z)(not psi)).
v. T proves (therexists x'|phi)(forall y',z')(psi(x/x',y/y',z/z') iff psi or
(y = y' and z = z').
vi. If rho holds of the empty x's with phi (see iii above), and rho is
preserved under adjunction of any y,z (see iv above), then rho holds of all
x|phi. Here rho is any formula of L(T).

Note that we stated the above semiformally in the interests of readability.

The idea is that phi(x) means "x is a finite binary relation", and
psi(x,y,z) means "x is a finite binary relation that holds of objects y,z".
The idea is that iv) asserts the existence of an empty finite binary
relation, and v) asserts that the finite binary relations are closed under
adjunction by pairs of objects. Also vi) asserts full induction for the
adjunction operation.

GODEL'S SECOND FOR FULLY INDUTIVE SYSTEMS. No consistent fully inductive
system is interpretable in any of its finite fragments.

COROLLARY 3. Let T be a consistent fully inductive system. No finitely
axiomatized system in many sorted predicate calculus, in which T is
interpretable, is interpretable in T.

COROLLARY 4. ZF is not interpretable in any finite fragment of ZF. ZFC +
"there exists an inaccessible  cardinal" is not interpretable in ZFC.

... more later ...

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 285th 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
284: Godel's Second  5/9/06  10:02AM

Harvey Friedman