FOM: 92:Thin Set Theorem

Harvey Friedman friedman at
Sun Jun 25 05:42:57 EDT 2000

CORRECTION: I misspoke in posting 88:Boolean Relation Theory, and said

"In fact, it (the thin set theorem) is provably equivalent over RCA_0 to
the classical infinite Ramsey theorem."

I never meant to claim this result.


This regardsthe thin set theorem and some variants. The thin set theorem is
a principal motivator for Boolean relation theory.


Let N be the set of all nonnegative integers. Let F be a multivariate
function from N into N (i.e., there exists k such that F"N^k into N). For A
containedin N, we write FA for F[A^k].

THEOREM (thin set theorem). Let F be a multivariate function from N into N.
There exists an infinite A containedin N such that FA not= N.

We write this theorem as TS. We write TS(k) for TS where F is required to
have k variables.

Our original proof of TS using the classical infinite Ramsey theorem showed
that for all k >= 1, TS(k) is provable in ACA_0. It also showed that TS is
provable in ACA_0' = ACA_0 + "for all x containedin N and k >= 1, the k-th
Turing jump of x exists." Also, for each k, TS(k) is provable in ACA_0.

Jeff Remmel recently gave a more direct proof of TS. From this proof one
immediately sees that TS(2) is provable in RCA_0 + the infinite Ramsey
theorem for pairs with 2 colors. (However, this is not the first proof of
this result. See the triple authored paper below. Also, there is another
direct proof of the thin set theorem in that triple paper).


H. Friedman, S. Simpson, Issues and Problems in Reverse Mathematics, to
appear in the Proceedings of the Boulder Conference

I sketched my proof that TS is not provable in ACA_0. In

H. Friedman, Pairs, e-mail to Cholak, Hirst, 4:08AM 6/14/00

I sketched my proof that TS(2) is not provable in WKL_0.

My original proof of TS passed through my related - but seemingly stronger
- free set theorem. This formed the basis of the preprint

Peter Cholak, Mariagnese Giusto, Jeffry L. HIrst, Free Sets and Reverse
Mathematics, 6/14/00.

There are a number of interesting new results in this triple paper,
including that Ramsey's theorem for pairs and two colors suffices to prove
the free set theorem for pairs.

>From the point of view of reverse mathematics, here are the principal open
problems with regard to TS and TS(k).

1. Does RCA_0 prove that TS and RT equivalent? Here RT is the classical
infinite Ramsey theorem. I proved the reverse implication. Does TS prove
even ACA_0?

2. For which k are TS(k) and ACA_0 equivalent? I proved the reverse
implication for all k, and that TS(1) is provable in RCA_0. Also for k = 2,
this is also false, since TS(2) follows from RT(2,2), which does not imply
ACA_0 - see Cholak, Giusto, Hirst above, and the Cholak, Jockusch, Slaman
paper. Are TS(3) and ACA_0 equivalent?


My proof that TS is not provable in ACA_0 and TS(2) is not provable in
WKL_0 actually works for substantial weakenings of TS and TS(2).

Let N^k< be the set of all strictly increasing elements of N^k. Let F:N^k<
into N. We say that F is strictly regressive if and only if

i) F(0,...,0) = 0;
ii) for all x in N^k< that is not (0,...,0), F(x) < min(x).

THEOREM 2.1. (VWTS = very weak thin set theorem.) Let F be a strictly
regressive multivariate function from N into N. There exists an infinite A
containedin N such that FA not= N.

Let VWTS(k) be VWTS for arity k.

THEOREM 2.2. VWTS is not provable in ACA_0. VWTS(2) is not provable in
WKL_0. Each VWTS(k) is provable in ACA_0.


We strengthen the conclusion from FA not= N to FA is itself thin.

THEOREM. Let F be a multivariate function from N into N, A containedin N be
infinite, h:N into N. There exists an infinite B containedin A such that FA
is finite or the enumeration function for FA eventually dominates h.

We don't know whether the stronger Theorem 3.1 implies Ramsey's theorem, or
even ACA_0.


Let dot be a binary function from N into N. At first, we place no
conditions on dot. Let A containedin N. We define dot^k(A) as the set of
elements of N that can be written as a term in dot where there are at most
k occurrences of variables in the term, each variable representing an
element of A. Thus dot^1(A) = A.

Here is an obvious consequence of the thin set theorem.

THEOREM 4.1. Let dot:N^2 into N and k >= 1. There exists infinite A
containedin N such that dot^k(N) not= N.

We can prove that Theorem 4.1 is equivalent to the thin set theorem.

However, what if we place conditions on the dot? E.g., that it is
associate, or that it is a group operation, etcetera? What is the status of
Theorem 4.1?


This is the 92nd 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
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
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
53:Free Sets/Reverse Math  7/19/99  2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry  8/27/99  3:01PM
57:Fixpoints/Summation/Large Cardinals  9/10/99  3:47AM
57':Restatement  9/11/99  7:06AM
58:Program A/Conjectures  9/12/99  1:03AM
59:Restricted summation:Pi-0-1 sentences  9/17/99  10:41AM
60:Program A/Results  9/17/99  1:32PM
61:Finitist proofs of conservation  9/29/99  11:52AM
62:Approximate fixed points revisited  10/11/99  1:35AM
63:Disjoint Covers/Large Cardinals  10/11/99  1:36AM
64:Finite Posets/Large Cardinals  10/11/99  1:37AM
65:Simplicity of Axioms/Conjectures  10/19/99  9:54AM
66:PA/an approach  10/21/99  8:02PM
67:Nested Min Recursion/Large Cardinals  10/25/99  8:00AM
68:Bad to Worse/Conjectures  10/28/99  10:00PM
69:Baby Real Analysis  11/1/99  6:59AM
70:Efficient Formulas and Schemes  11/1/99  1:46PM
71:Ackerman/Algebraic Geometry/1  12/10/99  1:52PM
72:New finite forms/large cardinals  12/12/99  6:11AM
73:Hilbert's program wide open?  12/20/99  8:28PM
74:Reverse arithmetic beginnings  12/22/99  8:33AM
75:Finite Reverse Mathematics  12/28/99  1:21PM
76: Finite set theories  12/28/99  1:28PM
77:Missing axiom/atonement  1/4/00  3:51PM
78:Qadratic Axioms/Literature Conjectures  1/7/00  11:51AM
79:Axioms for geometry  1/10/00  12:08PM
80.Boolean Relation Theory  3/10/00  9:41AM
81:Finite Distribution  3/13/00  1:44AM
82:Simplified Boolean Relation Theory  3/15/00  9:23AM
83:Tame Boolean Relation Theory  3/20/00  2:19AM
84:BRT/First Major Classification  3/27/00  4:04AM
85:General Framework/BRT   3/29/00  12:58AM
86:Invariant Subspace Problem/fA not= U  3/29/00  9:37AM
87:Programs in Naturalism  5/15/00  2:57AM
88:Boolean Relation Theory  6/8/00  10:40AM
89:Model Theoretic Interpretations of Set Theory  6/14/00 10:28AM
90:Two Universes  6/23/00  1:34PM
91:Counting Theorems  6/24/00  8:22PM

More information about the FOM mailing list