FOM: 88:Boolean Relation Theory

[Harvey Friedman]

This is a slightly edited version of an extended abstract that was handed
out at the ASL meeting in Urbana, 6/3/00 - 6/7/00.

BOOLEAN RELATION THEORY
by
Harvey M. Friedman
friedman at math.ohio-state.edu
www.math.ohio-state.edu/~friedman/
Extended Abstract
June 8, 2000

NOTE: The claims made here represent work in progress, documented by
working drafts of manuscripts that are expected to be circulated during the
summer. All developments in Boolean relation theory, past, present, and
future, will be presented and discussed on the FOM e-mail list. Interested
parties should subscribe by writing to Steve Simpson at
simpson at math.psu.edu.

Boolean relation theory concerns the relationship between sets and their
images under multivariate functions. We give detailed formulations of
Boolean relation theory and its specializations.

1. EQUATIONAL, INEQUATIONAL, PROPOSITIONAL, BOOLEAN RELATION THEORY.

A multivariate function f is a pair (g,k), where g is a function, k >= 1,
and dom(g) is a set of the form A^k. We say that f is k-ary. We write f(x)
for g(x) and dom(f) for dom(g) and rng(f) for rng(g).

We say that f is a multivariate function from A into B if and only if
dom(f) = A^k and rng(f) containedin B, where f is k-ary. For multivariate
functions f and sets A, we define fA to be f[A^k], where f is k-ary.

The Boolean expressions in sets (or set variables) B_1,Š,B_n are defined
inductively as follows:

i) emptyset and each B_i are Boolean expressions;
ii) if s,t are Boolean expression then (s union t), (s intersection t), and
s' are Boolean expressions.

Here s' denotes the complement of s.

A Boolean equation is an equation s = t, where s,t are Boolean expressions.

A Boolean inequation is an inequation s not= t, where s,t are Boolean
expressions.

The propositional combinations of Boolean equations are obtained from the
Boolean equations through use of the usual propositional connectives.

Let V be a set of multivariate functions and K be a set of sets.

Let n,m >= 1. Equational (inequational, propositional) BRT on (V,K) of type
(n,m) is the set of all statements of the form

for all f_1,Š,f_n in V there exists A_1,Š,A_m in K such that  a given
Boolean equation (Boolean inequation, propositional combination of Boolean
equations) holds in the m(n+1) sets

A_1,Š,A_m
f_1A_1,Š,f_1A_m
Š
f_nA_1,Š,f_nA_m.

Here we interpret complementation in such a way that we avoid proper
classes. Specifically, the interpretation of a Boolean expression t' is
taken to be (unionK)\B, where B is the interpretation of t.

Equational (inequational, propositional) BRT is the union over n,m >= 1 of
equational (inequational, propositional) BRT of type (n,m).

The case n = m = 1 is the most elemental type, where we have a single
function and a single set. Here even equational BRT on (V,K) of type (1,1)
can be highly nontrivial.

The goal of equational (inequational, propositional) BRT on (V,K) (of type
(n,m)) is to determine the truth or falsity of all of its members. For a
given n,m >= 1, there are 2^2^m(n+1) elements of equational (inequational)
BRT on (V,K) of type (n,m), up to Boolean equivalence. There are
2^2^2^2^m(n+1) elements of propositional BRT on (V,K) of type (n,m) up to
Boolean/logical equivalence.

2. EXTENDED EQUATIONAL, INEQUATIONAL, PROPOSITIONAL, BOOLEAN RELATION THEORY.

The extended Boolean expressions in functions (or function variables)
f_1,Š,f_n and sets (or set variables) A_1,Š,A_m are defined inductively as
follows:

i) emptyset and each A_i are extended Boolean expressions;
ii) if s,t are extended Boolean expressions then so are (s union t), (s
intersect t), and s';
iii) if s is an extended Boolean expression then each f_i(s) is an extended
Boolean expression.

An extended Boolean equation is an equation s = t, where s,t are extended
Boolean expressions.
not= t, where s,t are extended Boolean expressions.

The propositional combinations of extended Boolean equations are obtained
from the extended Boolean equations through use of the usual propositional
connectives.

