[FOM] 344: Thematic Pi01 Incompleteness 4
Harvey Friedman
friedman at math.ohio-state.edu
Mon Jun 15 13:16:35 EDT 2009
There has been substantial progress on finding specific Pi01
independent statements. The next posting will concern Templates.
Pi01 INCOMPLETENESS
DRAFT
Harvey M. Friedman
June 15, 2009
1. Definitions.
2. Independent Propositions.
3. Alternative: independence.
4. Alternative: foreignness.
5. Alternative: independence, foreignness.
6. Exponential Presburger.
1. DEFINITIONS.
We define N to be the set of all nonnegative integers.
Let R containedin N^pk x N^k. For A_1,...,A_p containedin N^k, we define
R(A_1,...,A_p) = {y in N^k: (therexists x_1,...,x_p from A_1,...,A_p,
respectively)(R(x_1,...,x_p,y))}.
It is very convenient to define
RA = R(A,...,A)
where there are p A's. Here we require that A,A_1,...,A_p containedin
N^k
We sometimes view N^pk x N^k as N^pk+k.
We say that R containedin N^pk x N^k is upwards if and only if
(forall x in N^pk)(forall y in N^k)(R(x,y) implies max(x) < max(y)).
Let x,y in N^s. We say that x,y have the same order type if and only if
(forall 1 <= i,j <= s)(x_i < x_j iff y_i < y_j).
We say that R containedin N^s is order invariant if and only if
(forall x,y in N^s)(x,y have the same order type implies (R(x) iff
R(y))).
For A containedin N^k, we write A' = N^k\A.
Let A,B containedin N^k and E containedin N. We say that A equals B
over E if and only if
(forall x in E^k)(x in A iff x in B).
For A containedin N^k and integers n, we define
A+n = {x+n: x in A}
where the addition is performed coordinatewise.
2. INDEPENDENT PROPOSITIONS.
First we start with some theorems.
THEOREM 2.1. For all k,p >= 1 and upwards R containedin N^pk x N^k,
some RA = A'. Furthermore, A is unique.
We are particularly interested in the following concrete specialization.
THEOREM 2.2. For all k,p >= 1 and order invariant upwards R
containedin N^pk x N^k, some RA = A'. Furthermore, A is unique and in
EXP.
The following follows immediately from Theorem 2.2.
THEOREM 2.3. For all k >= 1 and order invariant upwards R containedin
N^3k x N^k, there exists A containedin N^k such that R(A,A,RA) =
R(A,A,A').
THEOREM 2.4. The following is false, even for k = p = 1. For all k,p
>= 1 and order invariant upwards R containedin N^3k x N^k, there
exists A containedin N^k such that R(A,A,RA) = R(A,A,A') union A+1
PROPOSITION 2.5. For all k >= 1 and order invariant upwards R
containedin N^3k x N^k, some R((A,A,RA) equals R(A,A,A') union A+1
over some infinite set of nonnegative integers.
PROPOSITION 2.6. For all k >= 1 and order invariant upwards R
containedin N^3k x N^k, some R(A,A,RA) equals R(A,A,A') union A+1 over
some infinite geometric progression of nonnegative integers.
PROPOSITION 2.7. For all k >= 1 and order invariant upwards R
containedin N^3k x N^k, some R(A,A,RA) equals R(A,A,A') union A+1 over
an infinite tail of the powers of 2 by nonnegative integers.
PROPOSITION 2.8. For all k >= 1 and order invariant upwards R
containedin N^3k x N^k, some R(A,A,RA) equals R(A,A,A') union A+1 over
the powers of 2 by nonnegative integers greater than 8k^2.
Here is an explicitly Pi01 form of Proposition 2.8.
PROPOSITION 2.9. For all k,t >= 1 and order invariant upwards R
containedin [1,t]^3k x [1,t]^k, some R(A,A,RA) equals R(A,A,A') union A
+1 over the powers of 2 in [2^(8k^2),t].
Here order invariant and upwards are redefined for [1,t] instead of N.
We can also use [0,t] here instead of [1,t], and (2^(8k^2)] instead of
[2^(8k^2),t].
THEOREM 2.10. Theorems 2.1 - 2.4 are provable in RCA0. Propositions
2.5 - 2.9 are provably equivalent, in ACA, to the consistency of SMAH.
Hence they are provable in SMAH+ but not in any consistent subtheory
of SMAH.
Here SMAH = ZFC + {there exists a strongly k-Mahlo cardinal}_k. SMAH+
= ZFC + "for all k there exists a strongly k-Mahlo cardinal".
3. ALTERNATIVE: independence.
Let R containedin N^pk x N^k. We say that A is independent for R if
and only if RA intersect A is empty.
PROPOSITION 3.1. For all k >= 1, every order invariant upwards R
containedin N^3k x N^k has an independent A containedin N^k such that
RRA equals R(A') union A+1 over some infinite set of nonnegative
integers.
PROPOSITION 3.2. For all k >= 1, every order invariant upwards R
containedin N^3k x N^k has an independent A containedin N^k such that
RRA equals R(A') union A+1 over some infinite geometric progression of
nonnegative integers.
PROPOSITION 3.3. For all k >= 1, every order invariant upwards R
containedin N^3k x N^k has an independent A containedin N^k such that
RRA equals R(A') union A+1 over an infinite tail of the powers of 2 by
nonnegative integers.
PROPOSITION 3.4. For all k >= 1, every order invariant upwards R
containedin N^3k x N^k has an independent A containedin N^k such that
RRA equals R(A') union A+1 over the powers of 2 by nonnegative
integers greater than 8k^2.
PROPOSITION 3.5. For all k,t >= 1, every order invariant upwards R
containedin [1,t]^3k x [1,t]^k has an independent A containedin
[1,t]^k such that RRA equals R(A') union A+1 over the powers of 2 by
integers from [8k^2,t].
THEOREM 3.6. Propositions 3.1 - 3.4 are provably equivalent, in ACA,
to the consistency of SMAH. Hence they are provable in SMAH+ but not
in any consistent subtheory of SMAH.
4. ALTERNATIVE: foreignness.
Let A containedin N^k. We say that n is foreign to A if and only if n
is not a coordinate of any element of A.
PROPOSITION 4.1. For all k >= 1 and order invariant upwards R
containedin N^3k x N^k, some R(A,A,RA) equals R(A,A,A') over some
infinite set of nonnegative integers that are foreign to A+1.
PROPOSITION 4.2. For all k >= 1 and order invariant upwards R
containedin N^3k x N^k, some R(A,A,RA) equals R(A,A,A') over some
infinite geometric progression of nonnegative integers that are
foreign to A+1.
PROPOSITION 4.3. For all k >= 1 and order invariant upwards R
containedin N^3k x N^k, some R(A,A,RA) equals R(A,A,A') over an
infinite tail of powers of 2 by nonnegative integers, that are foreign
to A+1.
PROPOSITION 4.4. For all k,t >= 1 and order invariant upwards R
containedin [1,t]^3k x [1,t]^k, some R(A,A,RA) equals R(A,A,A') over
the at least floor(log(t)) - 8k^2 powers of 2 in [1,t] that are
foreign to A+1.
THEOREM 4.5. Propositions 4.1 - 4.4 are provably equivalent, in ACA,
to the consistency of SMAH. Hence they are provable in SMAH+ but not
in any consistent subtheory of SMAH.
5. ALTERNATIVE: independence, foreignness.
PROPOSITION 5.1. For all k >= 1, every order invariant upwards R
containedin N^3k x N^k has an independent A containedin N^k such that
RRA equals R(A') over some infinite set of nonnegative integers that
are foreign to A+1.
PROPOSITION 5.2. For all k >= 1, every order invariant upwards R
containedin N^3k x N^k has an independent A containedin N^k such that
RRA equals R(A') over some infinite geometric progression of
nonnegative integers that are foreign to A+1.
PROPOSITION 5.3. For all k >= 1, every order invariant upwards R
containedin N^3k x N^k has an independent A containedin N^k such that
RRA equals R(A') over an infinite tail of powers of 2, that are
foreign to A+1.
PROPOSITION 5.4. For all k,t >= 1, every order invariant upwards R
containedin [1,t]^3k x [1,t]^k has an independent A containedin
[1,t]^k such that RRA equals R(A') over the at least floor(log(t)) -
8k^2 powers of 2 in [1,t], that are foreign to A+1.
THEOREM 5.5. Propositions 4.1 - 4.4 are provably equivalent, in ACA,
to the consistency of SMAH. Hence they are provable in SMAH+ but not
in any consistent subtheory of SMAH.
6. EXPONENTIAL PRESBURGER.
The structure (N,+) is of course analyzed by Presburger, who gave a
decision procedure using elimination of quantifiers. More recently,
the structure (N,+,2^) has been analyzed by Semenov and others. See http://www.math.ohio-state.edu/%7Efriedman/pdf/AppB082707.pdf
Again, there is a decision procedure using elimination of
quantifiers.
A Presburger set is a subset of some N^k which is definable in (N,+).
An exponential Presburger set is a subset of some N^k which is
definable in (N,+,2^).
THEOREM 6.1. In Propositions 2.5 - 2.8, 3.1 - 3.4, 4.1 - 4.3, 5.1 -
5.3, we can require that A be an exponential Presburger set. In the
case of Propositions 2.7, 3.3, 4.3, 5.3, this results in a Pi01
sentence using the decision procedure for exponential Presburger
arithmetic (i.e., (N,+,2^)).
**********************************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 344th 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
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
343: Goedel's Second Revisited 2 6/1/09 9:21PM
Harvey Friedman
More information about the FOM
mailing list