[FOM] 341:Thematic Pi01 Incompleteness 2

Harvey Friedman friedman at math.ohio-state.edu
Thu May 21 17:46:51 EDT 2009

Harvey M. Friedman
May 21, 2009

We rearrange the presentation so that we have a nicely parameterized  
statement. We ask for information about the choices of parameters for  
which the statement is true. There are certain sufficient conditions.  
The statement that these conditions are sufficient is equivalent to  
the consistency of strongly Mahlo cardinals over ACA.

We define N to be the set of all nonnegative integers. For any set A
containedin N^k, we write A' = N^k\A. The difference between two sets
A,B is A\B.

Let R containedin N^k x N^k = N^2k. We say that R is upwards if and  
only if

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

We define RA for A containedin N^k, by

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

THEOREM 1. For all k >= 1 and upwards R containedin N^2k, there exists
A containedin N^k, such that RA = A'. Furthermore, A is unique.

We want to work with very concrete R containedin N^2k.

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^p is order invariant if and only if for
all order equivalent x,y in N^p, x in R iff y in R.

We have the following concrete form of Theorem 1. Here EXP means "the
characteristic function is computable in exponential time".

THEOREM 2. For all k >= 1 and upwards order invariant R containedin
N^2k, there exists A containedin N^k such that RA = A'. Furthermore, A  
is unique and lies in EXP.

We now consider a family of expressions involving
R,A,A',union,intersection, which we call *image terms in R,A*. These
are defined inductively as follows.

i. A,A' are image terms in R,A.
ii. if s,t are image terms in R,A, then s union t, s intersect t are
image terms in R,A.
iii. if s is an image term in R,A, then R(s) is an image term in R,A.

Let s be an image term in R,A. We define the rank of s to be the  
number of occurrences of R in t. We say that s is similar to t if and  
only if t is obtained from s by replacing some occurrences of RA by  
A', and some occurrences of A' by RA. Here "some" means "none, some,  
or all".

In an abuse of notation, if k,R,A have been specified, we think of t
both as a syntactic object and as the subset of N^k obtained by

The following is obvious from Theorem 2.

THEOREM 3. For all k >= 1 and upwards order invariant R containedin  
N^2k, there exists A containedin N^k such that any two similar image  
terms in R,A are equal. Furthermore, A is unique and lies in EXP.

We now consider the following statement with parameters k,E,S. We say  
that two sets U,V agree on a third set W if and only if

U intersection W =
V intersection W.

P(k,E,S). Let k >= 1 and E,S be subsets of N. For all upwards order  
invariant R containedin N^2k, there exists A containedin E^k, such  
that any two similar image terms in R,A of rank at most k agree on S^k.

Some sufficient conditions on k,E,S result in statements equivalent to  
Con(MAH) over ACA, which can also easily be seen to be Pi01. Others  
lead to inconsistency. As in the previous postings, they also  
trivially lead to statements that are explicitly Pi01, with the same  
metamathematical properties.

For example, here is a sufficient condition. S = {1,2,4,...}, E = N 
\{2^p - 1,2^p+1 - 1,2^p+2 - 1,...}, where p is, say, 2^2^8k. This will  
have the desired incompleteness properties.

It is natural to study the case where E,S are Boolean combinations of  
positive exponential expressions in k. In this case, we can adjust the  
sufficient condition to be

S = {2^n + 1: n >= 0}, E = N\{2^(n+c): n > = 0, c = 2^2^8k}.

Here we can take positive exponential expressions to allow addition,  
0, and base 2 exponentiation.

I think that there is a powerful and understandable sufficient  
condition on k,E,S, based on some simple inequalities. It would be  
exactly the kind of sufficient condition one would look for in a  
totally ordinary mathematical investigation of P(k,E,S). This would  
not involve restriction to the class of positive exponential  
expressions. Special cases of k,E,S already lead to strongly Mahlo  
cardinals (consistency thereof).


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

Harvey Friedman

More information about the FOM mailing list