In posting #269, Pi01,Pi00/digraphs 2/25/06 3:09AM,
http://www.cs.nyu.edu/pipermail/fom/2006-February/010056.html
I gave my mathematically cleanest, to date, Pi01 sentences independent of
ZFC:
PROPOSITION A. For all k,n,r >= 1, every order invariant upgraph G on
[1,n]^k has an independent set A such that every x!,y_1,...,y_r from V(G)\A
is G equivalent to some x!,z_1,...,z_r from GA\((8kr)!-1).
PROPOSITION B. For all n,r >= 1, every order invariant upgraph G on [1,n]^8
has an independent set A such that every x!,y_1,...,y_r from V(G)\A is G
equivalent to some x!,z_1,...,z_r from GA\((8r)!-1).
This also appears on my website http://www.math.ohio-state.edu/%7Efriedman/
under downloadable manuscripts, manuscript number 51.
It appears that I am now in a situation somewhat similar to where I was with
BRT before I made the following crucial move. This crucial move is also
proposed as something systematic in capital letters, in the middle of
posting http://www.cs.nyu.edu/pipermail/fom/2006-May/010506.html
Specifically, I will now step back and start to embed this or some closely
related independent Pi01 sentence, into a finite family of Pi01 sentences,
where
we can determine the truth values of all elements of the family using large
cardinals, but not in ZFC.
Also, as in the case of BRT,
we will endeavor to identify important features of the classification that
can be established using large cardinals, but not within ZFC.
In this way, we have our cake and eat it too: we will still find single
sentences that are provable using large cardinals but not within ZFC, that
are a conjunction of a Pi01 sentence and a Sigma01 sentence, and perhaps
even just a Pi01 sentence. The Sigma01 part should involve only reasonably
small integers, and therefore can be put into Pi00 form, and therefore, the
conjunction should be Pi01.
################################
Now in order to carry out this program, we will want to pick, out of all of
the Pi01 sentences we have constructed, the one that is most amenable to
this treatment.
It turns out not to be quite Propositions A and B above, but something else
more suited for this purpose.
This posting merely identifies the seemingly best Pi01 sentence for this
purpose, and starts with a first crude version of the results we are looking
for.
It is clear to me that this is going to be ultimately very satisfying, at
the same time very difficult, and subject to many many years of refinements.
#################################
Let us start from the beginning. Let R containedin [1,n]^k x [1,n]^k. We say
that R is strictly dominating if and only if
R(x,y) implies max(x) < max(y).
Also
RA = {y: (therexists x in A)(R(x,y)}.
A' = [1,n]^k\A.
Here is the basic mathematical theorem that initiates the development. It is
a special case of a well known theorem about dags in graph theory:
COMPLEMENTATION (relations). For all k,n >= 1 and strictly dominating R
containedin [1,n]^k x [1,n]^k, there exists A containedin [1,n]^k such that
RA = A'. Furthermore, A is unique.
We say that R containedin [1,n]^k x [1,n]^k is order invariant if and only
if the following holds. If (x,y) and (z,w) are order equivalent as elements
of [1,n]^2k, then R(x,y) iff R(z,w).
COMPLEMENTATION (invariant relations). For all k,n >= 1 and strictly
dominating order invariant R containedin [1,n]^k x [1,n]^k, there exists A
containedin [1,n]^k such that RA = A'. Furthermore, A is unique.
Let R contaiendin [1,n]^k x [1,n]^k. We say that A is an R antichain, or A
is an antichain for R, if and only if
i. A containedin [1,n]^k.
ii. for all x,y in A, not R(x,y).
Obviously RA = A' implies that A is an R antichain.
COMPLEMENTATION (first special form). For all k,n >= 1, every strictly
dominating order invariant R containedin [1,n]^k x [1,n]^k has an antichain
A such that every element of A' is equaled to an element of RA.
COMPLEMENTATION (second special form). For all k,n,p >= 1, every strictly
dominating order invariant R containedin [1,n]^k x [1,n]^k has an antichain
A such that every element of A'^p is equaled to an element of (RA)^p.
Here is the semiformal template.
TEMPLATE. For all k,n,p >= 1, every strictly dominating order invariant R
containedin [1,n]^k x [1,n]^k has an antichain A such that every element of
A'^p is RELATED to an element of (RA)^p.
More specifically, let Z+* be the space of all nonempty finite sequences
from Z+. Let W containedin Z+* x Z+* be length preserving. I.e.,
W(x,y) implies lth(x) = lth(y).
We define
TEMPLATE(W). For all k,n,p >= 1, every strictly dominating order invariant R
containedin [1,n]^k x [1,n]^k has an antichain A such that (forall x in
A'^p)(therexists y in (RA)^p)(W(x,y)).
So what kind of binary relations W on Z+* are we going to consider?
Consider one very important relation that is obviously crucial to this
enterprise. That is the notion of *order equivalence* or "having the same
order type*. This is defined as
x,y have the same order type iff
(forall 1 <= i,j <= lth(x))(x_i < x_j iff y_i < y_j).
This suggests that we move to the following more focused Template:
TEMPLATE(phi). For all k,n,p >= 1, every strictly dominating order invariant
R containedin [1,n]^k x [1,n]^k has an antichain A such that (forall x in
A'^p)(therexists y in (RA)^p)(forall 1 <= i,j <= kp)(phi(x_i,x_j,y_i,y_j)).
Here the parameter phi is to be some formula involving x_i,x_j,y_i,y_j of a
very simple kind.
Of course, this is a mere special case of using any finite number of indices
for the x,y. I.e., using
(forall 1 <= i1,...,is <= kp)(P(x_i1,...,x_is,y_i1,...,y_is))
but this is far beyond what we want to think of handling at this early
stage.
Now in all of our independent Pi01 sentences, we encounter special
combinatorial expressions, and this threatens to greatly impede our
progress. For this reason, we introduce a new parameter in the Template.
TEMPLATE(phi). Let n,t >> k,p >= 1. every strictly dominating order
invariant R containedin [1,n]^k x [1,n]^k has an antichain A such that
(forall x in A'^p)(therexists y in (RA)^p)(forall 1 <= i,j <=
kp)(phi(x_i,x_j,y_i,y_j,t)).
Here the parameter phi is to be some formula involving x_i,x_j,y_i,y_j,t of
a simple kind.
Note that Template(phi), for concrete phi, is a Pi02 sentence, not a Pi01
sentence. HOWEVER, we will be able to give an exponential type bound for the
>>, thus resulting in a Pi01 sentence. This simply amounts to placing the
burden of a slightly awkward exponential type expression at the end of the
development - the conversion of the Pi02 sentence to a Pi01 sentence -
rather than in the middle of the development, where it causes complications.
EXPOSITIONAL NOTE: It may be good to introduce the notion of a "bounded Pi02
sentence", which is of course, outright equivalent to a Pi01 sentence. END.
We now seek natural finite sets V of simple formulas phi in five variables
such that
i. Every Template(phi), phi in V, can be decided in ZFC with large
cardinals.
ii. Not every Template(phi), phi in V, can be decided in ZFC.
Of course, the more natural and more encompassing the V's are, the more
powerful the results are.
Now I wouldn't have taken us down this path if I hadn't already known that
for a quite simple phi in five variables,
*) Template(phi) is provably equivalent to Con(MAH) over EFA (exponential
function arithmetic).
Here is a phi for which *) holds.
phi(a,b,c,d,t) iff
i. a < b iff c < d.
ii. c+1 is not a power of t.
ii. if a is a power of t then a = c.
Here the powers of t are the integers 1,t,t^2,... .
THEOREM 1. For the above phi, Template(phi) is provably equivalent to
Con(MAH) over EFA.
Of course if we use
phi(a,b,c,d,t) iff
a = c and b = d
then Template(phi) is immediately equivalent to the above
Complementation (second special form).
#################################################
Let us look at our example of phi again. We can put it into the following
form.
i. a < b implies c < d.
ii. c < d implies a < b.
iii. c+1 a power of t implies c a power of t.
iv. a is a power of t implies a = c.
This suggests consideration of the following family of phi.
Let phi be a conjunction of implications between atomic formulas of the
forms
alpha < beta
alpha = beta
alpha is a power of t
where alpha,beta are among the 8 terms
a,b,c,d,a+1,b+1,c+1,d+1.
The following is immediate from Theorem 1.
THEOREM 2. There exists phi as above such that Template(phi) is provably
equivalent to Con(MAH) over EFA.
This language of conjunctions of implications is just simple enough for us
to be able to prove the following.
THEOREM 3. For every phi as above, Template(phi) is either provable in RCA0,
refutable in RCA0 with a short proof, or provably equivalent to Con(MAH) in
EFA.
Obviously we will want to extend the language considerably. For example,
instead of just considering conjunctions of implications, we can consider
all propositional combinations.
Beyond that, we can expand the collection of terms, first to perhaps
a,b,c,d,a+n,+n,c+n,d+n
where n is an integer, and then perhaps to allow addition of terms. We can
then first go back to conjunctions of implications, but then proceed again
to all propositional combinations.
Finally, we can attempt to add exponentiation to base t, and dispense with
the predicate "being a power of t". By a nontrivial argument, it seems that
we will retain an instance that is provably equivalent to Con(MAH) over EFA.
In any case, it now appears that this Pi01 program has been suitably
articulated and launched, and it is an instance of the Grand Conjecture
stated in http://www.cs.nyu.edu/pipermail/fom/2006-May/010506.html for Pi01
sentences, originating from a well known theorem from graph theory about
dags.
**********************************
I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 282nd 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
Harvey Friedman