[FOM] 323: Pi01 Incompleteness/point deletion
Harvey Friedman
friedman at math.ohio-state.edu
Fri Mar 14 07:28:49 EDT 2008
We rework posting 322, using point deletion instead of forward imaging. The
statements and Templates are simpler.
1. INFINITE STATEMENTS.
We define N to be the set of all nonnegative integers.
Let R containedin N^4k and A containedin N^k. We define A' = N^k\A.
We say that R is upwards if and only if for all x in N^3k and y in
N^k, (x,y) in R implies max(x) < max(y).
We define
RA = {y in N^k: (therexists x in A^3)((x,y) in R)}.
The following is implicit in the (hyper)graph theory literature.
THEOREM 1.1. For every upwards R containedin N^4k there is a (unique) A such
that RA = A'.
We say that A is R independent if and only if A containedin N^k, and
A,RA are disjoint.
Clearly, if RA = A' then A is R independent. So asserting that A is R
independent is clearly redundant. However, we state the following in
preparation for our independent proposition.
THEOREM 1.2. Every upwards R containedin N^4k has an (unique) independent A
such that RA = A'.
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, x
in R iff y in R.
The k dimensional powers of r are the elements of {1,r,r^2,...}^k.
PROPOSITION 1.3. For all r >> k, every upwards order invariant R containedin
N^4k has an independent A such that RRA and R(A'\{r}^k) have the same k
dimensional powers of r+1. We can replace r >> k with r >= (8k)!, or with r
= (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.4. Theorems 1.1,1.2 are provable in RCA_0. Proposition 1.3 is
provable in MAH+ but not in MAH, assuming that MAH is consistent.
Proposition 1.3 is provably equivalent, over ACA, to CON(MAH).
Proposition 1.3 is not provable in any consistent subsystem of MAH. In
particular, Proposition 1.3 is not provable in ZFC, assuming ZFC is
consistent. If we delete \{r}^k then Proposition 1.3 becomes a weakened
form of Theorems 1.1,1.2.
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.
We can use Z+ instead of N.
2. FINITE STATEMENTS.
For A containedin [0,n]^n, define A' = [0,n]^k\A.
THEOREM 2.1. For every upwards R containedin [0,n]^4k there is a (unique) A
such that RA = A'.
We say that A is R independent if and only if A containedin [0,n]^k, and
A,RA are disjoint.
THEOREM 2.2. Every upwards R containedin [0,n]^4k has a (unique)
independent A such that RA = A'.
PROPOSITION 2.3. For all r >> k, every upwards order invariant R containedin
[0,n]^4k has an independent A such that RRA and R(A'\{r}^k) have the same k
dimensional powers of r+1. We can replace r >> k with r >= (8k)!, or with r
= (8k)!.
MAH = ZFC + {there exists a strongly n-Mahlo cardinal}_n. MAH+ = ZFC +
"for all n there exists a strongly n-Mahlo cardinal".
THEOREM 2.4. Theorems 2.1,2.2 are provable in RCA_0. Proposition 2.3 is
provable in MAH+ but not in MAH, assuming that MAH is consistent.
Proposition 2.3 is provably equivalent, over ACA, to CON(MAH).
Proposition 2.3 is not provable in any consistent subsystem of MAH. In
particular, Proposition 2.3 is not provable in ZFC, assuming ZFC is
consistent. If we delete \{r}^k then Proposition 2.3 becomes a weakened
form of Theorems 2.1,2.2.
We can use [1,n] instead of [0,n].
3. INFINITE TEMPLATE.
Our Template for Proposition 1.3 involves replacing the expressions RRA and
R(A'\{r}^k) by other expressions.
It is most basic to consider the following expressions.
a. A, A\{r}^k, A', A'\{r}^k are expressions.
b. If alpha is an expression then so is RA.
The positive expressions are those that use A or A\{r}^k. The negative
expressions are those that use A' or A'\{r}^k. The normal expressions are
the ones that use A or A', and the deletion expressions are the ones that
use A\{r}^k or A'\{r}^k.
TEMPLATE 3.1. Let alpha_1,...,alpha_p be expressions, p >= 1. For all r >>
k, every upwards order invariant R containedin N^4k has an independent A
such that alpha_1,...,alpha_p have the same k dimensional powers of r+1.
PROPOSITION 3.2. Template 3.1 holds if and only if the positive alpha's all
use the same number of R's, the negative alpha's all use the same number of
R's, and every positive alpha uses exactly one more R than every negative
alpha. Furthermore, if this holds, then we can replace r >> k with r >=
(8kp)!, or with r = (8kp)!. where p is the maximum number of R's used in any
one of the alpha's.
THEOREM 3.3. If the condition in Proposition 3.2 fails for
alpha_1,...,alph_p, p >= 1, then Template 3.1 is refutable in RCA_0. If the
condition in Proposition 3.2 holds, where there are positive and negative
alpha's, all with at least one R, and at least one alpha is a deletion
expression, then Template 3.1 is provable equivalent, over ACA, to CON(MAH).
Otherwise, Template 3.1 is provable in RCA_0.
THEOREM 3.4. Proposition 3.2 is provably equivalent, over ACA, to CON(MAH).
4. FINITE TEMPLATE.
TEMPLATE 4.1. Let alpha_1,...,alpha_p be expressions, p >= 1. For all r >>
k, every upwards order invariant R containedin [0,n]^4k has an independent A
such that alpha_1,...,alpha_p have the same k dimensional powers of r+1.
PROPOSITION 4.2. Template 4.1 holds if and only if the positive alpha's all
use the same number of R's, the negative alpha's all use the same number of
R's, and every positive alpha uses exactly one more R than every negative
alpha. Furthermore, if this holds, then we can replace r >> k with r >=
(8kp)!, or with r = (8kp)!. where p is the maximum number of R's used in any
one of the alpha's.
THEOREM 4.3. If the condition in Proposition 4.2 fails for
alpha_1,...,alph_p, p >= 1, then Template 4.1 is refutable in EFA. If the
condition in Proposition 4.2 holds, where there are positive and negative
alpha's, all with at least one R, and at least one alpha is a deletion
expression, then Template 4.1 is provable equivalent, over ACA, to CON(MAH).
Otherwise, Template 4.1 is provable in EFA.
THEOREM 4.4. Proposition 4.2 is provably equivalent, over ACA, to CON(MAH).
**********************************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 323rd 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
11:01AM
291: Independently Free Minds/Collectively Random Agents (more) 6/13/06
5:01PM
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
Harvey Friedman
More information about the FOM
mailing list