[FOM] 174:Directly Honest 2nd Incompleteness

[Harvey Friedman]

OBJECTION TO SECOND THEOREM. It appears that no formal system can 
make assertions, in a completely honest and direct way, about its own 
syntax.

Actually, the above is really a conjecture that requires both very 
careful formulation and very careful proof. I have not done the 
necessary analysis.

1. ILLUSTRATION OF THE OBJECTION.

Let us attempt to address the first crucial point by constructing a 
system of set theory that can make assertions, in a completely honest 
and direct way, about its own syntax.

Let us start with ZFC, and fully accept the set theoretic 
interpretation of mathematics. To make things more honest, we will 
actually start with ZFC with urelements. The vocabularly of ZFCU is 
as follows:

( (punctuation)
) (punctuation)
epsilon (binary relation symbol for membership)
not (connective)
and (connective)
or (connective)
arrows (connective)
doublearrows (connective)
forall (quantifier)
therexists (quantifier)
0 (bit)
1 (bit)
x (variable)
= (special binary relation symbol for equality)
M (unary relation symbol for sethood)

REMARK: The important syntactic entities associated with ZFCU are all 
certain finite strings of letters in this 15 letter alphabet. 
Variables are finite strings starting with x, followed by zero or 
more bits. END

ZFCU cannot talk directly about itself since it doesn't have any way 
to refer to these actual 15 symbols.

So to get ZFCU to overcome this limitation, we expand its vocabularly 
as follows.

( (punctuation)
) (punctuation)
epsilon (binary relation symbol for membership)
not (connective)
and (connective)
or (connective)
arrows (connective)
doublearrows (connective)
forall (quantifier)
therexists (quantifier)
0 (bit)
1 (bit)
x (variable)
= (special binary relation symbol for equality)
M (unary relation symbol for sethood)
")" (constant symbol)
"(" (constant symbol)
"epsilon" (constant symbol)
"not" (constant symbol)
"and" (constant symbol)
"or" (constant symbol)
"arrows" (constant symbol)
"doublearrows" (constant symbol)
"forall" (constant symbol)
"therexists" (constant symbol)
"0" (constant symbol)
"1" (constant symbol)
"x" (constant symbol)
"=" (constant symbol)
"M" (constant symbol)

We let ZFCU' be the result of expanding the language of ZFCU in this way.

We add the following additional nonlogical axioms:

i. M(c), where c is any of these fifteen constant symbols.
ii. not c = d, where c,d are any of these fifteen constant symbols 
that are distinct.

Note that ZFCU' talks directly and honestly about the syntax of ZFCU. 
However, ZFCU' does not talk directly and honestly about the syntax 
of ZFCU'.

In order for ZFCU' to talk directly and honestly about the syntax of 
ZFCU', we need to add additional constant symbols.

However, we then have the same problem.

The only way around this would seem to be to construct a system that 
handles the limit of this procedure properly. But this is very 
delicate. One would probably have to add an operator corresponding to 
"placing quote signs", with appropriate axioms involving this 
operator. But then, the symbol for the operator itself creates 
additional syntactic structure, which itself must be discussed.

2. DEFENSE AGAINST THE OBJECTION.

There is a very straightforward. We concede the objection, but 
formulate the second theorem for ZFCU as follows.

THEOREM 1. If ZFCU is consistent then the consistency of ZFCU is not 
provable in ZFCU'.

Let WSTU be a weak set theory with urelements. E.g., extensionality, 
pairing, union, separation. Let T be a finitely axiomatized extension 
of WSTU. It is clear what the system T' is. We just add the same 
constant symbols.

THEOREM 2. Let T be a finitely axiomatized extension of WSTU. If T is 
consistent then T' does not prove the consistency of T.

Since WSTU is so closely related to PA (Peano Arithmetic), we obtain 
some of the  usual formulations of the 2nd incompleteness theorem as 
a Corollary to Theorem 2.

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 174th 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-149 can be found at 
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM 
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM

Harvey Friedman