FOM: 53:Free Sets/Reverse Math

[Harvey Friedman]

This is the 53rd in a series of self contained postings to fom covering a
wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM
5:Constructions  11/15/97  5:24PM
6:Undefinability/Nonstandard Models   11/16/97  12:04AM
7.Undefinability/Nonstandard Models   11/17/97  12:31AM
8.Schemes 11/17/97    12:30AM
9:Nonstandard Arithmetic 11/18/97  11:53AM
10:Pathology   12/8/97   12:37AM
11:F.O.M. & Math Logic  12/14/97 5:47AM
12:Finite trees/large cardinals  3/11/98  11:36AM
13:Min recursion/Provably recursive functions  3/20/98  4:45AM
14:New characterizations of the provable ordinals  4/8/98  2:09AM
14':Errata  4/8/98  9:48AM
15:Structural Independence results and provable ordinals  4/16/98
10:53PM
16:Logical Equations, etc.  4/17/98  1:25PM
16':Errata  4/28/98  10:28AM
17:Very Strong Borel statements  4/26/98  8:06PM
18:Binary Functions and Large Cardinals  4/30/98  12:03PM
19:Long Sequences  7/31/98  9:42AM
20:Proof Theoretic Degrees  8/2/98  9:37PM
21:Long Sequences/Update  10/13/98  3:18AM
22:Finite Trees/Impredicativity  10/20/98  10:13AM
23:Q-Systems and Proof Theoretic Ordinals  11/6/98  3:01AM
24:Predicatively Unfeasible Integers  11/10/98  10:44PM
25:Long Walks  11/16/98  7:05AM
26:Optimized functions/Large Cardinals  1/13/99  12:53PM
27:Finite Trees/Impredicativity:Sketches  1/13/99  12:54PM
28:Optimized Functions/Large Cardinals:more  1/27/99  4:37AM
28':Restatement  1/28/99  5:49AM
29:Large Cardinals/where are we? I  2/22/99  6:11AM
30:Large Cardinals/where are we? II  2/23/99  6:15AM
31:First Free Sets/Large Cardinals  2/27/99  1:43AM
32:Greedy Constructions/Large Cardinals  3/2/99  11:21PM
33:A Variant  3/4/99  1:52PM
34:Walks in N^k  3/7/99  1:43PM
35:Special AE Sentences  3/18/99  4:56AM
35':Restatement  3/21/99  2:20PM
36:Adjacent Ramsey Theory  3/23/99  1:00AM
37:Adjacent Ramsey Theory/more  5:45AM  3/25/99
38:Existential Properties of Numerical Functions  3/26/99  2:21PM
39:Large Cardinals/synthesis  4/7/99  11:43AM
40:Enormous Integers in Algebraic Geometry  5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees  5/25/99  5:11PM
43:More Enormous Integers/AlgGeom  5/25/99  6:00PM
44:Indiscernible Primes  5/27/99  12:53 PM
45:Result #1/Program A  7/14/99  11:07AM
46:Tamism  7/14/99  11:25AM
47:Subalgebras/Reverse Math  7/14/99  11:36AM
48:Continuous Embeddings/Reverse Mathematics  7/15/99  12:24PM
49:Ulm Theory/Reverse Mathematics  7/17/99  3:21PM D.A. Martin is the
originator of cone theorems involving Turing degrees.
50:Enormous Integers/Number Theory  7/17/99  11:39PN
51:Enormous Integers/Plane Geometry  7/18/99  3:16PM
52:Cardinals and Cones  7/18/99  3:33PM

This concerns the reverse mathematics of the well known free set theorem
for omega.

Let F:N^k into N. An F-free set is an A containedin N such that for all
x1,...,xk in N, if F(x1,...,xk) is in A then F(x1,...,xk) is among
x1,...,xk.

By way of background, Ramsey's theorem (RT) for arbitrary tuples is
equivalent to ACA0' = ACA0 + (forall n)(forall x)(the n-th Turing jump of x
exists) over RCA0. And Ramsey's theorem for 3 tuples (RT(3)) or any
specific arity >= 3 is equivalent to ACA0 over RCA0 (see Simpson's book).
The case of 2-tuples (RT(2)) is delicate and is discussed in detail in
Cholak, Jockusch, Slaman, On the strength of Rmasey's theorem for pairs, to
appear, with plenty of open questions.

THEOREM 1. (Well known). For all F:N^k into N there is an infinite F-free set.

Write this as FS (free set). FS(k) is FS for k-ary functions.

What is the reverse mathematics status of Theorem 1?

THEOREM 2. RCA0 proves FS(1). RCA0 + RT proves FS. For any specific k >= 1,
ACA0 proves FS(k).

THEOREM 3. FS is not provable in ACA0. FS is true in the arithmetical sets.

Theorem 3 uses the following fact about ACA0: if ACA0 proves a sentence
(forall x containedin omega)(therexists y containedin
omega)(arithmetical(x,y)), then there exists an arithmetical operator F
(defined without parameters) such that ACA0 proves (forall x containedin
omega)(arithmetical(x,F(x))).

THEOREM 4. FS(2) fails in the recursive sets. In fact, FS(2) fails in some
omega model of WKL0, and so is not provable in WKL = WKL0 + full induction.

SOME QUESTIONS:

1. Does FS imply ACA0?
2. Does FS(2) imply ACA0?
3. Does FS(2) imply WKL0?
4. Does FS(2) imply RT(2)?
5. Does RT(2) imply FS(2)?