[FOM] 196:Quantifier complexity in set theory

[Harvey Friedman]

FOR THE RECORD. Despite many recent postings with titles containing "195.
The axiom of choice", there is no indication that the results there either
need correction or can be improved or can be reproved in any simpler way.

##############################

In my posting: On AE...EA...A  4/2/03, 10:50PM, I wrote

"The complexity class
AE...EA...A
of sentences in primitive notation (epsilon,=), is very wild.
In particular, every sentence of the form
A...AE...EA...A(phi)
where phi is a formula with epsilon bounded quantifiers,
can be effectively converted to an equivalent sentence of the form
AE...EA...A

This means that the set of true sentences of the form AE...EA...A in
epsilon,= is of very high degree, and there are plenty of instances
which are undecided in ZFC."

The point of this posting is to elaborate on such matters.

On 11/5/03 10:59 AM, "Marcin Mostowski" <Marcin.Mostowski at mail.uw.edu.pl>
wrote:

> E.g. the following is equivalent to AC:
> 
> \forall R (\forall x \exists y R(x,y) implies
> \exists F \subseteq R (\forall x \exists y F(x,y) and
> \forall x \forall y,y'
>   (R(x,y) and R(x,y') implies y=y') ).
> 
> This has more than 6 quantifiers but has quantifier depth 4, and it
> seems
> to be optimal.

I assume that by quantifier depth, we are talking about the number of
alternations of quantifiers. I.e., you are saying that AxC is of the form

AE...EA...AE...E

over ZF, and conjecturing that

A...AE...EA...A
E...EA...AE...E

will not do. NOTE: We are talking about primitive notation only, with just
epsilon,=. 

A stronger conjecture is that for the AxC we cannot use

E...EA...AE...EA...A

in primitive notation; i.e., epsilon,=.

I believe this conjectures (and they are tractable). We remark that the AxC
can be stated in form AE (bounded). It cannot be stated in EA (bounded).
Here "(bounded)" means bounded quantifiers are allowed.

Also, EA...AE...E is strong enough to state, e.g.,

V(omega + omega) is well ordered.

#################################

There are several complexity hierarchies interesting for sentences of set
theory with epsilon,=. Let's organize them. I will assume that the sentence
is in prenex form A = Q1Q2...QkB. Let us call B the "matrix" (this is common
terminology). Below, C stands for "complexity".

C1. The matrix B has no quantifiers, and we count the number of quantifiers.
C2. The matrix B has no quantifiers, and we count the number of alternations
of quantifiers - and also indicate whether it starts with E's or with A's.
C3. The matrix is a BOUNDED formula (i.e., bounded quantifiers are used).
and we count the number of quantifiers.
C4. The matrix is a BOUNDED formula, and we count the number of alternations
of quantifiers - also indicate whether it starts with E's or with A's.

There are many other measures as well, say where Boolean combinations are
specifically considered.

I.e., define J0 = quantifier free formulas (or alternatively with bounded
quantifiers allowed).
Define Jn+1 = zero or one quantifier (or alternatively a block of like
quantifiers) followed by a Boolean combination of formulas from Jn.

I won't state any results or conjectures concerning these various kinds of
J's. 

####################################

Let me state some known information about C1-C4.

C1. We first remark that there are only finitely many sentences with k
quantifiers, up to a strong form of logical equivalence. This follows
immediately from the fact that there are only finitely many constant and
relation symbols, and no function symbols (we actually have no constant
symbols and only one (binary) relation symbol).

As I said many times on the FOM, all 3 quantifier sentences are decided in a
weak fragment of ZF. There is a 5 quantifier sentence that is not decided in
ZFC, and is provably equivalent to the existence of a subtle cardinal over
ZFC. (See recent issues of Fund. Math., and J. Math Logic). I do not know of
a 5 quantifier sentence that is independent of ZFC but equiconsistent with
ZFC. I conjecture that there is none. I conjecture that every 5 quantifier
sentence is provable or refutable from ZFC + small large cardinals, and in
particular ZFC + there exists a subtle cardinal. I conjecture that every 4
quantifier sentence is decided in a somewhat weak fragment of ZF (it has to
include the power set axiom). I conjecture that the axiom of choice cannot
be stated with 5 quantifiers, but this isn't known even for 4 quantifiers.
We know that the AxC can be stated with 6 quantifiers (posting #195). I
conjecture that every sentence with 6 quantifiers can be decided in ZFC
together with a proper class of small large cardinals. In the JML paper, I
gave an example of a 6 quantifier sentence that is provably equivalent to
"there is a proper class of subtle cardinals". I conjecture that any two 6
quantifier sentence A,B, have the property that ZFC + A is interpretable in
ZFC + B or vice versa, and that this even holds with ZFC replaced by ZF. I
conjecture that this comparability holds for at least a few levels beyond 6,
but breaks down soon thereafter.

Putting my feet to the fire, I will conjecture that this comparability holds
up through 9 quantifiers. I conjecture that every sentence with 9
quantifiers is decided in ZFC + there exists a proper class of cardinals
kappa such that there is an elementary embedding from kappa into kappa, all
with the same critical point, and that measurable cardinals do not suffice.

I conjecture that there is a robust notion of "profound chaos", and that
profound chaos kicks in using at most 12 quantifiers. E.g., incomparability
and other profound unpleasantness comes in.

I conjecture that for all k >= 5, there is a sentence with k+1 quantifiers
that is not provably equivalent to any sentence with k quantifiers, over
ZFC. Furthermore, I conjecture that for all k >= 5, there is a sentence A
with k+1 quantifiers such that ZFC + A proves the consistency of the
conjunction of all true k quantifier sentences.

In general, I conjecture that one can "map out" much of the large cardinal
hierarchy through this counting of quantifiers, in a ROBUST manner. This
would be a rather striking vindication of the naturalness of the large
cardinal hierarchy through an apparently completely "neutral" consideration
- the mere count of quantifiers.

However, there is unlikely to be sufficient control to fine tune the large
cardinal hierarchy, nor sufficient control to make this project fully
feasible within the Century.

I conjecture that additional fruitful and productive and illuminating
control comes from the following:

I. Exact prefix classes; e.g., I put "there exists a subtle cardinal" in
form EAEEA, and also that computation will put it in other five quantifier
prefix classes. 
II. The number of distinct atomic formulas used. The examples given in JML
always have relatively few distinct atomic formulas. In fact, relatively few
total occurrences of atomic formulas!
III. For finer detail, one can also just list the distinct atomic formulas
used. This information also tells us what quantifiers are used - but not
their sign (E or A) or order of appearance.
IV. Less robustly, one can even list the atomic formulas used with
multiplicities. This obviously depends on the choice of connectives used.
However, it does not seem to be silly to simply use the standard list, not,
and, or, if then, iff.

A particular intriguing possibility, based on III, is that of a map that
sends

*a finite set of atomic formulas*

into a level of set theory. Namely, one considers the finite set (up to
logical equivalence) of sentences in set theory whose atomic formulas are
among those in the given finite set. One then associates a level of set
theory to this finite set of sentences.

Of course, one can also consider the possibility of doing this with IV
instead of III.

C2. (Alternations). Here every complexity class is infinite, and so the
study is of a somewhat different character than of C1.

Every A...AE sentence can be proved or refuted in a very weak fragment of
ZF. It is not known if this is the case for A...AE...E. There are some
promising attacks on the A...AEE and E...EAA cases. See

Parlamento, On the decision problem for fragments of set theory, 6/3/03,
2:43PM

for a detailed discussion of this with references.

With three blocks, 

A...AE...EA...A

we step into a new world. See the remarks at the beginning of this posting
concerning my old posting: On AE...EA...A  4/2/03, 10:50PM.

This class is not only recursively undecidable, it is of same Turing degree
as (or even mutually effectively reducible to) the C4 class

A...AE...EA...A (bounded)

Here "(bounded)" means that bounded quantifiers are allowed in the matrix.
If "(bounded)" does not appear, then the matrix must be quantifier free.

By duality, we have an exact matching between

E...EA...AE...E and E...E and E...EA...AE...E (bounded).

In fact, we get an exact matching between C2 and C4 at the level of 3
quantifier blocks and higher - over ZFC.

Now just how rich is E...EA...AE...E (bounded)?  Incredibly. Already
E...EA...A (bounded) subsumes satisfiability in second order logic.

I know that E...EA...A (bounded) exactly matches satisfiability in second
order logic, and A...AE...E (bounded) exactly matches validity in second
order logic. 

Thus A...AE...EA...A properly subsumes validity and satisfiability in second
order logic, and so does E...EA...AE...E.

It is well known that in C4, you get "more and more" as you go up, and also
the ones starting with A are different than the ones starting with E, at any
given level. Therefore this is also true in C2, with at least 3 blocks.

QUESTION: These reductions take place over ZFC. What about reductions that
take place over ZF?

C4. This counts only blocks of unbounded quantifiers. This is one of the
most studied complexity notions in set theory.

E...E (bounded) is already highly nonrecursive, and matches Sigma-1-2
sentences in second order arithmetic. This result is over ZF.

We remarked above that E...EA...A (bounded) and A...AE...E (bounded) match
satisfiability and validity in second order logic.

C3. C3 is easily seen to exactly match C4.

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 196th 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-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM
186:Grand Unification 1  7/2/03  10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03  4:43AM
189:Some Model theoretic Pi-0-1 statements  9/25/03  11:04AM
190:Diagrammatic BRT 10/6/03  8:36PM
191:Boolean Roots 10/7/03  11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement  11/2/03  4:42PM
194:PL Statement/clarification  11/2/03  8:10PM
195:The axiom of choice  11/3/03  1:11PM
 
Harvey Friedman