[FOM] 321: Pi01 Incompleteness/forward imaging

Harvey Friedman friedman at math.ohio-state.edu
Tue Feb 19 17:12:16 EST 2008


We define N to be the set of all nonnegative integers.

We will use three different notions of: forward image of R on A. Here  
it is required that for some k >= 1, R containedin N^4k, and A  
containedin N^k. Specifically,

RA = {w in N^k: (therexists x,y,z in A)(R(x,y,z,w))}.

R<A = {w in N^k: (therexists x,y,z in A)(R(x,y,z,w) and  
max(x),max(y),max(z) < max(w))}.

R*A = {w in N^k: (therexists x,y,z in A)(R(x,y,z,w) and  
max(x),max(y),max(z) not= max(w)-1)}.

For A containedin N^k, define A' = N^k\A.

NOTE: Typographically, in R<A, the < is a subscript.

THEOREM 1.1. For all k >= 1 and R containedin N^4k, some R<A is A'.  
Furthermore, A is unique.

We say that x,y in N^k are order equivalent if and only if for all 1  
<= i,j <= k, x_i < x_j iff y_i < y_j. We say that R containedin N^k is  
order invariant if and only if for all order equivalent x,y in N^k,  
R(x) iff R(y).

For n >= 1, the powers of n are the tuples whose coordinates are drawn  
from {1,n,n^2,...}.

PROPOSITION 1.2. For all k >= 1 and order invariant R containedin  
N^4k, some R*R<A is a subset of R(A') with the same powers of (8k)!.

MAH = ZFC + {there exists a strongly n-Mahlo cardinal}_n. MAH+ = ZFC +  
"for all n there exists a strongly n-Mahlo cardinal".

THEOREM 1.3. Theorem 1.1 is provable in RCA_0. Proposition 1.2 is  
provable in MAH+ but not in MAH, assuming that MAH is consistent.  
Proposition 1 is provably equivalent, over ACA, to CON(MAH).  
Proposition 1 is not provable in any consistent subsystem of MAH. In  
particular, Proposition 1 is not provable in ZFC, assuming ZFC is  
consistent. If we delete * then Proposition 1.2 becomes a weakened  
form of Theorem 1.1.

The 4 in "4k" can be extended to any higher number in the obvious way  
without changing the results. We have not investigated the  
independence status when 4 is replaced by 2 or 3. Probably 3 will  
still give the same results, but 2 is not enough for independence.

Here (8k)! is just a convenient expression.

We can use Z+ instead of N.


The finite form is obtained trivially by replacing N with [0,n]. All  
of the definitions are restated in the obvious way with N replaced  
throughout by [0,n]. Specifically,

PROPOSTION 2.2. For all k,n >= 1 and order invariant R containedin  
[0,n]^4k, some R*R<A is a subset of R(A') with the same powers of (8k)!.

Note that Proposition 2.2 is explicitly Pi01.

All of the results read the same.

We can use [1,n] instead of [0,n].


Note that all three of the forward imaging notions that we have used  
can be unified in the following way.

Let # containedin N^2. We define #-imaging as follows.

For all k >= 1 and R containedin N^4k, we define R# the function  
mapping subsets of N^k into subsets of N^k, given by

R#A = {w: (therexists x,y,z in A)(R(x,y,z,w) and #(max(x),max(w)),  
#(max(y),max(w)), #(max(z),max(w)))}.

Note that the three forward image construction that we have used, RA,  
R<A, R*A, can be viewed as R#A, R##A, R###A, where

#(n,m) iff n = n.
##(n,m) iff n < m.
###(n,m) iff n not= m-1.

It is reasonable to require that # containedin N^2 be a Presburger  
relation. I.e., definable in (N,+). More restrictive requirements also  
make sense.

This leads to the following Template.

TEMPLATE. Let #,##,### be Presburger subsets of N^2. For all k >= 1  
and order invariant R containedin N^4k, some R#R##A is a subset of  
R###(A') with the same powers of (8k)!.

TEMPLATE. Let #,##,### be Presburger subsets of N^2. For all k,n >= 1  
and order invariant R containedin [0,n]^4k, some R#R##A is a subset of  
R###(A') with the same powers of (8k)!.

We intend to determine the status of all instances of these Templates.  
We conjecture that every instance is either provable in RCA_0,  
refutable in RCA_0, or provably equivalent to CON(MAH) over RCA_0. The  
latter occurs according to THeorems 1.3 and 2.3.

Obviously, further Templating can be done along these lines. E.g., we  
can consider using

R#1 R#2 ... R#p A is a subset of R#p+1 R#p+2 ... R#p+q A' with the  
same powers of (8k)!

where p,q >= 0 and the #'s are Presburger subsets of N^2. We make the  
extended conjecture.

I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 321st 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  
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

Harvey Friedman

More information about the FOM mailing list