THE UNIVERSITY OF MICHIGAN COMPUTING RESEARCH LABORATORY1 HENKIN QUANTIFIERS AND COMPLETE PROBLEMS Andreas. Blasn and Yuri GurevIch CRL-TR-39-84 September 1984 Room 1079, East Engineering Building Ann Arbor, Michigan 48109 USA Tel: (313) 783-8000 1Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of the funding agency.

u<Pl R 4ri7

HENKIN QUANTIFIERS AND COMPLETE PROBLEMS by Andreas Blass1 and Yuri Gurevich2 Mathematics Dept. and Computer and Communication Sciences Dept. The University of Michigan Ann Arbor, Michigan 48109, USA 1. Partially supported by NSF grant MCS 81-01560 2. Partially supported by NSF grant MCS 83-01022

Abstract We analyze computational aspects of partially ordered quantification in first-ordeir logic. We show that almost any non-linear quantifier, applied to quantifier-free firstorder formulas, suffices to express an NP-complete predicate. The remaining non-linear quantifiers express exactly co-NL predicates.

Introduction Certain applications of logic to computer science, for example those discussed in [Gu], have the following features: only finite models are of interest, and first-order logic is not sufficiently expressive. Accordingly, various extensions of first-order logic have been proposed and analyzed for finite structures. The analysis often reveals connections with computational complexity, and indeed some of the extensions were proposed just for the purpose of obtaining such connections. (See [Gu], [Im] and the works cited there.) It is natural to consider also those extensions of first-order logic which appear in the logical literature and whose introduction was motivated by considerations quite distant from computer science. One such extension, perhaps the oldest that can be meaningfully applied to finite models, is the logic with partially ordered quantification introduced by Henkin [He]. We show in this paper that formulas obtained from first-order ones by application of these so-called Henkin quantifiers are able to express NP-complete properties of finite structures, for example 3-colorability of finite graphs. This expressive power persists even if rather stringent restrictions are imposed on the Henkin quantifiers. However, Henkin quantifiers of one extremely restricted sort, which we call narrow Henkin quantifiers, express, when applied to first-order formulas, exactly the co-NL properties of finite structures.

-2We use the customary notations and conventions of firstorder logic with equality, except that we also allow Boolean variables, a, B,.., which range over {true, 4alse}. These can easily be eliminated by coding, but the coding would make some formulas unnecessarily complex. Formally, we work with a two-sorted language whose second sort is to be interpreted as {true, false} in all structures and therefore need never be specified when we define a structure. We can view predicates as functions whose values are of this second sort. We frequently consider algorithms taking finite structures S (for a finite vocabulary a) as inputs. In such situations, we always assume that the universe of S is {O,1,.,n-}, for the appropriate natural number n, and that the structure is presented in some standard format whose length and n are bounded by polynomials of each other.

-3~ 1. What are Henkin quantifiers? In [He], Henkin introduced several new sorts of quantifiers, including partially ordered quantifiers as in the expression l ft(XlX2,2Ylty2) (1) Vx2 aY2 This expression means that for every xl there is a Y1 and for every x2 there is a Y2 depending only on x2 such that %(Xl'x2,y11Y2). More formally, it means that there are functions Y1(X1) and Y2(x2) such that VXXlVx2 X (X1lX2'Y1(Xl1) Y2(X2)) Henkin asked whether (1) is expressible in first-order logic (if c is) and, if not, whether first-order logic enriched by (vxlaYl) is recursively axiomatizable. Ehrenfeucht answered x2aY2/ both questions negatively by showing how to express the quantifier "For infinitely many x" in this enriched logic; his solution is given in [He]. Henkin quantifiers were extensively studied by Walkoe [Wa], who considered them to be strict partial orders Q = <AQ, <Q> where AQ is a finite set of ordinary first-order quantifiers and <Q describes the dependence relationships between the existential and universal quantifiers in AQ. The meaning

