[FOM] 256:NAME:finite inclusion theory

[Harvey Friedman]

We have now tentatively named this approach to Pi01 sentences as

FINITE INCLUSION THEORY

or FIT as a nickname. So now we have BRT and FIT.

In this posting we want to begin to establish FIT as a systematic subject.

Right now, FIT concerns

the satisfiability of finite systems of inclusions and restricted inclusions
between forward images of multidimensional sets under order invariant
relations, in the context of finite initial segments of the positive
integers. 

At this point we will refrain from going into any greater generality. We
will remain very specific.

We will start slowly, even below the radar screen - we will not encounter
any independent statements in the claims made in this posting. We will
continue the development in a later posting, at and above the radar screen.

Recall Theorem 1.4, copied from
http://www.cs.nyu.edu/pipermail/fom/2005-November/009324.html

THEOREM 1.4. 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 R<A'\(8k)!> containedin R<A'> containedin A contain the same
k tuples of powers of (8k)!.

We begin our classification theory by considering all three expressions
appearing in Theorem 1.4.

A
R<A'>
R<A'\(8k)!>

Theorem 1.4 uses these two inclusion statements.

s containedin t
s containedin* t

where s,t are among the above five expressions. Here s ontainedin* t means
that every k tuple of powers of (8k)! lying in s, also lies in t.

Thus we can rewrite Theorem 1.4 as follows.

THEOREM 1.4'. 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
1. R<A'> containedin A.
2. A containedin* R<A'\(8k)!>.

Note how the conclusion of Theorem 1.4 reduces to only two inclusions. This
is because 

R<A'\(8k)!> containedin R<A'> containedin A
R<A'\(8k)!> =* R<A'> =* A

follow trivially from 1,2 in Theorem 1.4'.

Let K1 be the set of all inclusion statements of the above form. K1 has 18
elements, six of which are trivial because their left and right sides are
identical. So there are really 12 elements of K1 that need to be considered.
 
We now wish to classify (i.e., determine the truth or falsity of) all
statements of the following form.

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.

There are 2^12 subsets of K1 that need to be considered, which is 4096.

We have been able to carry out this classification; i.e., determine the
truth values of all instances of Template K1.

Now what exactly does this mean?

For one thing, we can actually exhibit this table, since 4096 is not too
big. 

But we have a methodology for determining these truth values without
exhibiting the entire table. Instead, we use a tree like methodology which
does exhibit all of the maximal subsets of K1 for which Template K1 holds.

The fundamental finding that can be stated without exhibiting anything is:

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

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)!.

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)!).

The plan is to do the same investigation associated with Proposition A,
copied from http://www.cs.nyu.edu/pipermail/fom/2005-November/009324.html.

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.

We analogously considering all three expressions appearing in Proposition A.

RA
RR<A'>
RR<A'\(8k)!>

Proposition A uses these two inclusion statements.

s containedin t
s containedin* t

where s,t are among the above five expressions. Here s ontainedin* t means
that every k tuple of powers of (8k)! lying in s, also lies in t.

Thus we can rewrite Proposition A as follows.

PROPOSITION A'. 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
1. RR<A'> containedin RA.
2. RA containedin* RR<A'\(8k)!>.

Note how the conclusion of Theorem 1.4 reduces to only two inclusions. This
is because 

RR<A'\(8k)!> containedin RR<A'> containedin RA
RR<A'\(8k)!> =* RR<A'> =* RA

follow trivially from 1,2 in Proposition A'.

Let K2 be the set of all inclusion statements of the above form. K2 has 18
elements, six of which are trivial because their left and right sides are
identical. So there are really 12 elements of K2 that need to be considered.
 
We now wish to classify (i.e., determine the truth or falsity of) all
statements of the following form.

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.

There are 2^12 subsets of K2 that need to be considered, which is 4096.

Presumably the result should be that every instance of Template K2 is either

i. Provable in EFA.
ii. Refutable in EFA.
iii. Provably equivalent, over ACA, to Con(MAH).

We have already 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).

It is more ambitious to work with the five expressions

A
A'
RA
R<A'>
R(A'\(8k)!).

And the two inclusion relations

s containedin t
s containedin* t.

This comprises 50 inclusions. The idea is to classify Proposition A using,
as conclusion, any of the 2^50 subsets interpreted conjunctively. I.e.,
which are true and which are false, and show that each one can be decided
in, say, EFA.

Getting rid of silly inclusions, we have 40 inclusions, and 2^40 subsets.
This is roughly 1 trillion statements.

Yet more ambitiously, we can generate a hierarchy of expressions as follows.

1. A,A',A\(8k)!,A'\(8k)! are expressions.
2. If t is an expression, then so are Rt, (Rt)', (Rt)\(8k)!, (Rt)'\(8k)!.

Atomic statements are again of the forms

3. s containedin t.
4. s containedin* t.

We want to handle arbitrary finite sets of atomic statements, interpreted
conjunctively. 

At the level appropriate for Theorem 1.4, we have 4 expressions from 1 and
another 16 from 2, for a total of 20 expressions. This yields 2(20)(19) =
760 nontrivial inclusions. The number of statements to be analyzed is 2^760.

At the level appropriate for Proposition A, we have 4 expressions from 1, 16
more from one application of 2, and 64 more from a second application of 2.
Total number of expressions is 84, yielding 2(84)(83) = 13,944 nontrivial
inclusions. The number of statements to be analyzed is 2^13,944.

It remains to be seen whether these classifications can actually be carried
out, and whether EFA is enough for the 2^760 classification, and whether
Con(MAH) is enough for the 2^13,944 classification.

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

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

Harvey Friedman