[FOM] 257:FIT/more

[Harvey Friedman]

We have carried out some of the plans outlined in the previous posting #256,
at http://www.cs.nyu.edu/pipermail/fom/2005-November/009369.html

Recall the two templates discussed in #256:

TEMPLATE K1. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exists A containedin [1,n]k such that a
given subset of K1 holds conjunctively.

TEMPLATE K2. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exists A containedin [1,n]k such that a
given subset of K2 holds conjunctively.

Recall that K1 consists of the inclusions s containedin t, s containedin* t,
where s,t are any of the three expressions A, R<A'>, R<A'\(8k)!>. Here
containedin* means every k tuple of powers of (8k)!+1 lying in the left
side, also lies in the right side.

Recall that K2 consists of the inclusions s containedin t, s containedin* t,
where s,t are any of the three expressions RA, RR<A'>, RR<A'\(8k)!>.

Recall that the three expressions used for K1 are the three expressions
appearing in 

THEOREM 1.4. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets R<A'\(8k)!> containedin R<A'> containedin A contain the same k
tuples of powers of (8k)!+1.

Recall that the three expressions used for K2 are the three expressions
appearing in 

PROPOSITION A. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k
tuples of powers of (8k)!+1.

Recall from #256,

THEOREM. Every instance of Template K1 is provable or refutable in EFA
(exponential function arithmetic).

Recall that in the course of this analysis, we did discover a variant of
Theorem 1.4 that does not seem to follow formally from Theorem 1.4, or
formally imply Theorem 1.4:

THEOREM 1.5. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exists A containedin [1,n]k such that
the three sets A containedin R<A'\(8k)!> containedin R<A'> contain the same
k tuples of powers of (8k)!.

Recall that we also discovered an interesting counterexample.

THEOREM 1.6. The following is false. For all k,n >= 1 and strictly
dominating order invariant R containedin [1,n]3k x [1,n]k, there exists A
containedin [1,n]k such that R<A'\(8k)!> containedin A containedin R<A'> and
R<A'> containedin* R<A'\(8k)!).

We have now shown the following.

THEOREM. Every instance of Template K2 is
i. Provable in EFA.
ii. Refutable in EFA.
iii. Provably equivalent, over ACA, to Con(MAH).

Recall that we have discovered a variant of Proposition A that does not seem
to formally imply or be implied by Proposition A:

PROPOSITION A*. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RA containedin RR<A'\(8k)!> containedin RR<A'> contain the same k
tuples of powers of (8k)!+1.

Proposition A* is also provably equivalent, over ACA, to Con(MAH).

The additional projects from #256 are much more ambitious.

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

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

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

Harvey Friedman