Let V be a set of multivariate functions and K be a set of sets. Let n,m >= 1.

Extended equational (inequational, propositional) BRT on (V,K) of type
(n,m) is the set of all statements of the form

for all f_1,Š,f_n in V there exists A_1,Š,A_m in K such that a given
extended Boolean equation (Boolean inequation, propositional combination of
Boolean equations) holds in the functions f_1,Š,f_n and the sets A_1,Š,A_m.

Extended equational (inequational, propositional) BRT on (V,K) is the union
over n,m >= 1 of extended equational (inequational, propositional) BRT of
type (n,m).

We say that extended equational (inequational, propositional) BRT on (V,K)
(of type (n,m)) can be carried out in a formal system T if and only if
every statement in it is provable or refutable in T. This definition
assumes that a definition of V,K is given in T, as is usual.

Note that there are infinitely many statements in even extended equational
BRT on (V,K) of type (1,1). However, we can introduce a new parameter for
the number of occurrences of functions (or function variables) in an
extended Boolean expression. We then have finitely many statements in the
extended theory of type (n,m).

We can omit (V,K) and consider equational (inequational, propositional) and
extended equational (inequational, propositional) BRT (of type (n,m)). Here
we consider the formal statements themselves, stated with undetermined V,K.

3. SOME V'S AND K'S.

Natural (V,K) appear throughout the whole of mathematics, and they are a
characteristic feature of many areas of mathematics. BRT on (V,K) appears
to be highly nontrivial for any nontrivial (V,K). In fact, even equational
BRT of type (1,1) is normally quite interesting.

In this section, we list some V's and K's that are used for results that we
are obtained thus far. Clearly these results have just barely scratched the
surface.

Let Z be the set of all integers, and N be the set of all nonnegative
integers. For x in Z^k, |x| is the sup norm of x; i.e., the maximum of the
absolute values of the coordinates of x.

V_1. All multivariate functions from N into N.
V_2. All strictly dominating multivariate functions from N into N. I.e.,
for all x in dom(f), f(x) > |x|.
V_3. All multivariate functions from N into N of expansive linear growth.
This means that there exist rationals p,q > 1 such that for all x in
dom(f), the inequality

p|x| <= f(x) <= q|x|

holds with finitely many exceptions.

V_4. All multivariate functions from N into N of quadratic growth. This
means that there exist positive rationals p,q such that for all x in
dom(f),

p|x|^2 <= f(x) <= q|x|^2.

V_5. All multivariate functions from N into N of nonlinear polynomial
growth. This means that there exist positive rationals p,q and integers n,m
> 1 such that for all x in dom(f),

p|x|^n <= f(x) <= q|x|^m.

A multivariate piecewise polynomial from N into N over Z is a multivariate
function f from N into N which is defined by cases, each of which is given
by a finite set of inequalities between multivariate polynomials with
integer coefficients, and where f is defined in each case by a polynomial
with integer coefficients.

V_6. All multivariate piecewise polynomials f from N into N over Z such
that for all x in dom(f), f(x) <= 2|x|.

V_7. All multivariate piecewise polynomials f from N into N over Z of
nonlinear growth. This means that there exists a rational p > 0 and an
integer n > 1 such that for all x in dom(P), f(x) >= p|x|^n.

Note that V7 is the same as V5 restricted to the multivariate piecewise
polynomials P from N into N over Z.

A maxed polynomial over Z is a multivariate function f from Z into Z of the
form

f(x) = max(P_1(x),Š,P_n(x))

where P_1,Š,P_n are polynomials over Z of the same arity as f.

V_8. All maxed polynomials f over Z such that for all x in dom(f), f(x) >=
2|x|.

V_9. All maxed polynomials f over Z of nonlinear growth. This means that
there exists a rational p > 0 and an integer n > 1 such that for all x in
dom(f), f(x) >= p|x|^n.

K_1. The set of all infinite subsets of N.

K_2. The set of all infinite subsets of N of the form fA, where f is a
piecewise polynomial over Z and A = {n!!: n in N}.

