[FOM] 349:Pi01 incompleteness/set series

Harvey Friedman friedman at math.ohio-state.edu
Mon Jul 20 23:21:10 EDT 2009


Let R be a binary relation on N^k. We define some nondeterministic  
notions of R derived set. Just as in Cantor's famous (deterministic)  
derived sets, our derived sets are subsets of the given set. And, as  
in Cantor, we iterate the process, ending in a "large" set.

We prove that for any suitable R there exist finite series of  
successive R derived sets of any finite length, which ends with an  
infinite cube. However, the proof necessarily uses Mahlo cardinals of  
all finite orders.

Harvey M. Friedman
July 18, 2009

1. E-1 delta RE.

We let N be the set of all nonnegative integers. A cube is a set of  
the form V^k, k >= 1.

Let R containedin N^k x N^k. For E containedin N^k, we define

RE = {y in N^k: (therexists x in A)(R(x,y)).

We say that R containedin N^k x N^k is upward if and only if

(forall x,y in N^k)(R(x,y) implies max(x) < max(y)).

COMPLEMENTATION THEOREM. For all k >= 1 and upward R contained in N^k  
x N^k, there exists a unique E contained in N^k, such that E delta RE  
= N^k. A contains the origin.

Actually, we can use any of the following four trivially equivalent  

E delta RE = N^k
E U. RE = N^k
E = N^k\RE
RE = N^k\E.

Here U. means "disjoint union".

THEOREM 1. For all k >= 1, there is an upward R contained in N^k x N^k  
such that for the unique E with E delta RE = N^k, E is the set  
consisting of the origin.

We now consider "approximations" to the set equation

E delta RE = N^k.

These "approximations" are called set series.

Let R contained in N^k x N^k and A contained in N^k.

A cube is a set of the form V^k.

For x in N^k and integers c, write x+c for the result of adding c to  
each coordinate. For B contained in N^k, write B+c = {x+c: x in B}.

We say that B is R derived from E if and only if B is the intersection  
of A with a cube contained in (E delta RE)-1.

A set series for R is a nonempty finite or infinite sequence of  
subsets of N^k, where each set is R derived from the preceding set.

THEOREM 2. For all k >= 1 and upward R contained in N^k x N^k, there  
is an infinite set series for R consisting of the same infinite set.

Just take E,E,E,..., where E is given by the Complementation Theorem.  
The cubes used will be N^k.

PROPOSITION 3. For all k,n >= 1 and upward R contained in N^k x N^k,  
there is a set series for R of length n ending with an infinite cube.

Let SMAH = ZFC + {there is a strongly n-Mahlo cardinal}_n. Let SMAH+ =  
ZFC + "for all n there is a strongly n-Mahlo cardinal".

THEOREM 4. Proposition 3 is provable in SMAH+ but not in any  
consistent subsystem of SMAH. In particular, Proposition 6 is not  
provable in ZFC, assuming ZFC is consistent. ACA proves that  
Proposition 3 is equivalent to Con(SMAH).

We now develop some explicitly concrete variants of Proposition 3. We  
let S(rel) be the binary successor relation (rather than the unary  
successor function).

PROPOSITION 5. Let k,n >= 1 and R contained in N^k x N^k be upward,  
where R is quantifier free definable in (N,S(rel),<). There is a set  
series for R of length n, quantifier free definable in (N,0,S,+,2^),  
ending with an infinite cube.

THEOREM 6. ACA proves the equivalence of Proposition 8 with Con(SMAH).

Obviously Proposition 5 is arithmetical, and in particular, is Pi04.  
In light of the decision procedure for the first order theory of (N, 
0,S,+,2^), referred to as exponential Presburger arithmetic, we see  
that Proposition 8 is Pi02. We can place a bound on the size of the  
quantifier free definitions in the conclusion as a function of the  
size of the quantifier free definition in the hypothesis. This results  
in a Pi01 form of Proposition 5.

We can avoid using exponential Presburger arithmetic, and give an  
explicit Pi01 form of Proposition 3 as follows.

PROPOSITION 7. Let p,n >> k and R containedin N^k x N^k be upward,  
where R is quantifier free definable in (N,S(rel),<). There is a set  
series for R of length n, starting with a subset of [0,p^n]^k, and  
ending with {1,p,...,p^n}^k. We can replace >> by a double exponential  

2. E-1 delta R(E+1), (E delta RE)-1.

We can replace

E-1 delta RE


E-1 delta R(E+1)
(E delta RE)-1

in the definition of set series for R, and obtain the same results in  
section 1. If we use E-1 delta R(E+1), then we get an added bonus: we  
can replace

quantifier free definable in (N,S(rel),<)

in Propositions 5,7 by

order invariant

which is the same as

quantifier free definable in (N,<).

This explicitly Pi01 sentence warrants an explicit presentation:

PROPOSITION 7. Let p,n >> k and R containedin N^k x N^k be upward and  
order invariant. There is a set series (using E-1 delta R(E+1)) for R  
of length n, starting with a subset of [0,p^n]^k, and ending with  
{1,p,...,p^n}^k. We can replace >> by a double exponential expression.


We can consider any (E+a delta R(E+b))+c, where a,b,c are integers. In  
this setup, we use the terminology

set series of kind (a,b,c).

Hence in section 1, we are using set series of kind (0,0,-1), and in  
section 2, we are using set series of kinds (-1,0,0), (-1,1,0).

It seems entirely manageable to determine the status of Proposition 3  
under any choice of kind (a,b,c).

In a different kind of templating, we can consider all Boolean  
expressions in E+a, R(E+b), where a,b are integers. In a given Boolean  
expression, there may be many a's and many b's. As a beginning, one  
should consider only a,b drawn from {-1,0,1}.

Many more ambitious templates along these lines can be investigated.


I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 349th 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
286: Godel's Second/still more  5/11/06  2:05PM
287: More Pi01 adventures  5/18/06  9:19AM
288: Discrete ordered rings and large cardinals  6/1/06  11:28AM
289: Integer Thresholds in FFF  6/6/06  10:23PM
290: Independently Free Minds/Collectively Random Agents 6/12/06
291: Independently Free Minds/Collectively Random Agents (more) 6/13/06
292: Concept Calculus 1  6/17/06  5:26PM
293: Concept Calculus 2  6/20/06  6:27PM
294: Concept Calculus 3  6/25/06  5:15PM
295: Concept Calculus 4  7/3/06  2:34AM
296: Order Calculus  7/7/06  12:13PM
297: Order Calculus/restatement  7/11/06  12:16PM
298: Concept Calculus 5  7/14/06  5:40AM
299: Order Calculus/simplification  7/23/06  7:38PM
300: Exotic Prefix Theory   9/14/06   7:11AM
301: Exotic Prefix Theory (correction)  9/14/06  6:09PM
302: PA Completeness  10/29/06  2:38AM
303: PA Completeness (restatement)  10/30/06  11:53AM
304: PA Completeness/strategy 11/4/06  10:57AM
305: Proofs of Godel's Second  12/21/06  11:31AM
306: Godel's Second/more  12/23/06  7:39PM
307: Formalized Consistency Problem Solved  1/14/07  6:24PM
308: Large Large Cardinals  7/05/07  5:01AM
309: Thematic PA Incompleteness  10/22/07  10:56AM
310: Thematic PA Incompleteness 2  11/6/07  5:31AM
311: Thematic PA Incompleteness 3  11/8/07  8:35AM
312: Pi01 Incompleteness  11/13/07  3:11PM
313: Pi01 Incompleteness  12/19/07  8:00AM
314: Pi01 Incompleteness/Digraphs  12/22/07  4:12AM
315: Pi01 Incompleteness/Digraphs/#2  1/16/08  7:32AM
316: Shift Theorems  1/24/08  12:36PM
317: Polynomials and PA  1/29/08  10:29PM
318: Polynomials and PA #2  2/4/08  12:07AM
319: Pi01 Incompleteness/Digraphs/#3  2/12/08  9:21PM
320: Pi01 Incompleteness/#4  2/13/08  5:32PM
321: Pi01 Incompleteness/forward imaging  2/19/08  5:09PM
322: Pi01 Incompleteness/forward imaging 2  3/10/08  11:09PM
323: Pi01 Incompleteness/point deletion  3/17/08  2:18PM
324: Existential Comprehension  4/10/08  10:16PM
325: Single Quantifier Comprehension  4/14/08  11:07AM
326: Progress in Pi01 Incompleteness 1  10/22/08  11:58PM
327: Finite Independence/update  1/16/09  7:39PM
328: Polynomial Independence 1   1/16/09  7:39PM
329: Finite Decidability/Templating  1/16/09  7:01PM
330: Templating Pi01/Polynomial  1/17/09  7:25PM
331: Corrected Pi01/Templating  1/20/09  8:50PM
332: Preferred Model  1/22/09  7:28PM
333: Single Quantifier Comprehension/more  1/26/09  4:32PM
334: Progress in Pi01 Incompleteness 2   4/3/09  11:26PM
335: Undecidability/Euclidean geometry  4/27/09  1:12PM
336: Undecidability/Euclidean geometry/2  4/29/09  1:43PM
337: Undecidability/Euclidean geometry/3  5/3/09   6:54PM
338: Undecidability/Euclidean geometry/4  5/5/09   6:38PM
339: Undecidability/Euclidean geometry/5  5/7/09   2:25PM
340: Thematic Pi01 Incompleteness 1  5/13/09  5:56PM
341: Thematic Pi01 Incompleteness 2  5/21/09  7:25PM
342: Thematic Pi01 Incompleteness 3  5/23/09  7:48PM
343: Goedel's Second Revisited 1  5/27/09  6:07AM
344: Goedel's Second Revisited 2  6/1/09  9:21PM
345: Thematic Pi01 Incompleteness 4 6/15/09  1:15PM
appears misnumbered as 344.
346: Goedel's Second Revisited 3  6/16/09  11:04PM
347: Goedel's Second Revisited 4  6/20/09  1:25AM
348: Goedel's Second Revisited 5  6/22/09  11:00AM

Harvey Friedman

More information about the FOM mailing list