# [FOM] 168:Incompleteness Reformulated/Again

Harvey Friedman friedman at math.ohio-state.edu
Thu May 8 12:30:15 EDT 2003

```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
```