[FOM] 168:Incompleteness Reformulated/Again

[Harvey Friedman]

Solovay 5/7/03 3:21PM, points out that for in my posting #167, one 
has to be careful about what form of predicate calculus one is using. 
He points out that the part of Theorem 1 that asserts that T can be 
taken to contain S is incorrect for predicate calculus with equality.

However, the result as stated is correct for predicate calculus 
without equality. It is also correct as stated for many sorted 
predicate calculus with equality,

For predicate calculus with equality, it can be fixed by requiring 
that S has an infinite model.

Here are the modified statements with "S is a subset of T, or "S is 
provable in T".

THEOREM 1. Let S be any consistent finite set of sentences in 
predicate calculus without equality (or in many sorted predicate 
calculus with equality). There is a consistent finite set T of 
sentences in predicate calculus without equality (or in many sorted 
predicate calculus with equality) which is not interpretable in S, 
and where S is a subset of T.

THEOREM 2. Let S be any finite set of sentences in predicate calculus 
with equality, which has an infinite model. There is a consistent 
finite set T of sentences in predicate calculus with equality which 
is not interpretable in S, and where S is a subset of T.

Note, e.g., that if S consists of just "there is exactly one object", 
then every consistent extension T of S follows from S.

Here are versions of the above for recursively enumerable sets of sentences.

THEOREM 3. Let S be any recursively enumerable set of sentences in 
predicate calculus without equality (or in many sorted predicate 
calculus with equality) in a finite relational type. There is a 
consistent finite set T of sentences in predicate calculus without 
equality (or in many sorted predicate calculus with equality) which 
is not interpretable in S, and where S is provable in T.

THEOREM 4. Let S be any recursively enumerable set of sentences in 
predicate calculus with equality, in a finite relational type, which 
has an infinite model. There is a consistent finite set T of 
sentences in predicate calculus with equality which is not 
interpretable in S, and where S is provable in T.

Note that if S consists of the infinite set of one sorted sentences 
Pi(c), then S has no consistent finitely axiomatized extension in 
(many sorted) predicate calculus with equality.

What if we drop the conclusion that "S is a subset of T" or "S is 
provable in T"?

THEOREM 5. Let S be any consistent recursively enumerable set of 
sentences in many sorted predicate calculus with equality. There is a 
consistent finite set T of sentences in predicate calculus without 
equality which is not interpretable in S.

Here we always take "interpretable" in the classical sense of Tarski.

Theorems 1-5 can be easily obtained from well known forms of the 
Godel second incompleteness theorem.

Theorems 1-5 can instead be proved using well known recursion theoretic ideas.

Note that there are no technical hypotheses appearing in these formulations.

The second incompleteness theorem gives a particularly interesting 
construction of T from S in Theorems 1-5.

THEOREM 6. There is a consistent finite set of sentences K in 
predicate calculus such that any consistent recursively enumerable 
set of sentences T in predicate calculus with equality that 
interprets K is incomplete.

The first incompleteness theorem gives a particularly interesting 
construction of K.

We can ask: how tiny can K be?

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.

This is the 168th 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/statisics  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