[FOM] 286:Godel's Second/still more

[Harvey Friedman]

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

There we stated  

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

We prefer the following reformulation:

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

We also have a second form, with a slightly different title:

GODEL'S SECOND FOR FULLY INDUCTIVE SUBSYSTEMS. No finitely axiomatized
system in ordinary first order predicate calculus with equality is
interpretable in any of its consistent fully inductive subsystems.

Also, notice that, at least *informally*, we see that the usual Godel's
second stated in terms of consistency proofs, follows from the above, in the
case of inductive systems. For suppose T is an inductive system that proves
its own consistency. Then some finite fragment of T proves the consistency
of T. Hence some finite fragment of T interprets T by formalizing the
completeness theorem within a possibly bigger finite fragment of T. This
contradicts Godel's Second for Fully Inductive Systems.

As observed in #285, these two formulations (either one) are enough to
destroy a particularly clear form of Hilbert's program in a particularly
clear way. 

However, we would still like to get closer to the content of the usual
Godel's Second: 

if T is suitable then Con(T) is is not provable in T.

Obviously we cannot have

if T is suitable then T is not interpretable in T.

We would like 

if T is suitable then T' is not interpretable in T

where T' is as close as possible to T, and in particular is a conservative
extension of T. 

BINARY EXTENSIONS.

Let T be a system in ordinary first order predicate calculus. We define
BIN(T) as follows. The language of BIN(T) extends L(T) by

i. Adding a new sort for "binary relations" = "binary relations on objects
of T". 
ii. The ternary relation HD(R,x,y), meaning "the binary relation R holds at
the objects x,y". Here R is a relation variable and x,y are object
variables. 
iii. Predicative comprehension for relations. I.e., (therexists R)(forall
x,y)(HD(R,x,y) iff phi), where phi is a formula of BIN(T) in which R is not
free, and where there are no quantifiers over relations.

GODEL'S SECOND FOR BINARY EXTENSIONS. No consistent system in ordinary first
order predicate calculus interprets its binary extension. I.e., If T is a
consistent system in ordinary first order predicate calculus then BIN(T) is
not interpretable in T.

Note that we do NOT include any induction like axioms in BIN(T). In fact,
BIN(T) is a conservative extension of T.

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

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

Harvey Friedman