5. THE THIN SET THEOREM.

Boolean relation theory begins with the thin set theorem. It is the most
basic interesting theorem in inequational Boolean relation theory. In fact,
it lies in inequational Boolean relation theory on (V_1,K_1) of type (1,1).

THIN SET THEOREM. Let f be a multivariate function from N into N. There
exists an infinite set A containedin N such that fA not= N.

The thin set theorem can be easily proved from the classical infinite
Ramsey theorem, and can be proved in ACA but not in ACA_0. In fact, it is
provably equivalent over RCA_0 to the classical infinite Ramsey theorem. It
is discussed in a joint paper with Steve Simpson to appear in the
Proceedings of the Boulder Conference (an AMS Summer Research Conference).

6. THE COMPLEMENTATION THEOREM.

The complementation theorem is the most basic interesting theorem in
equational Boolean relation theory. In fact, it lies in equational Boolean
relation theory on (V_2,K_1) of type (1,1). It is provable in RCA_0, but
is, in a sense, complete for bounded recursion.

COMPLEMENTATION THEOREM. Let f be a multivariate function from N into N
obeying the inequality f(x) > |x|. There exists an infinite set A
containedin N such that fA = N\A.

We can sharpen the complementation theorem in the following way. However,
this sharper form is, strictly speaking, not part of Boolean relation
theory.

THEOREM. Let f be a multivariate function from N into N obeying the
inequality f(x) > |x|. There exists a unique set A containedin N such that
fA = N\A. Furthermore, A is infinite.

We can obviously rewrite fA = N\A as A = N\fA, in which case it can be
viewed as a fixpoint theorem.

7. SOME EASY CLASSIFICATIONS.

For any V,K, both equational and inequational Boolean relation theory on
(V,K) of type (1,1) have 16 statements.
I have carried out equational and inequational Boolean relation theory on
(Vi,Kj) of type (1,1), where 1 <= i <= 9 and j = 1, and where 6 <= i <= 9
and j = 2. Every statement is refutable in RCA_0 or provable in RCA_0 plus
the classical infinite Ramsey theorem.

In future communications, I will present the actual classifications.

8. EQUATIONAL BOOLEAN RELATION THEORY OF TYPE (2,3).

This is the first level of BRT where we know that we run out of axioms in ZFC.

In particular, we consider the following instance of equational Boolean
relation theory of type (2,3).

For all f,g in V there exists A,B,C in K such that

i) A containedin B containedin C;
ii) fA containedin B union gB;
iii) fB containedin C union gC;
iv) C intersect gC = emptyset;
v) A intersect fC = emptyset.

Let MAH = ZFC + {there exists an n-Mahlo cardinal}_n. Let MAH+ = ZFC + "for
all n >= 1 there exists an n-Mahlo cardinal."

THOEREM 8.1. The above instance of equational Boolean relation theory of
type (2,3) in (V_i,K_1), where 3 <= i <= 9, is provably equivalent to the
1-consistency of MAH over ACA.

THEOREM 8.2. The above instance of equational Boolean relation theory of
type (2,3) in (V_i,K_2), where 6 <= i <= 9, is provably equivalent to the
1-consistency of MAH over ACA.

>From these results, we see that it is necessary to use Mahlo cardinals of
finite order in order to carry out equational Boolean relation theory of
type (2,3) in any of  (V_i,K_1), 3 <= i <= 9, and (V_i,K_2), 6 <= i <= 9.

But are they sufficient?

CONJECTURE 8.3. Every instance of equational Boolean relation theory of
type (2,3) in (V_i,K_1), 3 <= i <= 9, and in (V_i,K_2), 6 <= i <= 9, is
provable or refutable in MAH+. This is false with MAH+ replaced by MAH.
Thus we say that it is necessary and sufficient to use Mahlo cardinals of
finite order in order to carry out Boolean relation theory in these
contexts.

This conjecture is a moral certainty, and will be established within 2 years.

We have a significant partial result on this conjecture which convinces us
of this moral certainty.

Look at the five clauses in the above instance of equational Boolean
relation theory of type (2,3).

