[FOM] 249:Rich Antichains and Large Cardinals
Harvey Friedman
friedman at math.ohio-state.edu
Thu Jun 9 14:46:52 EDT 2005
RICH ANTICHAINS AND LARGE CARDINALS
Harvey M. Friedman
Ohio State University
http://www.math.ohio-state.edu/%7Efriedman/
June 9, 2005
In section 2, we present a statement asserting that every suitable relation
on Qk has an antichain containing certain associated sets. Here Q is the set
of all rational numbers. See Proposition 2.1 below.
We have shown that this rich antichain statement is provably equivalent to
the consistency of ZFC augmented with certain large cardinal axioms.
Thus the rich antichain statement is provably equivalent to a Pi01 sentence.
Evidently, the rich antichain statement as presented asserts the existence
of a subset of Qk, which is generally infinite. Thus the rich antichain
theorem as stated is far from being explicitly Pi01.
We can assert that the rich antichain is arithmetical, or even Delta02. This
will result in a statement somewhere in the arithmetical hierarchy. However,
we will still fall far short of giving a mathematically natural arithmetical
sentence whose proof requires large cardinals.
We have discovered a way of providing a closely associated multiple form
which is explicitly Pi02. Instead of using generally infinite antichains, we
use finite length towers of finite antichains. This results in a clear "rich
finite tower antichain statement", since all of the notions used in the
original rich antichain statement have obvious multiple forms.
This process is too crude, and results in a refutable statement. However, it
is easily repaired using the basic notions of forward and backward shift.
This results in an explicitly Pi02 rich finite tower antichain statement,
which is equivalent to the original rich antichain statement.
Some straightforward estimates are given to bound the conclusion, so that
the rich finite tower antichain statement becomes explicitly Pi01, and also
equivalent to the original rich antichain statement.
There is some general applicability of this method of obtaining finite
forms. We provisionally call this "the method of sequential shifts". We will
not discuss this method in any generality here.
###1. Field, forward image, antichain, order invariance, strict domination,
+'1.###
We use N for the set of all nonnegative integers and Q for the set of all
rational numbers.
For A containedin Qk, we write fld(A) for the set of all coordinates of
elements of A.
Let R containedin Qk x Qk. We consider k to be recoverable from R even if R
is empty.
For A containedin Qk, we define R[A] = {y in Qk: (therexists x in
Qk)(R(x,y))}.
We say that A is an antichain for R if and only if A containedin Qk and for
all x,y in A, not R(x,y).
We say that x,y in Qr have the same order type if and only if
for all 1 <= i,j <= r, xi < yi iff xj < yj.
We say that B containedin Qr is order invariant if and only if for all x,y
in Qr of the same order type, x in B iff y in B.
We say that R containedin Qk x Qk is order invariant if and only if the
graph of R is an order invariant subset of Q2k.
We say that R containedin Qk x Qk is strictly dominating if and only if for
all x,y, if R(x,y) then max(x) < max(y).
For x in Qk, we define x+'1 in Qk to be the result of replacing each
nonnegative coordinate of y of x by y+1.
For A containedin Qk, we define A+'1 = {x+'1: x in A}.
###2. Rich antichain statement.###
Let SUB = ZFC + {there exists an n-subtle cardinal}n.
PROPOSITION 2.1. For all k >= 1, every strictly dominating order invariant R
containedin Qk x Qk has an antichain A containing A+'1 and (fld(A) union
{0})k\R[A].
THEOREM 2.2. Proposition 2.1 is provably equivalent, over WKL0, to Con(SUB).
What happens if we fix k >= 1 in Proposition 2.1?
THEOREM 2.3. There is a fixed k >= 1 such that Proposition 2.1 for k is
provably equivalent, over WKL0, to Con(SUB).
How small can k be chosen for Theorem 2.3? We don't have the time to get
into this interesting detailed issue right now, but k = 3 looks like the
proper challenge.
###3. Finite set sequences, finite tower antichains.
Note that Proposition 2.1 is based on three operators on P(Qk) = the power
set of Qk. Specifically, the operators
F(A) = A+'1.
G(A) = fld(A) union {0})k.
H(A) = R[A].
Let P(Qk)* be the set of all finite sequences of elements of P(Qk). The
empty sequence is allowed.
Any operator on P(Qk) extends canonically to an operator on P(Qk)* by
applying the operator termwise.
Furthermore, any binary operator on P(Qk) and any binary relation on P(Qk)
also extends canonically to P(Qk)* in the following way.
H((A1,...,Ar),(B1,...,Bs)) = (H(A1,B1),...,H(Ap,Bp))
S((A1,...,Ar),(B1,...,Bs)) iff S(A1,B1) and ... and S(Ap,Bp)
where p = min(r,s).
In particular, we will use the binary operator \ and the binary relation of
containment.
Let R containedin Qk x Qk. A finite tower antichain for R consists of a
finite sequence of finite antichains for R, forming a chain under inclusion.
We have the following obvious naïve finite multiple form of Proposition 2.1.
PROPOSITION 3.1. For all k >= 1, every strictly dominating order invariant R
containedin Qk x Qk has a finite tower antichain A of length k containing
A+'1 and (fld(A) union {0})k\R[A].
Proposition 3.1 is a natural finite form of Proposition 2.1, and is
explicitly Pi02. Unfortunately, Proposition 3.1 is refutable.
In the next section, we remedy this situation using forward and backward
shifts.
###4. Rich finite tower antichain statement.###
Let A lie in P(Qk)*, and have nonzero length. Write A = A1,...,At, t >= 1.
We define the forward shift of A by
fsh(A) = (emptyset,A1,...,At-1).
We define the backward shift of A by
bsh(A) = (A2,...,At).
PROPOSITION 4.1. For all k >= 1, every strictly dominating order invariant R
containedin Qk x Qk has a finite tower antichain A of length k containing
fsh(A)+'1 and (fld(A) union {0})k\R[bsh(A)].
We now introduce a new parameter r.
PROPOSITION 4.2. For all k,r >= 1, every strictly dominating order invariant
R containedin Qk x Qk has a finite tower antichain A of length r containing
fsh(A)+'1 and (fld(A) union {0})k\R[bsh(A)].
Note that Propositions 4.1 and 4.2 are explicitly Pi02. We can place a bound
on the conclusion as follows.
PROPOSITION 4.3. For all k >= 1, every strictly dominating order invariant R
containedin Qk x Qk has a finite tower antichain A of length k containing
fsh(A)+'1 and (fld(A) union {0})k\R[bsh(A)], and using numerators and
denominators of magnitude at most (8k)!!!.
PROPOSITION 4.4. For all k,r >= 1, every strictly dominating order invariant
R containedin Qk x Qk has a finite tower antichain A of length r containing
fsh(A)+'1 and (fld(A) union {0})k\R[bsh(A)], and using numerators and
denominators of magnitude at most (8kr)!!!.
Obviously Propositions 4.3 and 4.4 are explicitly Pi01.
THEOREM 4.5. Propositions 4.1 - 4.4 are provably equivalent, over EFA, to
Con(SUB).
Here EFA is exponential function arithmetic, also known as ISigma0(exp).
Also (8k)!!! and (8kr)!!! are very crude upper bounds that are safe.
What happens if we fix k >= 1 in Propositions 4.2 and 4.4?
THEOREM 4.6. There is a fixed k >= 1 such that Propositions 4.2 and 4.4, for
k, are provably equivalent, over EFA, to Con(SUB).
What happens if we fix r >= 1 in Propositions 4.2, 4.4?
THEOREM 4.7. There is a fixed r >= 1 such that Propositions 4.2 and 4.4, for
k, are provably equivalent, over EFA, to Con(SUB).
How small can k be chosen for Theorem 4.6? We don't have the time to get
into this interesting detailed issue right now, but k = 3 looks like the
proper challenge.
How small can r be chosen for Theorem 4.7? We don't have the time to get
into this interesting detailed issue right now, but r = 4 looks like the
proper challenge.
*************************************
I use www.math.ohio-state.edu/~friedman/ for downloadable manuscripts.
This is the 249th 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-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:
150:Finite obstruction/statistics 8:55AM 6/1/02
151:Finite forms by bounding 4:35AM 6/5/02
152:sin 10:35PM 6/8/02
153:Large cardinals as general algebra 1:21PM 6/17/02
154:Orderings on theories 5:28AM 6/25/02
155:A way out 8/13/02 6:56PM
156:Societies 8/13/02 6:56PM
157:Finite Societies 8/13/02 6:56PM
158:Sentential Reflection 3/31/03 12:17AM
159.Elemental Sentential Reflection 3/31/03 12:17AM
160.Similar Subclasses 3/31/03 12:17AM
161:Restrictions and Extensions 3/31/03 12:18AM
162:Two Quantifier Blocks 3/31/03 12:28PM
163:Ouch! 4/20/03 3:08AM
164:Foundations with (almost) no axioms 4/22/03 5:31PM
165:Incompleteness Reformulated 4/29/03 1:42PM
166:Clean Godel Incompleteness 5/6/03 11:06AM
167:Incompleteness Reformulated/More 5/6/03 11:57AM
168:Incompleteness Reformulated/Again 5/8/03 12:30PM
169:New PA Independence 5:11PM 8:35PM
170:New Borel Independence 5/18/03 11:53PM
171:Coordinate Free Borel Statements 5/22/03 2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals 5/34/03 1:55AM
173:Borel/DST/PD 5/25/03 2:11AM
174:Directly Honest Second Incompleteness 6/3/03 1:39PM
175:Maximal Principle/Hilbert's Program 6/8/03 11:59PM
176:Count Arithmetic 6/10/03 8:54AM
177:Strict Reverse Mathematics 1 6/10/03 8:27PM
178:Diophantine Shift Sequences 6/14/03 6:34PM
179:Polynomial Shift Sequences/Correction 6/15/03 2:24PM
180:Provable Functions of PA 6/16/03 12:42AM
181:Strict Reverse Mathematics 2:06/19/03 2:06AM
182:Ideas in Proof Checking 1 6/21/03 10:50PM
183:Ideas in Proof Checking 2 6/22/03 5:48PM
184:Ideas in Proof Checking 3 6/23/03 5:58PM
185:Ideas in Proof Checking 4 6/25/03 3:25AM
186:Grand Unification 1 7/2/03 10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03 4:43AM
189:Some Model theoretic Pi-0-1 statements 9/25/03 11:04AM
190:Diagrammatic BRT 10/6/03 8:36PM
191:Boolean Roots 10/7/03 11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement 11/2/03 4:42PM
194:PL Statement/clarification 11/2/03 8:10PM
195:The axiom of choice 11/3/03 1:11PM
196:Quantifier complexity in set theory 11/6/03 3:18AM
197:PL and primes 11/12/03 7:46AM
198:Strong Thematic Propositions 12/18/03 10:54AM
199:Radical Polynomial Behavior Theorems
200:Advances in Sentential Reflection 12/22/03 11:17PM
201:Algebraic Treatment of First Order Notions 1/11/04 11:26PM
202:Proof(?) of Church's Thesis 1/12/04 2:41PM
203:Proof(?) of Church's Thesis - Restatement 1/13/04 12:23AM
204:Finite Extrapolation 1/18/04 8:18AM
205:First Order Extremal Clauses 1/18/04 2:25PM
206:On foundations of special relativistic kinematics 1 1/21/04 5:50PM
207:On foundations of special relativistic kinematics 2 1/26/04 12:18AM
208:On foundations of special relativistic kinematics 3 1/26/04 12:19AAM
209:Faithful Representation in Set Theory with Atoms 1/31/04 7:18AM
210:Coding in Reverse Mathematics 1 2/2/04 12:47AM
211:Coding in Reverse Mathematics 2 2/4/04 10:52AM
212:On foundations of special relativistic kinematics 4 2/7/04 6:28PM
213:On foundations of special relativistic kinematics 5 2/8/04 9:33PM
214:On foundations of special relativistic kinematics 6 2/14/04 9:43AM
215:Special Relativity Corrections 2/24/04 8:13PM
216:New Pi01 statements 6/6/04 6:33PM
217:New new Pi01 statements 6/13/04 9:59PM
218:Unexpected Pi01 statements 6/13/04 9:40PM
219:Typos in Unexpected Pi01 statements 6/15/04 1:38AM
220:Brand New Corrected Pi01 Statements 9/18/04 4:32AM
221:Pi01 Statements/getting it right 10/7/04 5:56PM
222:Statements/getting it right again 10/9/04 1:32AM
223:Better Pi01 Independence 11/2/04 11:15AM
224:Prettier Pi01 Independence 11/7/04 8:11PM
225:Better Pi01 Independence 11/9/04 10:47AM
226:Nicer Pi01 Independence 11/10/04 10:43AM
227:Progress in Pi01 Independence 11/11/04 11:22PM
228:Further Progress in Pi01 Independence 11/12/04 2:49AM
229:More Progress in Pi01 Independence 11/13/04 10:41PM
230:Piecewise Linear Pi01 Independence 11/14/04 9:38PM
231:More Piecewise Linear Pi01 Independence 11/15/04 11:18PM
232:More Piecewise Linear Pi01 Independence/correction 11/16/04 8:57AM
233:Neatening Piecewise Linear Pi01 Independence 11/17/04 12:22AM
234:Affine Pi01 Independence 11/20/04 9:54PM
235:Neatening Affine Pi01 Independence 11/28/04 6:08PM
236:Pi01 Independence/Huge Cardinals 12/2/04 3:49PM
237:More Neatening Pi01 Affine Independence 12/6/04 12:56AM
238:Pi01 Independence/Large Large Cardinals/Correction 12/7/04 10:31PM
239:Pi01 Update 12/11/04 1:12PM
240:2nd Pi01 Update 12/13/04 2:49AM
241:3rd Pi01 Update 12/13/04 4:08AM
242:4th Pi01 Update 12/18/04 9:47PM
243:Inexplicit Pi01/Ordinals of Set Theories 12/19/04 11:48PM
244:LUB Systems 2/26/05 8PM
245:Relational System Theory 1 5/16/05 12:24PM
246:Relational System Theory 2 5/15/05 9:57PM
247:Inevitability of Logical Strength 5/15/05 9:57PM
248:Relational System Theory 2/restated 5/26/05 1:46AM
Harvey Friedman
More information about the FOM
mailing list