FOM: 85:General Framework/BRT

Harvey Friedman friedman at math.ohio-state.edu
Wed Mar 29 00:58:46 EST 2000

There is a slight ambiguity about the general framework for Boolean
relation theory as discussed in postings #80, #82, #83. This ambiguity
concerns the use of a universal set. Now that Boolean relation theory has
gone from conception to a very young embryo, it is important to make a very
careful restatement.

1. EQUATIONAL BOOLEAN RELATION THEORY.

A Boolean relation theory context is a triple (V,K,U), where

i) V is a set of functions;
ii) U is a set;
iii) K is a set of subsets of U.

We place no further restrictions on V,K,U. U serves as the universal set in
Boolean expressions.

Let f be a function and A be a set. We write fA for {f(x): x in dom(f) and
for some k >= 1, x lies in A^k}.

The Boolean expressions in set variables E_1,...,E_r are defined
inductively as follows:

i) each E_i is a Boolean expression;
ii) U is a Boolean expression;
iii) if s,t are Boolean expressions then so is s\t.

For each n,m >= 1, we study the statements

1) For all f_1,...,f_n in V there exist A_1,...,A_m in K such that the
(1+n)m sets
A_1,...,A_m
f_1A_1,...,f_1A_m
...
f_nA_1,...,f_nA_m

obey a given Boolean equation in (1+n)m set variables.

An example of a BRT context of special interest is the triple (V,K,U), where

a) V is the set of all multivariate functions from N into N of expansive
linear growth (as defined in posting #84);
b) U is N;
c) K is the set of all infinite subsets of N.

2. INEQUATIONAL BOOLEAN RELATION THEORY.

Inequational BRT in the BRT context (V,K,U) studies the statements

2) For all f_1,...,f_n in V there exist A_1,...,A_m in K such that the
(1+n)m sets
A_1,...,A_m
f_1A_1,...,f_1A_m
...
f_nA_1,...,f_nA_m

obey a given set of Boolean equations and Boolean inequations in (1+n)m set
variables.

Here a Boolean inequation is just the negation of a Boolean equation.

Inequational BRT is already interesting in the very simple BRT context
(V,K,U), where

a) V is the set of all multivariate functions from N into N;
b) U is N;
c) K is the set of all infinite subsets of N.

In fact, the simple instance

2*) For all f in V there exists A in K such that fA not= U.

has been discussed in earlier postings. It is proved using the classical
infinite Ramsey theorem. We know that it is not provable in ACA_0,
suggesting that it cannot be proved without the classical infinite Ramsey
theorem. It gives a new application of the infinite Ramsey theorem of very
wide appeal.

Now let V be the set of bounded linear operators on Hilbert space H, U = H,
and K be the set of all closed subspaces of H.

Then 2*) is the invariant subspace problem for Hilbert space, as discussed
in postings Tue, 28 Mar 2000 22:32 and 3/29/00 12:16AM.

3. CONDITIONAL BOOLEAN RELATION THEORY.

Conditional BRT in the BRT context (V,K,U) studies the statements

3) For all f_1,...,f_n in V there exist A_1,...,A_m in K such that the
(1+n)m sets
A_1,...,A_m
f_1A_1,...,f_1A_m
...
f_nA_1,...,f_nA_m

obey a given propositional combination of Boolean equations in (1+n)m set
variables.

The reason we use the term "conditional" is that ***) includes, e.g.,
statements of the form "if such and such Boolean equations holds then such
and such Boolean equations hold."

4. SIMPLE COMPOUND EQUATIONAL, INEQUATIONAL, CONDITIONAL, BOOLEAN RELATION
THEORY.

The simple compound expressions in function variables h_1,...,h_p and set
variables E_1,...,E_q are defined inductively as follows:

i) each E_i is a simple compound expression;
ii) if t is a simple compound expression then each h_it is a simple
compound expression.

The simple compound Boolean expression in function variables h_1,...h_p and
set variables E_1,...,E_q are defined inductively as follows:

i) each simple compound expression is a simple compound Boolean expression;
ii) U is a simple compound Boolean expression;
iii) if s,t are Boolean expressions then so is s\t.

Simple compound equational BRT in the BRT context (V,K,U) studies the
statements

4) For all f_1,...,f_n in V there exist A_1,...,A_m in K such that a given
simple compound Boolean equation in n function variables and m set
variables holds.

Simple compound inequational BRT in the BRT context (V,K,U) studies the
statements

5) For all f_1,...,f_n in V there exist A_1,...,A_m in K such that a given
set of simple compound Boolean equations and simple compound Boolean
inequations in n function variables and m set variables holds.

Simple compound conditional BRT in the BRT context (V,K,U) studies the
statements

6) For all f_1,...,f_n in V there exist A_1,...,A_m in K such that a given
propositional combination of simple compound Boolean equations in n
function variables and m set variables holds.

5. COMPOUND EQUATIONAL, INEQUATIONAL, CONDITIONAL, BOOLEAN RELATION THEORY.

The compound expressions in function variables h_1,...,h_p and set
variables E_1,...,E_q are defined inductively as follows:

i) each E_i is a compound expression;
ii) if t is a compound expression then each h_it is a simple compound
expression;
iii) U is a compound expression;
iv) if s,t are compound expressions then so is s\t.

Compound equational BRT in the BRT context (V,K,U) studies the statements

7) For all f_1,...,f_n in V there exist A_1,...,A_m in K such that a given
compound Boolean equation in n function variables and m set variables
holds.

Compound inequational BRT in the BRT context (V,K,U) studies the statements

8) For all f_1,...,f_n in V there exist A_1,...,A_m in K such that a given
set of compound Boolean equations and  compound Boolean inequations in n
function variables and m set variables holds.

Compound conditional BRT in the BRT context (V,K,U) studies the statements

9) For all f_1,...,f_n in V there exist A_1,...,A_m in K such that a given
propositional combination of compound Boolean equations in n function
variables and m set variables holds.

**********

This is the 85th 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
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
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