FOM: BRT progress report

[Harvey Friedman]

This is a progress report on Boolean relation theory, a subject of numerous
recent postings by me on the FOM. I will be preoccupied with some other
matters for a little while, but thought it would be good to make this
report in advance of some more formal, unhedged, announcements expected
over the next month or so.

1. A manuscript sketching the proof using Mahlo cardinals of finite order
of a key instance of Boolean relation theory exists and was gone over in
detail (more detail than previously) in the local seminar here today
without any difficulties arising.

2. The first 25 pages of a manuscript reversing that key instance of
Boolean relation theory has been written, and the first priority of BRT now
is to finish this manuscript at least to the point of completing that
reversal. (I.e., that the key instance of BRT implies the consistency of
Mahlo cardinals of finite order - and less urgently, the 1-consistency of
Mahlo cardinals of finite order).

3. By key instance here, we mean an instance of the following set of
statements:

*) For all multivariate functions f,g from N into N of expansive linear
growth, there exist infinite A,B,C containedin N such that a given Boolean
equation hold of A,B,C,fA,fB,fC,gA,gB,gC.

Any Boolean equation between finitely many sets can be represented as a
finite set of inclusion statements, each of the form: a finite intersection
is included in a finite union.

The specific key instance under question is much simpler than any typical
Boolean equation, which is particularly apparent when looking at its
representation as a set of inclusions.

4.  The above shows that it is necessary to use Mahlo cardinals of every
finite order in order to decide all of the finitely many instances of *).
(Necessary in various obvious senses). Recall the conjecture that every
instance of *) can be proved or refuted using Mahlo cardinals of finite
order. When these are combined, we have the conjecture that it is necessary
and sufficient to use Mahlo cardinals of finite order to decide all
instances of *).

5. There is a 75 page manuscript which consists mainly of tables that
completely determine the truth values of all instances of *) that are
subject to a restriction. This is a partial result on the conjecture. The
restriction is quite natural. We can put it this way. We look at

**) For all multivariate functions f,g from N into N of expansive linear
growth, there exist infinite A1 containedin A2 containedin A3 containedin N
such that a given set of forward coverings and exclusions hold of
A1,A2,A3,fA1,fA2,fA3,gA1,gA2,gA3.

Here a covering asserts that one of the nine sets is included in the union
of others. A forward covering asserts that one of the nine sets is included
in the union of others, where the subscript used on the left (1,2, or 3) is
less than all of the subscripts used on the right. Here an exlusion asserts
that two of the nine sets are disjoint.

6. The 75 page manuscript has the following form. There are about a dozen
crucial instances of **) that are identified, some of which are refuted,
some of which are proved in RCA_0, and some of which are proved using Mahlo
cardinals of finite order. The latter are simply variants of the crucial
instance referred to above in 1 and 2. The remaining ones are handled in
this manuscript, and are a bit tricky but with short arguments. The rest of
the 75 pages is just formal Boolean algebra. So there is a classification
of **) based on just a few principles, and the classification can be
axiomatized.

Now that I have slogged through the patterns, the manuscript will likely be
substantially consolidated, with the benefit of hindsight.

7. The key instance of *) corresponding to Mahlo cardinals of finite order
is in fact (also) an instance of **), where there are two forward coverings
and two exclusions.

8. I will discuss this key instance on the FOM when I have completed the
writeup of the proof that it corresponds to Mahlo cardinals of finite
order.

9. I have discovered that there is much to be gained by viewing statements
in Boolean relation theory in the following form: given functions of a
certain kind there exists sets of a certain kind such that a special kind
of forall/thereexists statement holds of the sets and their images. One can
say more here because one is using variables. This allows one to say local
things rather than just global things as in *) and **). At the moment, this
extended theory is a step backward for the general mathematical community.
It probably can be reworked, however, to be competitive with BRT, but at
the moment I envision it as

i) mainly for the math logic community and others already interested in f.o.m.;
ii) something which is very natural even for the general mathematical
community AFTER they have digested BRT.

10. The big gain from this extended theory is that it appears that one
immediately runs right into large cardinals even for finite functions and
finite sets. In fact, when doing this, one runs right into subtle cardinals
of finite order, which are somewhat larger. And these finite statements can
be given iterated exponential estimates, and so are Pi-0-1 on the page.

Also, one runs into smaller cardinals, and even just aleph omega.

11. Also, in the infinite case, one immediately runs right into much
stronger axioms such as 0#. In fact, it appears that one runs right into
the entire large cardinal hierarchy including j:V into V (over ZF). It even
seems very likely that one runs right into j:V into V with finite functions
and finite sets, and again with iterated exponential estimates, Pi-0-1 on
the page! At least, that is the plan.

In fact, I believe that one can fine tune this extended theory to any level
of the logical universe one desires (conjecture).

12. As in BRT, all of this becomes much more striking in the presence of
substantial classification theorems. However, because in this extended
theory, one can say more, it would appear that appropriate classification
theorems may remain out of reach. However, the added power also allows one
to make many more natural distinctions, which should allow for appropriate
classification theorems. I will start developing this extended theory in
detail only after BRT is properly formally launched with unhedged claims
and manuscipts - which I expect to be at the upcoming ASL meeting in
Urbana.

13. There is an important theoretical concept that seems crucial in gaining
a perspective on all this. Let S be any  set of sentences in set theory. We
say that S is amenable over ZFC if and only if there is a short sentence
phi in set theory such that

i) ZFC + phi is consistent;
ii) every element of S is provable or refutable in ZFC + phi.

Also, S is very amenable over ZFC if and only if there is a short sentence
phi in set theory such that

i) ZFC + phi is consistent;
ii) every element of S has a short proof or a short refutation in ZFC + phi.

This definition is most relevant for our purposes in the case of *finite* S.

All of the large cardinal axioms seriously studied can be written down as
short sentences of set theory. By various things I have done over the
years, I know how to write them down as much shorter sentences of set
theory than one would normally.

14. Note that classification problems *) and **), as well as any
interesting ones that are coming up in this whole BRT development and
beyond, involve enormous numbers of instances, the preponderance of which
are somewhat bigger than short. With *), there are 2^2^9 instances,
generally of size about 2^9. So there is absolutely no a priori reason to
assume that these sets of statements are amenable or very amenable. Of
course, I now know that **) is very amenable over ZFC - assuming Mahlo
cardinals of finite order are consistent. In fact, I have good reasons to
believe that "**) is amenable over ZFC" can be proved even without the
assumption that Mahlo cardinals of finite order are consistent (even in
just ACA). Obviously, I conjecture that *) is very amenable over ZFC. In
fact, I conjecture that any reasonable classfication problem coming out of
BRT and beyond is very amenable over ZFC.