-4of such a quantifier Q is defined, as for (1), by Skolemization. For example, if AQ = {VXl,VX2 tvx3,ay1 Iay2 and < is given by Vxi <Q ayj when i P j as in the figure'WX, 3V 3>3 then QO(xl,x2,x3,yl,y2,y3) means that there are binary functions Y Y2' Y3 such that Vx1 Vx2 3x3 (X12X2,x3 Yl (X2 X3), Y2(X1,X3), Y3(X1,X2)) Notice that the only relevant information in <Q is what universal quantifiers precede what existential quantifiers. Walkoe calls this the essential order of Q, while Henkin considers, in effect, only orders where all of <Q is essential. The linearly ordered quantifier strings of ordinary first-order logic correspond to the linear Henkin quantifiers, in which <Q is linear or (since we can ignore the inessential part of <Q) the existential quantifiers are linearly pre-ordered by the inclusion relation on their sets of universal predecessors.

-5Following Walkoe, we call a Henkin quantifier standard if AQ is the disjoint union of chains (with respect to <Q) in each of which the last member is existential and all the others are universal. Such a quantifier, like that in (1), can be written as a sequence of rows each of which consists of universal quantifiers followed by a single existential quantifier. It is not difficult to express an arbitrary Henkin quantifier by means of a standard one. For example, if Q is the six-element quantifier above, then QO(Xl1X21x3,Yl,Y21y3) is equivalent to ( Vx2 Vx3 ay1 VxVx aY2 x1 = x x2 3 x 3 = x x3'Y1'Y 2 Y''Vx; Vx ay3 The concatenation of two Henkin quantifiers is equivalent to a single Henkin quantifier. For example, VX l 1 ay1 VX3 ay3 vx2 aY2 Vx4 aY4 is equivalent to the quantifier Q with domain { 1l',I X2, X3,V X4 Z Y1,a Y2'ay3, ay4} and aY1 preceded by v x1 3y2 preceded by Vx2, ay3 preceded by Vxl, yx2, and Vx3, and ay4 preceded by Vxl, Vx2, and Vx4

-6It follows easily that any formula built according to the formation rules of first-order logic but allowing positive occurrences of Henkin quantifiers can be rewritten as a single standard Henkin quantifier followed by a quantifierfree first-order formula. Walkoe showed [Wa, Theorem 4.3] that the expressive power of such formulas is exactly the same as the expressive power of existential second-order formulas. For example, the sentence aRVxyz [ (R(x,y) + R(x-z, yz) ) R(a,b)A — R(b,a) ] can be rewritten to make the arguments of R simply variables, aRVxyzuv [ (R(x,y)Au=x- zAv=y- z -)R(u,V) )(x=a1yb -R(x, y))A(x=by=a- 1R(xy) ) ], and can then be written in Henkin quantifier form as / V y 2ca\ V U VV S [(x = UA y = V + a = 8)^ (CAu = x-zA v = y-z + B) V z A (x aAy = b + a)A (x = bay = a la)]. Here a and a are Boolean variables. So the associated Skolem functions are actually binary predicates, and the conjunct (x = uAy = v + a = S) forces them to be the same predicate R. The remaining conjuncts are essentially copied from the previous version of the formula, and the last row of the quantifier should, if we insist on standard form, have a dummy existential quantifier added. The same rewriting procedure can be applied to any secondorder existential formula once it has been put into Skolem form so that all its first order quantifiers are universal.

-7In Theorem 1 below, we apply this result of Walkoe to give the simplest connection between Henkin quantifiers and complexity theory. Before stating the theorem, we introduce some useful terminology. By an Z-ary global predicate for a vocabulary a, we mean a function Ir assigning to each finite a-structure S an z-ary predicate S: S ( {true,false}. The decision problem for Ir is the problem specified by: Instance: A finite a-structure S and a e S Question: Does wrf (a) hold? Theorem 1. For any global predicate w, the following are equivalent. (1) The decision problem for r is in NP. (2) r is expressible by an existential second-order formula. (3) r is expressible by a formula Q% where Q is a Henkin quantifier and % is a quantifier-free first-order formula. Proof. The equivalence (1)- (2) is a theorem of Fagin [Fa], and the equivalence (2) - (3) is the theorem of Walkoe cited above. ID

-8~2. Henkin _ uantifiers and NP-complete 2roblems. Theorem 1 implies in particular that the global predicate defined by a formula Q%, with Q a Henkin quantifier and p a quantifier-free first-order formula, can be NP-complete. In this section, we investigate how complicated Q must be in order for this phenomemon to occur. Useful measures of the complexity of Q, for this purpose, are the number of rows (if Q is standard) and the type - individual or Booleanof the existentially quantified variables. For the sake of brevity, we call a Henkin quantifier mighty if, by applying it to a quantifier-free first-order formula, one can define an NP-complete global predicate. Linear Henkin quantifiers are, of course, not mighty unless L = P = NP, since first-order definable predicates are in L (logspace computable). We shall show in this section that almost any non-linear Henkin quantifier is mighty. In the first place, as long as the existentially quantified variables are individual ones ranging over the universe of the structure, rather than Boolean ones, all non-linear Henkin quantifiers are mighty. Theorem 2. The quantifier (Vxl awY) is mighty. V x2 aY2 Proof. In a vocabulary a with a binary predicate symbol E and three constant symbols 0, 1, 2, let 4 be the conjunction of

-9X1 = X2 + Y1 = Y2 Yl y 0 = IV Y1 = 2, and ExlX2 + Y1 Y2 Then, in any a-structure where 0., 1, 2 denote distinct elements, ay1\ holds if and only if the graph \X2 2 Y2 defined by E is 3-colorable. It is well-known [GJ] that 3-colorability is an NP-complete problem. I] Observe that, in the proof of Theorem 2, the existentially quantified variables ranged, in effect, over only a threeelement set, because of the second conjunct in %. If we introduce "almost Boolean" variables u, v to range over fO,1,2}, then the same proof shows: Corollary. Vx1 d ti is mighty. C Vx2 aV It is natural to try to obtain a similar result with Boolean variables c, 8 in place of the almost Boolean ones. We shall see later that this cannot be done without proving NL = NP. In the next two theorems, however, we almost achieve this replacement. Theorem 3. (Vx a=\ VY a8 is mighty.

-10Proof. Think of a Boolean circuit built from binary NAND-gates (where NAND means negated conjunction) as being a structure for the vocabulary a that consists of a constant symbol c (designating the output node) and a binary relation symbol I (where I (x,y) means that node x produces one of the two inputs to node y). We assume, without loss of generality, that the two inputs to each NAND-gate come from distinct nodes; at worst we just make two copies of every node. Then the NP-complete satisfiability problem - decide whether such a circuit has output true for some inputs - is Yx Ha given by the formula Vy.a where % is the conjunction of x=y+a=, y= z + y, z=x+ I(x,Z)A I(y,z)A x $ y - y = (A ), and X + a. (The third of the five conjuncts is redundant but was included for symmetry.) ) Theorem 4. (vix ac is mighty. Bvy ai) Proof. Think of Boolean circuits as in the previous proof except that, for each NAND-gate, we distinguish a left and a right input. Thus, a now contains c as before

