[FOM] 316: Shift Theorems

Thu Jan 24 12:36:43 EST 2008

SHIFT THEOREMS
Harvey M. Friedman
Ohio State University
friedman at math.ohio-state.edu
January 24, 2008

These bring PA incompleteness to a new level.

1. INFINITE FORMS.

We use [1,inf) for the set of all positive integers. We use [1,n] for the
set of all integers from 1 through n. For x,y in [1,inf)^k, we write x
<= y for 

for all i, x_i <= y_i.

THEOREM A. For all k >= 1 and f:[1,inf)^k into [1,inf)^2, there exist
distinct x_1,...,x_k+1 such that f(x_1,...,x_k) <= f(x_2,...,x_k+1).

THEOREM B. For all k >= 1 and f:[1,inf)^k into [1,inf), there exist distinct
x_1,...,x_k+2 such that f(x_1,...,x_k) <= f(x_2,...,x_k+1) <=
f(x_3,...,x_k+2).

THEOREM C. For all k >= 1 and f:[1,inf)^k into [1,inf), there exist distinct
x_1,...,x_k+1 such that f(x_2,...,x_k+1)-f(x_1,...,x_k) in {0,2,4,...}.

Here are three stronger forms.

THEOREM D. For all k,r >= 1 and f;[1,inf)^k into [1,inf)^r, there exist
distinct x_1,...,x_k+1 such that f(x_1,...,x_k) <= f(x_2,...,x_k+1).

THEOREM E. For all k,r,t >= 1 and f:[1,inf)^k into [1,inf)^r, there exist
distinct x_1,...,x_k+t-1 such that f(x_1,...,x_k) <= ... <=
f(x_t,...,x_k+t-1).

THEOREM F. For all k,r,t >= 1 and f:[1,inf)^k into [1,inf)^r, there exist
distinct x_1,...,x_k+1 such that f(x_2,...,x_k+1)-f(x_1,...,x_k) in
{0,t,2t,...}^r..

THEOREM 1.1. RCA_0 proves that each of Theorems A-F is provably equivalent
to "epsilon naught is well ordered". In particular, none of Theorems A-F is
provable in ACA_0. They are all provable in ACA_0 + "for all n,x, the n-th
Turing jump of x exists".

2. LIMITED FORMS. 

We say that f:[1,inf)^k into [1,inf)^r is limited if and only if for all x
in [1,inf)^k, max(f(x)) <= max(x).

Theorems A-F have limited forms A'-F', where we insert that f must be
limited. 

THEOREM 2.1. RCA_0 proves that each of Theorems A'-F' is provably equivalent
to the 1-consistency of PA. In particular, none of Theorems A'-F' is
provable in ACA_0. They are all provable in RCA_0 + 1-CON(PA).

3. FINITE FORMS.

THEOREM A*. For all n >> k >= 1 and limited f:[1,n]^k into [1,n]^2, there
exist distinct x_1,...,x_k+1 such that f(x_1,...,x_k) <= f(x_2,...,x_k+1).

THEOREM B*. For all n >> k >= 1 and limited f:[1,n]^k into [1,n], there
exist distinct x_1,...,x_k+2 such that f(x_1,...,x_k) <= f(x_2,...,x_k+1) <=
f(x_3,...,x_k+2).

THEOREM C*. For all n >> k >= 1 and limited f:[1,n]^k into [1,n], there
exist distinct x_1,...,x_k+1 such that f(x_2,...,x_k+1)-f(x_1,...,x_k) in
{0,2,...,2n}.

THEOREM D*. For all n >> k,r >= 1 and limited f;[1,n]^k into [1,n]^r, there
exist distinct x_1,...,x_k+1 such that f(x_1,...,x_k) <= f(x_2,...,x_k+1).

THEOREM E*. For all k,r,t >= 1 and limited f:[1,n]^k into [1,n]^r, there
exist distinct x_1,...,x_k+t-1 such that f(x_1,...,x_k) <= ... <=
f(x_t,...,x_k+t-1).

THEOREM F*. For all n >> k,r,t >= 1 and limited f:[1,n]^k into [1,n]^r,
there exist distinct x_1,...,x_k+1 such that f(x_2,...,x_k+1)-f(x_1,...,x_k)
in {0,t,2t,...,nt}^r.

THEOREM 3.1. EFA proves that each of Theorems A*-F* is provably equivalent
to the 1-consistency of PA. In particular, none of Theorems A*-F* is
provable in PA. They are all provable in EFA + 1-CON(PA).

**********************************

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

Harvey Friedman