Note that it consists of two disjointness condition and four inclusions.
The inclusions have a single term on the left side. These are called
coverings conditions. Thus there are two disjointness conditions and four
coverings.

We will separate A containedin B containedin C off as a given. Thus we use
the terminology towered equational Boolean relation theory to indicate that
the sets have to form a tower under inclusion.

At this point, the natural partial result for Conjecture 8.3 would treat
sets of disjointness and covering conditions in towered equational BRT of
type (2,3) in these (V,K).

This is the major partial result we expect to have this summer. But right
now, we have a draft that carries this out with a restriction on the
covering conditions. The restriction is that the covering conditions be
forward covering conditions.

To explain what forwardness means, rewrite A,B,C as A1,A2,A3. The
forwardness requirement asserts that the subscript on the left side must be
less than all subscripts appearing on the right side.

THEOREM 8.4. Let 3 <= i <= 9 and j = 1, or 6 <= i <= 9 and j = 2. All
statements in towered Boolean relation theory in (V_i,K_j). with
disjointness and forward covering conditions only, are provable or
refutable in MAH+. This is false with MAH+ replaced by MAH. In fact, they
are either refutable in RCA_0 or provable in ACA + the 1-consistency of
MAH,. Thus we say that it is necessary and sufficient to use Mahlo
cardinals of finite order in order to carry our Boolean relation theory in
these contexts.

9. FINITENESS.

We have seen that it is necessary and sufficient to use large cardinals for
certain concrete classification problems and to prove certain special cases
of those classification problems.

It remains to give a necessary and sufficient uses of large cardinals for
proving concrete statements of a nontechnical nature.

Our examples arise in the form of a general feature of the classifications
that follow immediately from the way the classifications are carried out.

In any form of Boolean relation theory in (V,K), we say that a statement is
finitely true if and only if the existentially quantified sets in K are
required instead to be nonempty finite sets rather than elements of K.

CONJECTURE 9.1 (finiteness). Let 3 <= i <= 9 and j = 1, or 6 <= i <= 9 and
j = 2. The following is provably equivalent to the 1-consistency of MAH.
All statements in equational Boolean relation theory in (V_i,K_j) that are
finitely true, are true.

We know that we can replace "is provably eqvuivalent to the" with "provably
implies the".

THEOREM 9.2. (finiteness). Let 3 <= i <= 9 and j = 1, or 6 <= i <= 9 and j
= 2. The following is provably eqvuivalent to the 1-consistency of MAH. All
statements in towered equational Boolean relation theory in (V_i,K_j),
using only disjointness and forward coverings, that are finitely true, are
true.

**********