-11and two binary predicates L and R whose disjunction would be the previous I. The satisfiability problem is described by Y x ~a a where c is the conjunction of x = y + (c *t ( 11 0)) X C + (- a)A (L(x,y)v R(x,y)) + u 0 O a A L(x,y) + V 3 1, and cA R(x,y) + u # 2 To see this, note that our formula asserts the existence of a function a = f(x) from the set S of nodes to {rue, false} (which is to describe the truth value computed at each node) and an auxiliary function vu = g(y) from S to {0,1,2 } with the-. following properties. First f is f alse wherever g is 0 and f is re wherever g is 1 or 2, so g completely determines f. Second, the value of f at the output node c is true. And finally certain values of g(y) are prohibited if f had certain values at the two inputs to y. The prohibitions resulting from each of the last three conjuncts of % are shown in the following table, along with the permitted values of g(y) and f(y) -

f (left input) f (right input) prohibited by conjunct g.(y) f(y)..... _ a(3).(4) (5) true true: 2 0 se ru.e fal 0 1 s2 falrse t- 0 2 1 trt f-alse ls 0 l or 2 true So our formula requires- the: NAND-gates to produce the correct outputs. D

-13~3. Narrow Henkin quantifiers and nondeterministic log space computability. In this section we study "narrow" Henkin quantifiers of the form (Vx a.C) where a, 8 are, as before, Boolean VY:a variables while x and y are tuples of individual or Boolean variables. We say that x and y are compatible if they have the same length and have variables of the same type at corresponding positions. We write x = y as an abbreviation for the conjunction of the equations x =yi between corresponding components of x and y provided x and y are compatible; if they are incompatible then x = y means false. For future reference, we exhibit the definition, i.e. the Skolem form, of l(x ag) O(X,y,a,8) it is:A B x y (x,y,A(x), B (y)) If x and y are compatible and % has the "equality bound" form (x = y + = B) ^(xYt,8), then this definition reduces to aA x V y ~ (xyA(x),A(y) ). It will be convenient for us to view 2-SAT, the satisfiability problem for propositional formulas in conjunctivre normal form with only two disjuncts in each conjunct, as a quantifier. Given propositional variables Po''''Ptn-1' consider a conjunction C of 2-disjunctions

-14of the forms piV pj, PiV- Pj,Pi V Pj and -Pi pj If we write p and - p in the equivalent forms (tue - p) and (false - p) then C can be described by a predicate R on {0,1,...,n-l} namely R(x,y,,a,) - C has a conjunct (a x)V (B * py) Conversely, with each such quaternary predicate R we associate the Boolean formula /{( px) V (aB -V py): R(x,y,ct,) }. Let (2-SAT x,y,a,S) R(x,y,a,B) mean that this Boolean formula is satisfiable. More generally, let (2-SAT xty,a,B) (x,y,ra,B) be interpreted as true in a structure S if and only if the Boolean formula A {(a *X pR)v (a - p ): 4(xy,ca,I,) holds in S} is satisfiable. Satisfiability of such a Boolean formula means that there exist suitable truth values for all the propositional variables p_ and p_. These truth values define predicates x y A and B on S, where A(x) holds if and only if px was assigned the value true, and similarly for B. (If x and y are compatible then A and B must coincide. ) Thus, the formula

-15(2-SAT x,y,a,B) %(x,y,a,B) is equivalent to A HaB Vx Vy[(x = y. (A(x)4-* B(y)))A^-(x,y,-A(x), —1B(y))]. If x and y are compatible, this reduces to aA Vx Vy — 3 (x,y,-1A(x),-1A(y)). The main result of this section is that narrow Henkin quantifiers are equivalent, in a suitable sense, to the quantifiers 2-SAT. Theorem 5. Narrow Henkin quantifiers and 2-satisfiability quantifiers are each expressible by means of the others. More precisely: C(i) ( Vx Ha) %(xy,,8) is equivalent to (2-SAT xy j,ta 1) (yA-ISA6A(x,y,lar, l8) ) (ii) (2-SAT'xy,,,BS) O(x,y,a,8) is equivalent to ('Vx a\ [(x = y + = a )A- (xy,-1,)-) ] Proof. Part (ii) is immediate, by comparison of the existential second order forms given above for 2-SAT and for narrow Henkin quantifiers. For part (i), we have the following list of formulas in which the equivalence of each

-16consecutive pair is clear either from the discussion above or from pure logic. (2-SAT xy,y6,, B) (yA^- dA- (x,y, Ta, -- )),:A aB Vxy Vy6 [(xy = y +(A(xy) B(y6)))A 7 (Y^A 6A — (xy,A(xy), B(y) ) ) ], aA aB Vxy Vy6 [(xy = y + (A(xy) -B(yS)))A (yA^-d + ((x,y,A(xy),B(y6)))], aA IB Vx Vy O(x,y,A(x true), B (y false)), a'B aB.' xVy j (x,y,A (x),B' (y)), 1yx c3\ 0(xy,a, ). O.. Y a J The following corollary is obtained by combining Theorem 5 with the well-known result [JLL] that the unsatisfiability problem for conjunctive normal forms with two literals per clause is complete, with respect to log space computable reductions, for the class NL of languages nondeterministically recognizable in log space. Corollary. All global predicates defined by formulas of the form Y vx xac\ (x,y atS), with first-order a, are V y a s in co-NL, and some of them, even with quantifier-free are complete for co-NL. n

-17In particular, the narrow Henkin quantifier is not mighty unless co-NL = NP (which would imply NL = P = NP ). In part (ii) of Theorem 5, we showed how to express 2-SAT by means of an equality bound narrow Henkin quantifier, i.e., the first conjunct after the quantifier requires the two Skolem functions to coincide. Combining this observation with part (i), we find that every narrow Henkin quantifier can be expressed by an equality bound one. Indeed, we find that (Vx aa) *(x,y,a,8) is equivalent to (VxY aca [(xy = y a = i) A (YA 6 + 8 (xya, l) )] This is easily verified directly (without 2-SAT), and the same method can be used to change any Henkin quantifier into an equality bound one, at the cost of introducing additional universally quantified Boolean variables. Immerman [Im] extended first-order logic by adding various operators, including the transitive closure operator TC, and obtained connections between these extended logics and various complexity classes. In the next theorem, we exhibit a close connection between TC and narrow Henkin quantifiers. Combining this connection with Immerman's results, we obtain a corollary characterizing, more precisely than Theorem 5 does, the expressive power of narrow Henkin quantifiers in logic with linear order.

-18Following Immerman, we write TC *(x,y), with compatible k-tuples x and y, for the reflexive transitive closure of the binary relation on k-tuples defined by the formula p. That is, TC p(x,y) is equivalent to the disjunction, over all n _ O, of the formulas azo.. Z (X=z A^ (Z Zl)^ (Zl 2)A. (n-l Zn) Zn=y); it is also equivalent to the second-order formula -l A[A(x)^A-A(y)/Au Vuv(A(u) A (u, ) + A(v))]. (Think of A as the set accessible from x.) The notation TC ~ (x,jy) is poorly adapted to situations where t contains additional variables as parameters or where terms are to be substituted for x and y. For example, if E is the edge relation of a graph, then TC E(x,y) means x is connected to y, so, to say that F(x) is connected to F(y), where F is a function from vertices to vertices, one would write TC E(F(x),F(y)); but this last formula also represents the transitive closure of the relation "F(x) is adjacent to F(y)", and this transitive closure amounts to "F(x) is connected to F(y) by a path all of whose vertices are in the range of F." Ambiguities like this can be avoided either by adopting a more accurate but longer notation, as in [Gu], or by ad hoc conventions. For our present purposes, it will suffice to adopt the convention that, if x and y are the specified k-tuples of free variables of', then TC'p(p,q), for terms p, q, means the result of substituting p for x and q for y in TC'p(x,y), not the transitive closure of (p,q).

-19Theorem 6. Narrow Henkin quantifiers and transitive closures can be expressed in terms of each other; positive occurrences of either can be expressed by neative occurrences of the other. Proof. To express TC in terms of a narrow Henkin quantifier, it suffices to rewrite the second-order form given above of the definition of TC as (Vu aca ((u=v - a = A)A (u=x -* a))A (u=y - a)A (a^A(uv) + S)] ~ For the other direction, we note first that any narrow Henkin quantifier can be expressed by one whose tuples of universally quantified variables are compatible: wy a s Vx'y ab where x' and y' are tuples of dummy variables compatible with x and y respectively. By a remark above, we can also assume, without loss of generality, that we are dealing with an equality-bound quantifier. We therefore wish to express, in terms of (negatively occuring) TC, a formula aA Vx Vy (x,A(x),y,A(y)) Think of this formula as asserting the existence of an assignment A of truth values A(x) to all tuples x of the appropriate type, such that all instances of %(x,A(x),y,A(y)) are true. If, for certain x, a, y, and I

-200 (x, a,y, B) is false, and if we assign x the value, then we must not assign y the value -1, for then we would not satisfy O(x,A(x),y,A(y)), so the value a for x forces the value 8 for y. The same holds if (y,-1B,x,a) is false. Let (x,a,y, B) be the formula - I (XOa,y ) v L v (y,'I r6 xa; whenever it holds, the value a for x forces the value 8 for y. Since this "forcing" is clearly a reflexive transitive relation on tuples xa, we see that xa forces ys whenever TC (x,l,y,8 ) holds (where xa and y8 are the specified tuples of variables for the application of TC ). In particular, if TC i(x,r,x —,ia) then x cannot be assigned the value, and therefore, for an assignment A of the desired sort to exist, it is necessary that ~: x [C TC * (x,a,x,-)TC f(xa,0,X,)]. We complete the proof of Theorem 6 by showing that this necessary condition is also sufficient. First, make the preliminary observation that o(x,a,y,B) and therefore also TC ~(x,a,y,B) are invariant under the operation of interchanging x and y while simultaneously interchanging and negating a and B In any structure, TC p defines a pre-ordering < (i.e. a reflexive transitive relation) on the tuples xa. Negating the last component of a tuple defines an anti-automorphism

-21of this pre-order (by the preliminary observation) of order two. Furthermore if the structure satisfies the necessary condition above, then we never have xM and x la each < the other. Lemma. Let (X,<) be a finite pre-ordered set, and let i: X -+ X be an order-reversing function such that every x e X satisfies i(i(x)) = x and either x i(x) or i(x) 4 x (or both). Then there is a subset T of X, closed upward for <, containing exactly one -of x and i(x) for each x e X Granting the lemma for the moment, we apply it to the set of tuples xa, pre-ordered according to TC, with i(xac) = x-la. We obtain a set T as in the conclusion of the lemma, and we define A(x) to be tre if and only if x true e T, or equivalently x fals * T. Thus, we always have x A(x) e T and x-1A(x) $ T. This assignment A has the desired property that N(x,A(x),y,A(y)) holds for all x and y. To see this, suppose x and y were a counterexample, i.e., -1 (x,A(x),y,A(y)) holds. Then i(x,A(x),y, -A(y)) would hold and, as i implies TC, we would have xA(x) < ylA(y). But xA(x) e T, y-lA(y) $ T, and T is closed upward, a contradiction. This completes the proof of Theorem 6, assuming the lemma.

-22Proof of lemma. We proceed by induction on the number of elements of X, the case X = 0 being vacuously true. If X $ 0, consider an arbitrary x e X. Replacing x with i(x) if necessary, we may assume x 4 i(x). Then we decide to put into (resp. out of) T all elements > x (resp. < i(x)); there is no conflict here, as x $ i(x). Note that an element y has been put into T if and only if i(y) has been put out of T. The set Y of elements whose membership is still in doubt is smaller than X (as x * Y). Apply the induction hypothesis to Y, with the restrictions of < and i, to get T' C Y satisfying the conclusion of the lemma for Y. Finally put all members of T' into T and put all members of Y - T' out of T It is easy to verify that T has all the required properties. C Remark. A compactness argument shows that the lemma holds without the hypothesis that X is finite. By "logic with linear order", we mean logic with an additional logical symbol <, which functions syntactically as a binary predicate symbol, and which is interpreted in every structure as the usual ordering of the universe { 0,1,.,n-l}. Immerman [Im] proved that the global predicates definable in first-order logic with linear order augmented by TC are exactly those that are in the log-space hierarchy L E*. He also proved that, if we allow only positive occurrences of TC, then exactly the NL global predicates are expressible.

-23The following corollary is obtained by combining these results with Theorem 6. Corollary. The global predicates definable in first-order logic with linear order augmented bynarrow Henkin quantification are exactly those that are in the lo -sPace hierarchy. If only positive occurrences of narrow Henkin quantifiers are permitted, then exactly the co-NL global predicates are definable. [

-24~4. Remarks (A) In the proofs of Theorems 2, 3, and 4, one can fairly easily reduce the vocabulary a that is needed. For example, if we take the Boolean circuits in the proof of Theorem 4 to be trees, then the two binary predicates L and R can be replaced by a single binary predicate, namely the union of L and R augmented by loops at the left sons of all nodes. We have made no serious attempt to determine the minimal vocabularies for which these results hold. (B) In ~2 and ~ 3 we used the type - individual or Booleanof existentially quantified variables as an essential ingredient in our classification of Henkin quantifiers according to might. It is natural to ask whether the results could be extended by taking into account the type of the universally quantified variables. Such an extension is easily obtained by observing that universally quantified Boolean variables can be eliminated in favor of additional rows in the quantifier. Specifically, (ac Vx y) a (,x,y, —.), where R represents the remaining rows of a standard Henkin quantifier, is equivalent to [V Xa Y Vx' y') ((,xy,.... x''..) ). Using this R elimination procedure together with the results of ~2 and ~3, we obtain the following characterization of the standard Henkin quantifiers that are mighty.

-25Theorem 7. Assume NL + NP. Let Q be a standard Henkin quantifier whose variables are either individual or Boolean. Q is mighty if and only if either it has at least three rows containing universally quantified individual variables or it has two such rows-and the existentially quantified variable in at least one of these two rows is an individual one. Proof. If the condition is satisfied, then Q has at Vx Ha Vx E l a least the expressive power of either V Y Ha or (y a Vz aY and is therefore mighty by the results of ~2. If the condition is not satisfied, then by eliminating universally quantified Boolean variables as above, from rows without universal quantifiers, we can rewrite any formula Q% as Q'' where Q' has, apart from rows consisting just of a single existential quantifier, either just one other row, or two other rows both of whose existentially quantified variables are Boolean. The existential quantifiers that are in rows without universal quantifiers can, without changing the meaning of the formula, be moved to the left, since ( ax) is logically equivalent to (ax) R. Thus, we can R rewrite Q'p' in the form a xQ"', where Q" consists of those rows of Q' that contain universal quantifiers. But, because of the limitation on such rows in Q', we know that Q" is either linear or narrow, so the global predicate defined by Q" %' is at worst co-NL. This complexity estimate is

-26preserved by first-order quantification, so the global predicate defined by ax Q" T' (and by Q0) is co-NL. Our assumption that NL $ NP prevents any co-NL predicate from being NP complete, so Q is not mighty. I (C) All our theorems have been about formulas in which a Henkin quantifier occurs at the beginning and is applied to a first-order (in fact quantifier-free) matrix. We remarked in ~1 that formulas built using the formation rules of firstorder logic but allowing positive occurrences of Henkin quantifiers can always be rewritten in the "Henkin prenex" form that we considered. It is natural to ask about the full logic, called H by Walkoe, obtained from first-order logic by adding Henkin quantification as an additional formation rule. This logic contains formulas with negative occurrences of Henkin quantifiers, like Vx1 ayl/ Vu1 av1 -YI 1. (Xl,X2,Yl Y2,U lu2, V11v2), \ X2 "aY2 VU2 a 2 which, by definition of Henkin quantifiers, means aY 9Y2 Vx,X2sV1PV2 aUl U2l1((xl x2.Y1 (XY) Y2(X2)UllU2( 2V1 (U1j'2 (U2)) The global predicate defined by this formula is in the class E2 of the polynomial time hierarchy [St]. Similarly, a formula of H containing n Henkin quantifiers defines a global predicate in the nth level of the polynomial time hierarchy. But, in fact, these global predicates are all

-27in 2rII2, by a result of Enderton [En, Theorem 2], which also applies to infinite structures. (D)Y The semantics of Henkin quantifiers treats existential quantifiers quite differently from universal ones. This is reflected in the fact that the dual - Q 1 of a Henkin quantifier is usually not a Henkin quantifier; applied to first-order formulas, -1Q - produces co-NP global predicates, not NP ones. It is natural to try to restore symmetry by returning to the symmetrical "games" with which Henkin introduces generalized quantifiers in [He]. If Q = <AQ,<Q) as in ~1, then the game for Q% is played as follows. One player, called a, assigns values to the existentially quantified variables; his opponent, V, assigns values to the universally quantified variables. When assigning a value to a variable x, a player knows the values of only those variables whose quantifiers precede that of x in <Q. A play of the game is won by a if and only if the chosen values of the variables make * true. Finally, Q - holds if a has a winning strategy and fails if V has a winning strategy. This definition can be made precise, and kept symmetrical, as follows. A strategy for a consists of functions Xi for all the existential quantifiers ( xi) in Q; the argument places of Xi correspond to the quantifiers (~yj) CQ ( xi). Strategies for V are defined symnetrically.

-28Given strategies for both players, we assign a value to each variable x. or yj occuring in Q by applying the corresponding function X. or Y. to the values assigned to the variables whose quantifiers occur earlier in < Q (This recursive definition of the values assigned to variables makes sense because <Q, being a partial order on a finite set, is well-founded.) The outcome, for the two given strategies, is a win for a (resp. V ) if these values for the variables make O true (resp. false). Finally, QO is said to hold (resp. fail) if there is a strategy for a (resp. v) which wins against every *strategy for V (resp. a). The price we pay for the symmetry of this definition is that a formula might neither hold nor fail; that is, there might be no winning strategy for either player. The simplest example of this phenomenon is given by (Vx) x = y a y in any structure with at least two elements. Although unpleasant, this lack of determinacy should not be viewed as pathological; it is the usual situation for games of imperfect information. Miklos Ajtai has suggested applying the von Neumann minimax theorem to these games. The theorem asserts the existence of a number p and a probability distribution Da (resp. D ) on the set of a's (resp. V's) strategies such that, if a (resp. V) chooses a strategy at random according to the distribution DH (resp. D ), then he

-29wins with probability at least p (resp. l-p), no matter what strategy his opponent uses. Ajtai suggested that the number p be viewed as a truth value for Qu. This truth value is 1 (resp. 0) if and only if Q% holds (resp. fails) in the sense defined above. Formulas which neither hold nor fail have intermediate truth values; the example ( Y x = y has truth value n in structures of cardinality n n

IL111111 1 I llllllllll II IkflllllllllL lllllllll lllll 3 9015 02229 1895 -30Bibliography [En] Herbert Enderton, Finite partially ordered quantifiers, Z. Math. Logik 16 (1970), 393-397. [Fal Ronald Fagin, Generalized first-order spectra and polynomial-time'recognizable sets, in Complexity of Computation, ed. R. Karp, SIAM-AMS Proc. 7 (1974), 43-73. [GJ] Michael Garey and David Johnson, Computers and Intractability, W.H. Freeman & Co. (1979). [Gu] Yuri Gurevich, Toward logic tailored for computational complexity, to appear in Proc. 1983 European Logic Colloquium in Aachen, Springer Lecture Notes. [He] Leon Henkin, Some remarks on infinitely long formulas, in Infinitistic Methods, Warsaw (1961), 167-183. [Im] Neil Immerman, Languages which capture complexity classes, Proc. 15th ACM Symposium on Theory of Computing (1983), 347-354. [JLL] Neil Jones, Edmund Lien, and William Laaser, New problems complete for nondeterministic log space, Math Systems Thery 10 (1976), 1-17. [St] Larry Stockmeyer, The polynomial-time hierarchy, Theoret. Como. Sci. 3 (1977), 1-22. [Wa] Wilbur Walkoe, Finite partially-ordered quantification, J. Symbolic Logic 35 (1970), 535-555.