This is the 88th in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM
5:Constructions  11/15/97  5:24PM
6:Undefinability/Nonstandard Models   11/16/97  12:04AM
7.Undefinability/Nonstandard Models   11/17/97  12:31AM
8.Schemes 11/17/97    12:30AM
9:Nonstandard Arithmetic 11/18/97  11:53AM
10:Pathology   12/8/97   12:37AM
11:F.O.M. & Math Logic  12/14/97 5:47AM
12:Finite trees/large cardinals  3/11/98  11:36AM
13:Min recursion/Provably recursive functions  3/20/98  4:45AM
14:New characterizations of the provable ordinals  4/8/98  2:09AM
14':Errata  4/8/98  9:48AM
15:Structural Independence results and provable ordinals  4/16/98
10:53PM
16:Logical Equations, etc.  4/17/98  1:25PM
16':Errata  4/28/98  10:28AM
17:Very Strong Borel statements  4/26/98  8:06PM
18:Binary Functions and Large Cardinals  4/30/98  12:03PM
19:Long Sequences  7/31/98  9:42AM
20:Proof Theoretic Degrees  8/2/98  9:37PM
21:Long Sequences/Update  10/13/98  3:18AM
22:Finite Trees/Impredicativity  10/20/98  10:13AM
23:Q-Systems and Proof Theoretic Ordinals  11/6/98  3:01AM
24:Predicatively Unfeasible Integers  11/10/98  10:44PM
25:Long Walks  11/16/98  7:05AM
26:Optimized functions/Large Cardinals  1/13/99  12:53PM
27:Finite Trees/Impredicativity:Sketches  1/13/99  12:54PM
28:Optimized Functions/Large Cardinals:more  1/27/99  4:37AM
28':Restatement  1/28/99  5:49AM
29:Large Cardinals/where are we? I  2/22/99  6:11AM
30:Large Cardinals/where are we? II  2/23/99  6:15AM
31:First Free Sets/Large Cardinals  2/27/99  1:43AM
32:Greedy Constructions/Large Cardinals  3/2/99  11:21PM
33:A Variant  3/4/99  1:52PM
34:Walks in N^k  3/7/99  1:43PM
35:Special AE Sentences  3/18/99  4:56AM
35':Restatement  3/21/99  2:20PM
36:Adjacent Ramsey Theory  3/23/99  1:00AM
37:Adjacent Ramsey Theory/more  5:45AM  3/25/99
38:Existential Properties of Numerical Functions  3/26/99  2:21PM
39:Large Cardinals/synthesis  4/7/99  11:43AM
40:Enormous Integers in Algebraic Geometry  5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees  5/25/99  5:11PM
43:More Enormous Integers/AlgGeom  5/25/99  6:00PM
44:Indiscernible Primes  5/27/99  12:53 PM
45:Result #1/Program A  7/14/99  11:07AM
46:Tamism  7/14/99  11:25AM
47:Subalgebras/Reverse Math  7/14/99  11:36AM
48:Continuous Embeddings/Reverse Mathematics  7/15/99  12:24PM
49:Ulm Theory/Reverse Mathematics  7/17/99  3:21PM
50:Enormous Integers/Number Theory  7/17/99  11:39PN
51:Enormous Integers/Plane Geometry  7/18/99  3:16PM
52:Cardinals and Cones  7/18/99  3:33PM
53:Free Sets/Reverse Math  7/19/99  2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry  8/27/99  3:01PM
57:Fixpoints/Summation/Large Cardinals  9/10/99  3:47AM
57':Restatement  9/11/99  7:06AM
58:Program A/Conjectures  9/12/99  1:03AM
59:Restricted summation:Pi-0-1 sentences  9/17/99  10:41AM
60:Program A/Results  9/17/99  1:32PM
61:Finitist proofs of conservation  9/29/99  11:52AM
62:Approximate fixed points revisited  10/11/99  1:35AM
63:Disjoint Covers/Large Cardinals  10/11/99  1:36AM
64:Finite Posets/Large Cardinals  10/11/99  1:37AM
65:Simplicity of Axioms/Conjectures  10/19/99  9:54AM
66:PA/an approach  10/21/99  8:02PM
67:Nested Min Recursion/Large Cardinals  10/25/99  8:00AM
68:Bad to Worse/Conjectures  10/28/99  10:00PM
69:Baby Real Analysis  11/1/99  6:59AM
70:Efficient Formulas and Schemes  11/1/99  1:46PM
71:Ackerman/Algebraic Geometry/1  12/10/99  1:52PM
72:New finite forms/large cardinals  12/12/99  6:11AM
73:Hilbert's program wide open?  12/20/99  8:28PM
74:Reverse arithmetic beginnings  12/22/99  8:33AM
75:Finite Reverse Mathematics  12/28/99  1:21PM
76: Finite set theories  12/28/99  1:28PM
77:Missing axiom/atonement  1/4/00  3:51PM
78:Qadratic Axioms/Literature Conjectures  1/7/00  11:51AM
79.Axioms for geometry  1/10/00  12:08PM
80.Boolean Relation Theory  3/10/00  9:41AM
81:Finite Distribution  3/13/00  1:44AM
82:Simplified Boolean Relation Theory  3/15/00  9:23AM
83: Tame Boolean Relation Theory  3/20/00  2:19AM
84: BRT/First Major Classification  3/27/00  4:04AM
85:General Framework/BRT   3/29/00  12:58AM
86:Invariant Subspace Problem/fA not= U  3/29/00  9:37AM
87:Programs in Naturalism  5/15/00  2:57AM