THE UNIVERSITY OF MICHIGAN COMPUTING RESEARCH LABORATORY TOWARDI LOGIC TAILORED FOR COMPUTA''TIONALI COM PILXITY Yuri Gurevich CRL-TR-3-64 JAN UARY 1984 Room 1079. East Engineering Building Ann Arbor, Michigan 4-8109 USA Tel: (313) 763-8000

Toward logic tailored for computational complexity by Yuri Gurevich Computer Science The University of Michigan Ann Arbor, Mlichigan 48109 Abstract. Whereas first-order logic was developed to confront the infinite it is often used in computer science in such a way that infinite models are meaningless. We discuss the first-order theory of finite structures and alternatives to firstorder logic, especially polynomial time logic. Introduction Turning to theoretical computer science a logician discovers with pleasure an important role of first-order logic. One of the fashionable programming languages - PROLOG - is based on first-order logic; variants of first-order logic - Tuple Calculus, Relational Algebra, Domain Calculus - are used as query languages to retrieve information from relational databases; et cetera. The database applications of first-order logic are of special interest to us here. In this connection let us mention that relational databases are not a side issue in the data field. The relational data model together with the network and the hierarchical data models are "the three most important'data models', the models that have been used in the great bulk of commercial database systems" [UZ, Section 1.4]. The relational data model brought a Turing Award to its inventor E.F. Codd. The three query languages, mentioned above, were also introduced by Codd and are important: "A language that can (at least) simulate tuple calculus, or equivalently relational algebra or domain calculus, is said to be complete" [UZ, Section 6.1]. Some of the new applications of first-order logic are unusual in that only finite structures are of interest. In particular, relational databases can be seen as finite first-order structures (for the purpose of this paper), and the query languages, mentioned above, express exactly the first-order properties of relational databases. The question arises how good is first-order logic in handling finite 1Supported in part by NSF grant MCS83-01022

2 structures. It was not designed to deal exclusively with finite structures. In a sense the contrary is true. It was developed as a tool in Foundations of Mathematics, especially when mathematicians and philosophers confronted paradoxes of the Infinite. We do not question here the greatness of first-order logic of not necessarily finite structures. Taking into account how elegant, natural and expressive firstorder logic is, it is actually amazing that formulas true in all structures (of an appropriate vocabulary) are exactly the ones for which there exist proofs in a specific formal system. (Let us also recall the unique character of first-order logic [Lin].) But what happens to recursive axiomatizability, compactness and other famous theorems about first-order logic in the case of finite structures? We address this question in ~1. Our feelings about the answer are expressed in the title of ~1: Failure of first-order logic in the case of finite structures. In ~2 we address a certain ineffectiveness of famous theorems about first-order logic. Consider for example Craig's Interpolation Theorem: for each valid implication 4+- there is an interpolant 6 such that vocabulary(9)C vocabulary(P)nF vocabulary(W) and the implications 4+- and 0-+ are valid. No total recursive function constructs an interpolant from the given implication [Kr]. There is no recursive bound on the size of the desired interpolant in terms of the size of the given implication [Fr]. Moreover, weaken the interpolation theorem by replacing "the implications ~~O and G+- are valid" by "the implications ~+Q and 9+- are valid in all finite structures of appropriate vocabularies". Still there is no recursive bound on the size of the desired interpolant in terms of the size of the given implication. What is the use of criticizing first-order logic if we cannot come up with a reasonable alternative? We think here about applications where one needs at least the expressive power of first-order logic, like PROLOG or relational query languages. "It is the case that almost all modern query languages embed within them on of the three notations" [IJZ, Section 6.1]. (The three notations are the tuple calculus, the relational algebra, and the domain calculus.)

3 One would like to enrich first-order logic so that the enriched logic Fits better the case of finite structures. The first temptation of a logician would be to regain recursive axiomatizability. But no extension of the first-order theory of finite structures is recursively axiomatizable. (Satisfiability of first-order formulas on finite structures is recursively axiomatizable. But this axiomatizability provides only a criterion of existence of a formal proof for existence of a finite model. It is not interesting. The whole point of axiomatizability was to provide an existential criterion for a universal statement.) Another temptation is to consider second-order logic (without third-order )redicates or functions) or its fragments (like existential second-order logic) as an alternative to first-order logic. Confining ourselves to finite structures, we consider this alternative in ~3. Second-order logic is certainly elegant, natural and much more expressive than first-order logic. Second-order logic itself becomes more attractive in the case of finite structures: no nonstandard models, no distinction between the weak and the strong versions of second-order logic, etc. There is however one important - from the point of view of computer science - property of first-order logic that is lost in the transition to second-order logic. For every first-order sentence 0 there is an algorithm that, given a presentation of a structure S of the vocabulary of 1, computes the truth-value of P on S within time bounded by a polynomial in the cardinality ISI of S (and within working space bounded by log SI). In other words, first-order properties are PTIME (and LOGSPACE) computable. Second-order properties and even existential second-order properties are not PTIME computable unless P=NP. If one takes the popular point of view that feasible computations are PTIME bounded and that P is probably different from NP then second-order logic is not a good alternative to first-order logic. Let us mention that computer scientists do feel that first-order logic is unreasonably restrictive. PROLOG does have non-first-order features, and it was suggested to augment the essentially first-order query languages by different onerators preserving feasible computability of queries. Of course the notion of Feasibility varies with applications. From the point of view of PTIME computa

bility, the least fixed point operator LFP [AU] appeared to be especially import;alnt. It preserves PT I'Mi cmlllt;l)li i ty and has ^,reat express ive )ow(r. A natural idea arises to extend first-order logic in such a way that exactly PTIME (LOGSPACE, etc.) computable properties of structures are expressible in the extended logic. Chandra and Harel [CH2] considered the extension FO + LFP of first-order logic by LFP from that point of view and discovered that FO + LFP does not capture PTIME. It turned out, however, that FO + LFP does capture PTIME in the presence of linear order [IM1, Var]. In ~4 we discuss fixed points and logics with order (as a logical constant) tailored for PTIME. In ~5 we return to some of the famous theorems about first-order logic and consider whether their analogues hold in the case of logic specially designed for PTIME. More specifically, we consider the analogues of Craig's Interpolation Theorem, Beth's Definability Theorem and the Weak Beth Definability Theorem for polynomial time logic. These analogues happen to be equivalent to natural complexity principles whose status is unknown. A lot of interesting problems arise. Design a logic that captures PTIME even in absence of linear order, or prove that there is no reasonable such logic if PNMP. What is a logic? What is a complexity class? Can every reasonable complexity class be captured by a logic in the presence of linear order? Capture LOGSPACE, NLOGSPACE, LOG2SPACE, LOG2SPACEO PTIME, etc. in the presence of linear order. What are complexity tailored logics good for? Are complexity bounded programming languages useful? Some answers can be found in [Im2] and [Gu3]. Our terminology is more or less standard. We use the term "vocabulary" rather than "signature" or "similarity type", and we use the term "structure" rather than "model" or "algebraic system". Our vocabularies are always finite. Acknowledgements. I am very grateful to Andreas Blass and Neil Immerman for very useful discussions related to this paper.

5 ~1. lailure of first-order logic in the case of finite structures We examine famous theorems about first-order logic in the case when only finite structures are allowed. The terms formula and sentence will refer in this section to first-order formulas and first order sentences. As usual, a sentence is a formula without free individual variables. Recall that a formula ) is called valid (or logically true) if it is true in every structure of the vocabulary of (), a formula 4 (resp. a set D of formulas) is said to imply a formula i logically if 4 is true in every model of ) (resp. of D) whose vocabulary includes that of I, and formulas ),$ are called logically equivalent if each of them logically implies the other. We will say that a formula P is valid in the finite case if it is true in every finite structure of the vocabulary of ), a formula ) (resp. a set D of formulas) implies a formula in the finite case if 4 is true in every finite model of ) (respectively of D) whose vocabulary includes that of 4, and formulas 4, are equivalent in the finite case if each of them implies the other in the finite case. The Soundness and Completeness Theorem is formulated usually for a specific logical calculus. It states that a formula is valid iff it is provable in the calculus. The calculus-independent meaning of this theorem is that first-order logic is recursively axiomatizable, which boils down to the fact that valid formulas are recursively enumerable. Trakhtenbrot [Tr] proved that the formulas valid in the finite case are not recursively enumerable. Therefore first-order logic is not recursively axiomatizable in the finite case, and the Soundness and Completeness Theorem fails for any logical calculus in the finite case. Remark. Tiny fragments of first-order logic are not axiomatizable recursively in the case of finite structures. For example, let a be a vocabulary that consists of one binary predicate symbol. The 3V* a-sentences (i.e. the prenex a-sentences with prefixes 33Vn), that are valid in the finite case, are not enumerable recursively [Gul, Ko]. Summaries of results of that sort can be found in [(Gu2]. Goldfarb claims that even 32V a-sentences with equality, valid in the finite case, are not enumerable recursively [Go].

The Compactness Theorem for first-order logic states that if a set D of.formulas logically implies another formula tP then some finite subset of a logically imp)lies Ti.''he theorem fails in the finite case. Let for example D={(n:n>l} where every sentence 4n states existence of at least n different elements, and let 4 be any logically false formula. Then ~ implies' in the finite case; however no finite subset of ~ implies P in the finite case. The Craig Interpolation Theorem states that if a formula 4 logically implies a formula ip then there is a formula 6 (an interpolant) such that vocabulary(6)c_ vocabulary(t)nf vocabulary( ), ) logically implies 8, and 6 logically implies W. The interpolation theorem implies the Beth Definability Theorem that states the following. Suppose that a sentence )(P) defines an Z-ary relation P implicitly i.e. if P' is a new Z-ary predicate symbol then )(P) and C(P') imply Vx...Vx (P(x,...,x)< —>P'(xl,,x) ) Then there is an explicit first-order definition of the same relation i.e. there is a formula 0(xl,...,xE) such that vocabulary(6) Cvocabulary()(P)) - {P} and 4(P) logically implies Vx... Vx,(P(xl,....,x)< —>e(X...,)). If )(P) and P' are as in the antecedent of the Beth Definability Theorem then )(P)&P(xl,...,xQ) logically implies ((P') —->P'(xl,...,x9)), and the corresponding interpolant is the desired explicit definition. The same proof shows that the finite case version of the interpolation theorem implies the finite case version of the definability theorem. The Weak Definabilitv Theorem is the result of strengthening the antecedent of the Beth Definability Theorem. The antecedent of the Beth Definability Theorem states that for every structure of the vocabulary o=vocabulary(((P)) -{P} there is at most one relation P that satisfies 4(P). The antecedent of the Weak

7 Definability Theorem states that for every a-structure there is a unique relationP that satisfies (L(P). Theorem 1. The Craig Interpolation Theorem, the Beth Definability Theorem and the Weak Definability Theorem fail in the finite case. Proof. Let us recall the definition of the quantifier depth of a formula: q.d.(a quantifier-free formula)=0 q.d.(a Boolean combination of formulas a... a )=max{q.d;.(a),..,q.d. ( ) q.d. (Vx) =q.d. (3 xa)=l + q.d. (a). Lemma. (i) Suppose that a is a sentence in the vocabulary {<} of order, n is the quantifier depth of a, and A,B are finite linear orders of cardinalities A|I,IBI>2n. Then a does not distinguish between A and B i.e. A satisfy a iff B satisfies a. (ii) There is no sentence a in the vocabulary {V} such that an arbitrary finite linear order S satisfies a iff the cardinality |IS is even. (iii) There is no formula e(x) in the vocabulary {<} such that if S is a finite order al<a2<...<a then {x:S D 9(x)}={ak:k is even}. Proof of Lemma. (i) We use the Ehrenfeucht games [Eh]. It suffices to exhibit a winning strategy for player II in the Ehrenfeucht game G (A,B). Without loss of generality no element ispicked twice during the game. The proposed strategy is to ensure the following. Let al<a2<...<ak and bl<b2<...<bk be the elements chosen in A and B respectively during the first k steps of the game. Let AO,A1,...,A be the segments [min(A),al], [a,a2],...,[ak, max(A) of A, and let BO,B,...,Bk be the respective segments of B. Then for every i=l,...,k the elements ai,bi were n-k chosen at the same step of the game, and either |Ail=lBi| or IAi|,Bil>2n for O<i<k, and either 1Ai.=|Bi. or |Ai|,|Bil>2nk for i~{0,k}. (ii) The statement follows from fi).

8 (iii.) If -)(x) defines the set of even elements in every finite linear order then the sentence 3x(x is maximal and O(x)) holds in an arbitrary finite linear order S iff |S| is even.0 Since the interpolation theorem implies the definability theorem and the definability theorem implies the weak definability theorem, it suffices to refute the weak definability theorem. It is easy, however, to construct separate counterexamples to all three theorems. Write a sentence a stating that < is a linear order. let P,Q be distinct unary predicates. Write a sentence P(P) in the vocabulary {<,P} such that if S is a finite linear order al<a <...<a and S satisfies B(P) then 1 2 n {x:S 0 P(x)}={ak:k is even}. (Write that P does not contain the first element, and the successor of an element x belongs to P iff x does not belong to P.) Obviously ac (P)&P(x) implies (Q) ->Q(x) in the finite case. If the interpolation theorem were true in the finite case then the interpolant would violate the statement (iii) of the Lemma. Obviously, aG&(P) defines P implicitly in finite structures. If the definability theorem were true in the finite case then the explicit definition of P would violate the statement (iii) of the Lemma. Finally, the sentence (ax -> 3(P))4(,ca ->-3xP(x)) defines P uniquely in the finite case. If the weak definability theorem were true in the finite case then the explicit definition would violate the statement (iii) of the Lemma. Theorem 1 is proved. Remark. The formula g(P) in the proof of Theorem 1 can be simplified if we use an individual constant for the first element in the order and an additional binary predicate symbol for the successor relation. The Lemma remains true for the is changed n+l richer vocabulary if 2 is changed to 2 (with an obvious change in the proof). A sentence ( is said to be preserved under substructures if every substructure of a model of ~ is a model of ). According to the Substructure Preservation Theorem [CK, ~3.2], a sentence C is preserved under substructures iff it is logically equivalent to a universal sentence.

9 Theorem 2 (Tait). The Substructure Preservation Theorem fails in the case of finite structures. In other words, there is a sentence ( such that any substructure of a finite model of ( is a model of X, yet ( is not equivalent to any universal sentence in the finite case. Proof. Let (1 be the universal closure of the conjunction of the following formulas (where x<y abbreviates x=y V x<y): (x<y & y<z) -> x<z, - (x<x), x<y v y<x, O<x, [S(x,y) & y:O] -— > [x<y & (z<x v y<z)], S(x,O) -> y<x. A) states that < is a linear order, 0 is the minimal element, and Sxy implies that either y is the successor of x or else x is the maximal element and y=O. Let (2 be Vx3y S(x,y), and let ( be 1 & ('2 ->3xP(x)) where P is a unary predicate symbol. First we check that 4 is preserved under substructures of finite models. Suppose that A is a finite model of p and B is a substructure of A. Then B contains 0 and satisfies (1. If B does not satisfy'2 then it satisfies the second conjunct of ( by default. If B satisfies P2 then B=A and B satisfies 4. Next, let a be a sentence Vxl...VxnS(xl,....,xn) where B is quantifierfree. Let A be a model of P1 & P2 such that the vocabulary of A includes that of a,A has at least n+2 elements and P is empty in A, so that p fails in A. If a is true in A then it is not equivalent to ( in the finite case. Suppose that a is false in A. Then g(cl,...,c ) is false in A for some c,...,c. Choose dcA different from O,cl,...,c, and put d into P. The resulting structure B satisfies (. However 6(cl,...,c ) remains false in B. Hence a is false in B, and a is not equivalent to c( in the finite case. I did not perform an exhaustive study of important theorems about first-order logic in the finite case. Some theorems become meaningless in the finite-case.

10 Some theorems do survive: the game criterion for two'structures to be indistinguishable by sentences of a given quantifier depth [Eh], composition theorems of the sort found in [FV], etc. Moreover, some theorems were specifically proved for the finite case: the 0-1 Law Theorem for example [GKLT, Fa]. Too often however we see the familiar pattern: the proof uses a kind of compactness argument and the theorem fails in the finite case. Sometimes a weaker version of the theorem in question survives. Here is an example. Recall that an V*3* sentence is a prenex sentence with a prefix m 3n. Theorem 3 (Compton). Let c be an V* 3* sentence without function symbols. If q is preserved y substructures of its finite models then it is equivalent to some universal sentence in the finite case. Proof. First let us recall a relativized version of the Substructure Preservation Theorem: Let TO be a first-order theory, and a be a sentence in the language of TO. Suppose that for every model A of To and for every substructure B of A that is a model of TO, if A is a model of a then B is a model of a. Then a is equivalent in To to some universal sentence. The usual proof of the Substructure Preservation Theorem is easily relativizable: just take A to be the set of all sentences, that are equivalent in T to universal sentences, in the proof of Theorem 3.2.2 in [CK]. In our application TO is the first-order theory of finite structures of the vocabulary of q. Let A be a (possibly infinite) model of To that satisfies q. Let B be a substructure of A that is also a model of T. It suffices to prove that B satisfies P. First, we show that an arbitrary finite substructure A0 of A satisfies P. Write an existential sentence a stating existence of elements that form a structure isomorphic to A. The sentence ac& has a finite model A1: otherwise TOF C(a&) which contradicts the fact that A is a model of TO, a and ~. Since A1 satisfies a it has a substructure isomorphic to A0. Now use the fact that v holds in A1 and is preserved by substructures of finite structures.

11 Recall that 4 is Vx1...vx3 Y1.. 3 YnM,.(x1..xmYl'..Yn) for some quantifier-free formula Q. We argue by reductio ad absurdum. Suppose that B fails to satisfy T. Then there are elements al...,a such that the universal formula Yl...V Ynn(al',... amYl...'Yn) holds in B. This universal formula logically implies -n and holds in the substructure Ao={a,...,a } of B (because universal formulas are preserved by substructure). Thus a finite substructure of A fails to satisfy ( which is impossible. M Note that the counterexample to the Substructure Preservation Theorem, constructed in the proof of Theorem 2 is logically equivalent to an 3*V* sentence. Thus Theorems 2 and 3 delimit each other. Historical Remarks. I am not the first to discover that Craig's Interpolation Theorem and Beth's Definability Theorem fail in the finite case. (A question of Steve Simpson led me from Craig's Theorem to Beth's Theorem.) Ron Fagin knew about the failure. It was probably discovered long ago though I do not have any reference. Theorem 2 was proved in [Ta]. The proof above is due to Gurevich and Shelah (that were not aware [Ta]). Theorem 3 was formulated and proved by Kevin Compton in a letter [Co] to me.

~2. An ineffective side of first-order logic We saw in ~1 that Craig's Interpolation Theorem, Beth's Definability Theorem, the Weak Definability Theorem and the Substructure Preservation Theorem fail in the case of finite structures. One may be tempted to allow infinite structures (to allow infinite relational databases in database theory) in order to regain these wonderful theorems; see [Va] for example. There is however a catch there. Let us speak, for example, about the weak definability theorem. Even if you happen to know that P(P) implicitly defines a relation P in every - finite or infinite - structure and even if you are interested in an explicit definition of the same relation P in finite structures only, still constructing the desired explicit definition from the given implicity definition may be most problematic. This is the point of the present section. Again, the terms formula and sentence mean first-order formulas and first-order sentences. The length of a formula ( is denoted ||. So then, how constructive are the wonderful theorems mentioned above? In a certain sense the interpolation theorem is very constructive. The desired interpolant for a valid implication (1+-) is easily constructible from a proof of (C+) in an appropriate predicate calculus [Cr]. In the same sense the definability theorem is very constructive because the desired explicit definition can be found as an interpolant for an implication that is easily built from the given implicit definition, see 51. There are also partial recursive functions f and g such that if (p$) is a valid implication then f(q-'l) is an interpolant for (4-t+), and if p(P) is an implicit definition of a relation P then g(P(P)) is an explicit definition of the same relation. However, there are no total recursive functions f and g with the same properties [Kr]. Moreover, there are no total recursive functions that bound the length of the desired interpolant or explicit definition in terms of the length of a given formula [Fr]. Even the weak definability theorem is ineffective in that sense: the length of the desired explicit definition is not bounded by any recursive function of the length of a given implicit definition. The next theorem gives a straightforward proof of this result of Friedman and strengthens it in a way related to finite structures.

13 Theorem 1. For every total recursive function f there is a sentence'( P) such that (i) 4(P) implicitly defines a relation P in every structure of the vocabulary =vo ularlary((P))-{P}, and (ii) if 4 is an explicit definition of the same relation P in every finite a-structure, then ||>f(|I(P)). Proof. Given a total recursive function f we construct an auxiliary total recursive function g. The exact definition of g will be given later. Let M be a Turing machine that computes g. We suppose the following about M. Its internal states are q0,..,qm here q0 is the initial state and is the halting state. The only tape of M is one-way infinite, the tape alphabet is {0,1} where 0 is also the blank. An instruction of M is a 5-tuple qiaqjbd where d~{-l,0,l} indicates whether the head of M will move to the left, stay still or move to the right. If at moment 0 the state of M is q0, the head is in cell 0 and the tape word is 1n then M will eventually halt in the halting state q with the tape word 1g(. In order to describe computations of M by formulas we introduce unary predicates qO(t),...,qm(t) to indicate the state at moment t, a binary predicate H(x,t) to indicate that the head is in cell x at moment t, a binary predicate C(x,t) to indicate that the content of cell x at moment t is 1, and unary predicates D l(t), Do(t), D (t) to indicate the move of the head that the machine is instructed at moment t to perform. In order to use all these predicates properly, we need binary predicates <,S and an individual constant 0. Let a sentence $0 state that < is a linear order, 0 is the minimal element, S is the corresponding successor relation, and every nonmaximal eletent has a successor. A sentence $1 describes the initial configuration of M with the input n. It is the conjunction of sentences q0(0), H(O,0), 3x...3x n[x0=0 S( and S:xx ) and A C(xi,0) and C(x,O)], VxVy[iC(x, 0) and x<y imply C(y,0) ].

14 A sentence (2 describes one computational step. It is the universal closure of a quantifier-free conjunction. Every instruction qiaqjbd contributes the conjunct [qi(t) & H(x,t) & Ca(x,t) & S(t,t') implies qj(t') & Cb(x,t') & Dd(t)] where C1,CO are C,-r.C respectively. In addition the quantifier-free part of has the following conjuncts: ["qi(t) or iqj(t)] for O<i<j<m, [H(x,t) and H(y,t) imply x=y], [-'Dd(t) or'D (t)] for -l<d<e<l, [Do(t) & H(x,t) & S(t,t') implies H(x,t')], [Dl(t) & H(x,t) & S(t,t') & S(x,x') implies H(x',t')], [D1 (t) & S(t,t') & S(x,x') & H(x',t) implies H(x,t')], ["H(x,t) and S(t,t') imply (C(x,t')< —>C(x,t))]. A sentence (3 describes what happens after halting. It is the universal closure of the formula [qm(t) and t<u imply (i.m'q.i(u) and -H(x,u) and -C(x,u) and -lD( i<m -l<d< 1 d(u) Lemma. For every model A of 0 and for every natural number n there are unique predicates q0'...,'qHC,'D'D O1D on A that satisfy 1n&2& 3. Proof is straightforward. In particular, the sentences 0'1'2 and (3 imply that for every t there is a unique x with H(x,t): the head does not slip from the tape because M computes a total function, and if D1(t), H(x,t), S(t,t') hold then x<t<t' and there is x' such that S(x,x'), H(x',t') hold. Let P be a ternary predicate symbol. Write a sentence (n(P) that states the following. If 0 fails or there are at most m+3 elements then P is empty. If holds and there are more than m+3 elements then (a) ('1 2,'3 hold where qi(t),Dd(t),H(x,t),C(x,t) abbreviate P(O,i,t), P(O,m+2+d,t),P(l,x,t),P(2,x,t) respectively, and.(b) P(O,x,t) fails for x>m+3, and P(x,y,t) fails for x>2.

15 When numbers 1,2,etc. appear as arguments of P they mean of course the successor of 0, the successor of the successor of 0, etc. It is easy to see that n implicitly defines a relation P in every structure of the vocabulary a={<,0,S}. Let n be an explicit definition of the same relation in every finite a-structure. Note that 1 and the quantifier depth of n do not depend on the choice of g. Define g(n) tobe the power of 2 such that log2g(n)=f(,n +n)+q.d. (dn) +1. n1 is the only part of n that depends on n. It occurs in (n only once. Thus the number k= |n1- lnlI does not depend on n. Let f=kk and =k. Then log2g(k)=f(|l|)+q.d. ()+l. Let a be the sentence [~(W) and 3tqm(t)]. Every model of a reflects the whole computation M and has at least g(k) elements. By the Remark following the Lemma in ~1, g(k)<2l+q.d.(). Hence q.d. (a)+l>log2g(k)=f(I|) +q.d. () +1 But q.d.(a)<q.d.(4)+q.d.(4). Hence | P>q.d.(G)>f(l )..O Remark 1. It is easy to make the relation P of Theorem 1 unary. The idea is to use auxiliary elements to code triples of real elements. Remark 2. Mundici exhibits in [Mu] short valid implications ((+-) whose interpolants are enormously long. The proof of Theorem 1 can be used for analogous purposes. Theorem 2. For every total recursive function f there is a sentence $ such that (i) P is preserved by substructures, and (ii) if i is a universal sentence that is equivalent to P in every finite structure of the vocabulary of n then I|l>f( | |). Proof. Let f be a total recursive function. As in the proof of Theorem 1, let g be an auxiliary total recursive function (specified later) and let M be a Turing machine that computes g. Once again we describe computations of M by

16 first-order sentences. However, we take some additional care to make the desired description preserved under substructures. Instead of the sentence )0 in the proof of Theorem 1 we use sentences 1',2 from the proof of Theorem 2 in ~1. We call them {01 and 02 here. We split the sentence n from the proof of Theorem 1 into a conjunction Olln2 where (12 is the existential conjunct of (f and {11 is the conjunction of the two other conjuncts of (n Let ( be the sentence &01 & {11 & ~2 & ~3 & [~02 & &12+3t-x(qm(t) & x<t & Q(x))] where {2 and (3 are the sentences from the proof of theorem 1 and ( is a new unary predicate. First we check that every (n is preserved by substructures. Let A be a model of n. Every substructure B of A contains 0 and satisfies the sentences {01'-112l',23 because universal sentences are preserved by substructures. If B does not satisfy 02 or n12 then it satisfies the last conjunct of n by default. Suppose that (n satisfies o02 and n12' Since B satisfies 02 it is closed in A under successors. If A is finite then B is equal to A and satisfies (. Suppose A is infinite. Then B includes the least substructure of A closed under successors whose elements can be identified with natural numbers in the obvious way. Since B satisfies the existential sentence 2 the 12 structure A satisfies {n2 too. It is easy to see that A reflects the whole computation of the machine M on input 1. If M halts at moment T(n) then qm(T(n)) holds in A. In virtue of (3 there is no element u>T(n) in A that satisfies qc. Since A satisfies n there is some x<T(n) in A that satisfies Q. Both T(n) and x belong to B; hence B satisfies (n. Note that f2 does not depend on the choice of g. Define g(n)=f(|l n2+n). 12 12 Since fn2 is the only part of n that depends on n, the number k= lnl -I1P2I Since 212 k does not depend on n. Let (=(. Then g(k)=f(|1(). The computation of M on input 1 halts at certain moment that will be denoted T(k). Finally let P be a universal sentence Vxl...~Vxz'(xl,...,x9) that is equivalent to ( in the finite case. Here (' is quantifier-free. Let A be the model of {01 & {02 & 11 & (l2 & (2 (P3 with the universe (O,1,...,T(k)) and

17 the intended interpretation of the predicates. First we define Q to be empty in A. The resulting structure A0 does not satisfy ); hence it does not satisfy W and -P'(cl,...,cY) holds in A0 for some c1,...,c. If Z<T(k) choose cEA-{O,cl,...,c } and put c into Q. The resulting structure A satisfies - yet cl,..,ct still witness failure of i in Al which is impossible. Thus |^|9>T(k)>k).gk)>f(|I|). a

18 ~3. First-order logic versus second-order logic In spite of the criticism in Sections 1 and 2, first-order logic is still a very good logic even in the case of finite structures. It is not without reason that first-order logic is used in computer science. It is elegant, natural and fairly expressive. However, if elegance, naturality and expressiveness are that important why wouldn't we turn to second-order logic? Second-order logic is elegant and natural as well, and it is much more expressive. Second-order logic is not very popular among logicians. The objection against second-order logic is that it isnot well manageable. However some fragments of second-order logic are much better manageable. One of them is weak second-order logic, which allows quantification over finite predicates only. In the finite case, of course, there is no difference between the two versions of second-order logic. As we saw in ~1 the theorems that made first-order logic so much preferable to second-order logic often fail or become meaningless in the finite case. Is there any important advantage of first-order logic versus second-order logic in the finite case? We take a computational point of view and answer this question positively. Proviso 1. The term "structure" refers to finite structures if the contrary has not been stated explicitly. A structure will be viewed as certain data, as an input to algorithms. A seeming difficulty is that elements of a structure are not necessarily constructive objects. We are interested however in the isomorphism type of a given structure rather than in the nature of its elements. Recall that IS| is the cardinality of a structure S. Proviso 2. The universe of a structure S consists of numbers 0,1,...,ISI-1. Proviso 2 by itself does not turn structures into inputs. We still have to choose a way to represent basic relations and functions. For example, a graph (V,E) may be represented as the lexicographically ordered list of edges or as an array A(ii,j) where A(i,j)=l if (i,j)~E and A(i,j)=O otherwise. Proviso 3. A reasonable standard way to represent structures is chosen.

19 We introduce global predicates. Let o be a vocabulary. An Z-ary a-predicate is a function T that assigns to each a-structure S an 9-ary S predicate ir on S. (The superscript S will be usually omitted.) A zero-ary a-predicate TT assigns a truth value to each a-structure and therefore can be S viewed as the set {S: S is a a-structure and T is true}. Every first-order formula in the vocabulary a with Z free variables gives an Z-ary a-predicate. A global predicate is a a-predicate for some a. Examples. Let a={E} where E is a binary predicate symbol. Note that a-structures are graphs. The first example is a binary a-predicate W1 such that for any graph G and any elements x,y of (;, Tl(x,y) holds in G iff there is an E-path from x to y. A more usual way to describe 71 is just to say that T1 is the binary a-predicate "There is an E-path from x to y". The second example is the set T2 of symmetric graphs. In other words, T2 is a zero-ary a-predicate such that T2 holds in a graph G iff G is symmetric. Note that every relational query is a global predicate. With each global predicate T we associate the problem of computing (or recognizing) TV. It is a decision problem. An instance of this decision problem is a pair (S,x) where S is a structure of the vocabulary of Tr and x is a tuple of elements of S whose length is the arity of T. The corresponding question is whether w(x) holds in S. In order to avoid trivialities we suppose that the length of the presentation of S is at least IS|. Theorem 1. A Boolean combination of PTIME recognizable global predicates is a PTIME recognizable global predicate. If V(x,...,xQ,y) is an (Z+l)-ary PTIME recognizable global predicate then 3yT(xl,...,xy,y) is an Z-ary PTIME recognizable global predicate (with an obvious meaning). Every first-order global predicate is PTIME recognizable. Proof. The first statement is obvious. The compute the truth value of 3yir(x,y) in S compute successively the truth values for TT(x,O),7T(x, ),...,'T(x, IS-l) in S. Since atomic first-order predicates are PTIME computable (here

20 we need reasonable standard representationa of structures), the third statement follows from the first two. Some second-order global predicates are NP-complete. For example, the set of 3-colorable graphs - a well-known iP-complete set - is definable by a second-order sentence 4X3Y3Z?(X,Y,Z) where X,Y,Z are unary predicate variables and I is first-order. Attaching little gadgets to vertices it is easy to construct an NP-complete set of graphs definable by a second-order sentence AX@(X) where X is a unary predicate variable and ip is first-order. Thus there are second-order global predicates that are not PTIME recognizable unless P=NP. It is almost a consensus in Theoretical Computer Science that PTIME computations are feasible wherease superpolynomial time computations are intractable, see [GJ], [HU]. In particular, Hopcoft and UJllman write the following. "Although one 57 might quibble that an n step algorithm is not very efficient, in practice we find that problems in P usually have low-degree polynomial time solutions". Thus first-order global predicates appear to be feasibly recognizable, whereas recognizing a second-order global predicate may be intractable. From our point of view, explicit PTIME recognizability is a decisive advantage of first-order logic versus second order logic. Remark. Theorem 1 remains true if "PTIME" is replaced by "LOGSPACE". The same proof proves the new (and stronger) version of the theorem: just represent numbers in binary. Theorem 1 and the stronger version of it are well-known.

21 ~4. Fixed points and polynomial time logic Provisos 1-3 of ~3 are in force. As we saw above in ~3, first-order global predicates are PTIME computable and even LOGSPACE computable. Unfortunately neither of these two statements can be reversed. For example, the property of graphs to be of even cardinality is recognizable by an obvious algorithm in linear time and logarithmic space. In virtue of the Lemma in ~1 this property is not first-order. A natural idea arises: to augment first-order logic by additional operators in order to express exactly the PTIME (LOGSPACE, etc.) computable global predicates. This is the idea reflected in the title: given a complexity level to tailor a logic expressing exactly the global predicates computable within the complexity level. Neil Immerman uses the word "capture" [Im2]. The problem is to capture a given complexity level by logical means. This section is devoted mainly to logic tailored for PTIME. Remark. Actually itmakes sense to generalize the notion of global predicate to the notion of global function and try to capture exactly the global functions computable within a given complexity level. Restricting attention to global predicates is even ridiculous if we see our-logic as a notation system for algorithms or a potential programming language. Just imagine a programming language such that each program outputs only a boolean value. Global functions and functional (rather than predicate) logics are explored in [Gu3]. Let us start with a note that first-order expressible global predicates apparently do not form a natural complexity class. They certainly do not form a complexity class defined by Turing machines with bounds on time and/or space (see again the even cardinality example). A computational model which is much closer to first-order logic is that of uniform sequences of boolean circuits of constant depth, unbounded fan-in, and polynomial size. Modest extensions of first-order logic do capture natural circuit complexity classes, see [Im2] and especially [GL] in this connection.

22 If we consider NP, co-NP and higher levels of the polynomial hierarchy [St] as genuine complexity classes then second-order logic and some of its natural sublogics do capture complexity classes. (When we speak about second-order logic we suppose that there are np third-order predicates or functions.) Recall that an existential second-order formula is a second-order formula =3X1...3Xk3X where 4 1 k is first-order and X1,...,Xk are predicate (or function) variables. The formula p may have free predicate and function variables as well as free individual variables. Theorem 1. A global predicate is computable in polynomial time by a nondeterministic Turing machine if and only if it is expressible by an existential secondorder formula. Theorem 1 is due to Fagin [Fal] and is readily generalizable to capture co-NP and higher levels of the polynomial hierarchy. Actually Fagin did not seek to characterize NP. It was just the other way around. He sought to characterize existential second-order sentences (generalized spectra in his terminology). Theorem 1 grew from investigations on spectra.of first-order sentences [Be, JS', Fal, Bo]. It looks pretty obvious today, and nondeterministic polynomial time computable global predicates are not necessarily feasible. However existential second-order logic does capture exactly the nondeterministic polynomial time computable global predicates and this fact inspired attempts to capture in a similar way deterministic PTIME computable global predicates. (About extending Fagin's result to richer logics and higher complexity classes see [St] and [CKS].) Meantime Codd proposed the relational database model and used variations of first-order logic (relational algebra, relational calculus) as query languages [UZ]. The relational model was a big success. However, the first-order query languages were proven to be too restrictive in many applications. Attempts were made to enrich those languages by additional operators, most notably by the transitive closure operator [ZQ] and the least fixed point operator [AU]. The transitive closure of a binary global predicate c(x,y) of some vocabulary a is a global a-predicate 8(x,y) such that for every a-structure S the

ZJ relation is the transitive closure relationelation a. More generally one can s;peI)k;lo(Lttt the tratlnsi. tive clostlr';e ()' a global lpredi'iatuc i (x, y) whcre x, y iarc tuple of individual variables of the same length [Im2]. In addition to x and y, a may have individual parameters. First-order expressible global predicates are not closed under the transitive closure operator; see Appendix 2. In a conversation with Andreas Blass the question of notation for the transitive closure of a(p,x,y) was raised. The naive notation TCa(p,x,y) is ambiguous. A possible unambiguous notation is TC(x,y; a(p,x,y),u,v) or TC- -(a(p,x,y),u,v). x, y Here x and y are tuples of bound variables, p is a tuple of parameters, and u,v are tuples of new free variables. Let us define the least fixed point operator for global predicates. It will be convenient to view global predicates as global sets: a global Z-ary predicate a of a vocabulary a assigns a set aS 6S to each a-structure S. We order global S S ~-ary a-predicates by inclusion: a<8 if aSc for every a-structure S. We say that a global a-predicate a is empty if aS is empty for every a-structure S. Definition. Let a be a vocabulary, P be an additional predicate variable of some arity Q, and 1(P) be a global Z-ary'predicate of the vocabulary aU{P}. View U(P) as an operator that, given a global Z-ary a-predicate a, produces a global Z-ary a-predicate r(a). A global Z-ary a-predicate a is a fixed point for TT(P) if a=ir(a), and a is the least fixed point for Tr(P) if it is a fixed point and a< for every fixed point 0 for T(P). Recall the notion of monotonicity of a first-order formula in a predicate variable defined in Appendix 1. This notion obviously generalizes to monotonicity of a global predicate in a predicate variable. Claim 1. Let a,P,Q and Ir(P) be as in the definition above. Suppose that rr(P) is monotone in P. Then there is a unique least fixed point for Tr(P). Moreover, let a0,a1,a2,... be global 9,-ary a-predicates such that aO is empty and every am+l equals 7r(a ). If 8 is the least fixed point for Tr(P) and S is

24 a a-structure then PS=tS where m=|SI. Thus the least fixed point for T(P) is PTIME computable if T(P) is. The proof is clear. The claim appears in [AU] in terms of relational algebra. A transfinite induction generalizes the claim to infinite structures. In either form the claim is a special case of the classical theorem of Tarski [Tar]. Example 1 [AU]. The transitive closure of a global predicate E(x,y) is the least fixed point with respect to P for E(x,y) v 3z[P(x,z) S P(z,y)]. Example 2. The semigroup generated by a set A is the least fixed point with respect to P for A(x) v 3y3z[P(y) & P(z) & x=y*z] A possible notation for the least fixed point for a global Z-ary predicate T(P) with free individual variables x1,...,xa is LFP(P,x1,...,xQ; T, Y1,...,y). It reflects the fact that LFP binds P and xl...,xp. The new individual variables Y1....,y are free. By the definition, LFP applies only to global predicates that are monotone in a given predicate variable. By Claim 1 in Appendix 1 the decision problem whether a given first-order formula is monotone in a given predicate variable, is unsolvable. This poses a difficulty in defining the extension of first-order logic by LFP. To overcome this difficulty Chandra and Harel [CH2] use positivity instead of monotonicity. Let FO + LFP be the extension of first-order logic by the following formation rule. (For the sake of definiteness we assume that substitution of terms for free occurrences of individual variables is one of the first-order formation rules.) LFP formation rule. Let P be a predicate variable of some arity Z and let P(P,x1,...,x) be a well-formed formula. If all free occurrences of P in 4 are positive and y,...y,Y y are new individual variables then

25 is a well-formed formula. All occurrences'of P and xl,...,x9 in the new formula are bound. If Q is a predicate variable different from P then every free (resp. bound) occurrence of Q in P remains free (resp. bound), and every positive (resp. negative) occurrence of Q in. remains positive (resp. negative). The only occurrences of individual variables Y1,'...,Y in the new formula are bound. (~ may have individual parameters. They remain free.) The meaning of the new formula is that the tuple (Y1,...,) belongs to the least fixed point for V(P,xl,...,x). Remark. Allowing individual parameters does not increase the expressive power of FO + LFP. For example, the formula LFP(P,y; E(u,y) v 3z(P(z) & E(z,y)), x) is equivalent to the formula LFP(Q,w,y; E(w,y)v 3z(Q(w,z) & E(z,y)), u,x). More generally, LFP(P,y; 4(P,u,y), x) is equivalent to LFP(Q,w,y; C(Qw,wy),u,x) where Q (z)=Q(w,z). However, parameters may be useful from the computational point of view. Sometimes logicians speak about logic with equality. In those cases the equality relation is a logical constant. The equality sign is interpreted as the identity relation on the elements of a given structure and it is not listed as a member of a given vocabulary. By Proviso 2 our structures are built from natural numbers. This allows us to introduce the natural order of elements as a logical constant and to speak about logic with order. Theorem 2 [Iml, Varl. A global predicate is PTIME computable if and only if it is expressible in FO + LFP with order. The "if" implication of Theorem 2 follows from Theorem 1 in ~3 and from Claim 1. A sketch of a proof of the "only if" implication can be found in [Iml]. An alternative proof of the "only if" implication will be indicated later in this section.

26 Aho and Ullman [AU] define a generalization of LFP whose application is not restricted by monotonicity. A similar idea was independently explored by Livchak [lLil]. Unaware of developments related to the least fixed point operator Livchak (who happened to be a former Ph.D. student of mine) proposes to augment the definition of first-order formulas by the following additional formation rule: If F(x), G(x) and H(x) are well-formed formulas with the same free individual variables x=(xl,...,x) then L(F(x), G(x), H(x)) is a new weil-formed formula whose meaning is the infinite disjunction F0(x) v Flx) v F2(x) v. where Fo(x) is H(x) and each Fi+l(x) is the disjunction of F.(x) and the result of replacing each subformula G(y1,...,y.) of F(x) by Fi(yl,...,y). The extension of first-order logic with order by Livchak's rule captures PTIME [Li2]. We incorporate this fact into Theorem 3. But first let us reformulate Livchak's rule. Definition. Let a be a vocabulary, P be an additional predicate variable of some arity Z, and 7T(P) be a global Z-ary predicate of the vocabulary aU{P}. View T(P) as an operator that, given a global S-ary a-predicate a, produces a global g-ary a-predicate rT(0). This operator Tr(P) is inflationary if a<rr(a) for every global a-predicate a. Let o0,al,etc. be a sequence of global k-ary a-predicates where a0 is empty and each a. equals to T(ai). A fixed point - for rr(P) is an iterative fixed point if for every a-structure S there is an S S i with S =.. 1 Claim 2. Let a, P, Z, 7T(P) and x,1,etc. be as in the definition above. Suppose that -(P) is inflationary in P. Then there is a unique iterative fixed S S sI point 8 for r(P). Moreover, for every o-structure S, = where m=|S|. Thus the iterative fixed point for Tv(P) is PTIME computable if Tr(P) is. The proof is clear. Note that if P and V(P) are as in the definition above then P v r(P) is inflationary. Let FO + IFP be the extension of first-order logic by the following formation rule.

27 IFP formation rule. Let P be a predicate variable of some arity Q, and let (P, x) he a well -formed formull; whose free i.ndividua ll variables are all or some menmbers of x=(xl,, x.. f y(y,,...,yQ) is a tuple of new individual variables then IFP(P, x; P(x) v 4(P,x),y) is a well-formed formula. The meaning of the new formula is that y is in the iterative fixed point for P(x) v (P,x). Claim 3. FO + IFP expresses exactly the global predicates expressible in first-order logic augmented by Livchak's rule. Proof. We consider the extension of first-order logic by both formation rules and show that either rule can be eliminated. The formula IFP(P,x;P(x) v 4(P,x),y) is equivalent to L(f(P,y), Ply), FALSE(y)). Given a formula L(F,G,H) with free individual variables x=(xl,...,xg) and an additional Z-ary predicate variable P write down a formula F'(P,x) such that F(x)=F'(G,x). Using P,F'(P,x), H(x) and first-order means write-down a formula (P,x) saying the following: If -3 H(x) then F' (P,x), else if -3xP(x) then H(x), else F'(P,x). It is easy to check that L(F(x),G(Cx),H(x)) is equivalent to IFP(P,y;P(y) v p(P,y), x) where y is a tuple of new individual variables. a Theorem 3. Let 5r be a global predicate. The following statements are equivalent: (1) ~ is PTIME computable, (2) Tr is expressible in FO + LFP with order, and (3) aT is expressible in FO + IFP with order.

28 Proof. the implication (1) - (2) follows from Theorem 2. The implication (.3) + (fl fol.lows from (Claim 2.'o prove the implication (2) + (3) note that if a global Z-ary predicate Tr(P,x) is monotone in an L-ary predicate variable P -then LFP(P,x;7r(P;x), y) is equivalent to IFP(P,x;P(x) V 7T(P,x), y).' Chandra and Harel show that FO + LFP without order is not able to express the global zero-ary predicate "The cardinality of a given structure is even" [CH2]. Their argument can be extended to show that FO + IFP without order is not able to express the same global predicate. Our Appendix 3 gives an alternative proof of the fact that FO + IFP without order is not able to express some PTIME computable order-independent global predicates T. We turn our attention to global functions. Definition. A global partial function f of vocabulary a, arity 9 and co-arity r assigns to each Y-structure S a partial function f from S to sr S. Example 3. Let, a consist of one binary predicate variable E (for "edge"), so that a-structures are (directed) graphs. Let f(x,y) be the length of a shortest path from x to y. If S is a graph and fS is defined at (x,y) then f S(xy)<S I and therefore f (x,y) is an element of S. Example 4. Let again a be the vocabulary of graphs. For every graph S and every xeS let f(x) be the pair (y,z)ES2 such that there are exactly y. S|+z elements u with an edge from x to u. As was mentioned above, we are interested in logics (or algebras) that capture PTIME (LOGSPACE, etc.) computable global functions. In a sense FO + LFP with order does capture PTIME computable functions: it allows one to speak about the graph of a PTIME computable function f and about digits in the binary notation for f(x). We prefer to speak about global functions directly. See [Gu3] in this connection. Here we mention only the results related to PTIME.

29 Let us ingore singleton structures (altneratively we may allow boolean variables). See the definition of recursive global partial functions in [Gu3]. Theorem 4 [Gu3, Sa]. A global partial function is PTIME computable if and only if it is recursive. Two algebras of recursive global partial functions were given in [Gu3] by some initial members and certain operations. Let ARF (for "Algebra of Recursive Functions") be either of them. Theorem 5 [Gu3]. A global partial function is PTIME computable if and only if it belongs to ARF. An important advantage of (the proof of) Theorem 5 versus (the proof of) Theorem 2 is preserving essential time bounds. Remark. It is easy to prove directly that the graph of every function in ARF is expressible in FO + LFP with order. This together with Theorem 5 gives an alternative proof of the "only if" implication of Theorem 2. Let 7T(x) be a PTIME computable global predicate and let f(x) be the characteristic function for Ir(x) i.e. f(x)=l if 1T(x) holds and f(x)=O otherwise. By Theorem 5, f is in ARF. Hence the predicate f(x)=y is expressible in FO + LFP with order. Hence the predicate f(x)=l is expressible in FO + LFP with order.

30 ~5. Interpolation and definability for polynomial time logic According to ~1, many famous and important theorems about first-order logic fail in the case of finite structures. What happens to those theorems in the case of logic tailored for polynomial time'? We concentrate here on the interpolation and definability principles for polynomial time logic and show that these principles are equivalent to natural complexity principles whose status is unknown. Let PTL (for Polynomial Time Logic) bethe logic FO + LFP with order, or the logic FO + IFP with order, or an algebra of PTIME computable functions from [Gu3]. It will be important that. PTL expresses precisely PTIME computable global predicates. The exact syntax of PTL will not be important. Definition. A partial function f from {0,1}* to {0,1}* is polynomially bounded if there is a natural number k such that If(x) <lxi for all x6Domain(f) with lxl>l. Here I|x is the length of x. More generally, a binary relation B over t0,1}* is polynomially bounded if there is k such that B(x,y) and Ixl>l imply |y<jx|. We identify a nonempty word x=a al...a~ _ in {0,1}* with the structure with universe {0,l,...,-l} and one unary predicate X={i: a.=l}. If Z>2, m=Z for some k and y is a word bo,bl,...,bm 1 in {0,1}*, we identify the pair (x,y) with the extension of the structure x by a k-ary predicate Y={(il,...,ik): if j is the number whose notation in the positional system of base g is i...i then b.=l.} ~- V~1 k Lemma 1. For every NP set A of nonempty words over {0,1}* there is a PTL sentence q such that A={x~{0,1}*: x is the reduct of a model of (}. Proof. Without loss of generality, every xcA is of length at least 2. There are a natural number k and a PTIME computable polynomially bounded binary relation B over {0,1}* such that A={x: (x,y)eB for some y}, and (x,y)EB implies |y|=|x|:. The desired sentence ~ expresses (x,y)EB.CD

31 The analogue of Craig's Interpolation Theorem for PTL will be called the Interpolation Principlle for PTL. T'his principle states that for every valid (in all relevant finite structures) PTL sentence l1 - there is a PTL sentence 0 such that vocabulary (e) vocabulary (1)/l vocabulary (2) and the implications $1 + 0, 6 -+ 6 2 are valid. Theorem 1. The following two statements are equivalent: (1) The Interpolation Principle for PTL, and (2) The following separation principle for NP: for every pair of disjoint NP subsets A1,A2 of {0,1}* there is a P subset B of {0,1}* such that B includes A and avoids A2. Proof. First suppose (1) and let A1,A2 be disjoint NP subsets of {0,1}*. Without loss of generality neither A nor A2 contains the empty word. By Lemma 1 there are PTL sentences $1l'2 such that A.={xc{0,1}*: x is the reduct of a model of Pi} for i=1,2. Without loss of generality, the only common nonlogical constant of 1,'~2 is the unary predicate variable X. Obviously, the implication l - s2 is valid. Let 0 be an appropriate interpolant. The set of models of 0 is the desired set B. Next suppose (2) and let ~1 ~ $2 be a valid PTL sentence. Let a be the common part of the vocabularies of P14,2. For i=1,2 let A.={x: x is the binary code for the ca-reduct of a model of $i}. By (2) there is a P set B that includes Al and avoids A2. The desired interpolant 0 expresses x6B. Note that the Interpolation Principle for PTL implies NPOco-NP=P. The analogue of Beth Definability Theorem for PTL will be called the Definability Principle for PTL. This principle states the following. Let y be a vocabulary, P be an additional predicate variable of some arity Z and fp(P) be a PTL sentence of the vocabulary oU{P}. Suppose that for every a-structure S and all P,P2CS,,s(Pl) and $S(P2) imply Pi=P^. Then there is a PTL formula t of the vocabulary a with g free variables such that for every

32 7-structures S and every P C S S S S()1P ) implies P =S The Weak Definability Principle for PTL is the result of strengthening the antecedent of the Definability Principle for PTL as follows: for every z S a-structure S there is a unique P,1 S such that ) (P1) holds. Definition (cf. [Vat]). A nondeterministic Turing machine M is unambiguous if for every input x there is at most one accepting computation of M on x. An NP subset A of {0,1}* is UNAMBIGUOUS if there is an unambiguous Turing machine that accepts A. Theorem 2. The following statements (1)-(4) are equivalent. (1) The Definability Principle for PTL. (2) For every polynomially bounded partial function f from {0,1}* to {0,1}*, if the graph of f is in P then f is PTIME computable. (3) For every polynomially bounded partial function f from {0,1}* to {O,1}*, if the graph-of f is in P then the domain of f is in P. (4) UNAMBIGUOUS = P. Proof. (1) - (2). Suppose (1) and let f be a polynomially bounded partial function from {0,1}* to {0,1}* with PTIME computable graph. It suffices to construct a PTIME algorithm for calculating f(x) for x of length at least 2. Let x range over words of length at least 2. Without loss of generality there is k such that f(x)|=|x|k for all x in Domain(f). There is a PTL sentence )(X,Y) with a unary predicate variable X and a k-ary predicate variable Y that expresses (x,y)cGraph(f). By (1) there is a PTL formula i such that if )(X,Y) holds in the structure (x,y) then Y={(il,...,ik) (il;...,ik) holds in x}. Here is a PTIME algorithm for calculating f(x). View x as a structure in the vocabulary {X}. Compute Y=(il,...,ik) (il,...,ik holds in x}.

J3 The extension of the structure x by the predicate Y corresponds to a pair (x,y) for some word y of length xk. Check whether ('X,Y) holds in'the extended structure. If yes then y=f(x). The implications (2) + (3) and (3) + (4) are trivial. (4) - (1). Suppose (4) and let a be a vocabulary variable of some arity Q and (P) be a PTL sentence such that for every 9, S a-structure S there is at most one PCS satisfying qS(P). Set K={(S,c): S is a o-structure, c~S and there is P CS such that q (P) holds and caP}. Obviously, K is UNAMBIGUOUS. By (4), K is P. The desired PTL formula?(V1,.',v) expresses (S,v,.,v).K.Q The following theorem was established in a discussion with Neil Immerman. (It succeeded Theorem 1 but preceded Theorem 2.) Theorem 3. The following statements (1) - (3) are equivalent. (1) The Weak Definability Principle for PTL. (2) For every polynomially bounded function f:{O,1}* + {0,1}*, if the graph of f is in P then f is PTIME computable. (3) UNAMBIGUOUS co-UNAMBIGUOUS=P. Proof. The case (1) + (2) is similar to the case (1) - (2) in the proof of Theorem (2). (2) + (3). Suppose (2) and let AO,A1 be complementary UNAMBIGUOUS subsets of {0,1}*. There are unambiguous nondeterministic Turing machines M0,M accepting AOA1 respectively. For i=0,l and xcAi let f(x) be the digit i followed be the binary code for the accepting computation of M. on x. By (2), f is PTIME computable. Hence A and A are P. (3) + (1). Suppose (3) and let a,P,t(P) and K be as in the case (4) - (1) of the proof of Theorem 2 except now for every a-structure S there is a unique PCSS satisfying ( (P). Obviously K is UNAMBIGUOUS and co-UNAMBIGUOUS. By (3), K is P. The desired PTL formula C(v1,...,v9) expresses (S,vl,...,vg)EK.C

34 As we saw in ~1, the Interpolation Principle for first-order logic implies the Definability Principle for first-order logic. The same proof shows that the Interpolation Principle for PTL implies the Definability Principle for PTL. If P=NP then the Interpolation Principle for PTL is obviously true. It is easy however to construct an oracle for which even the Weak Decidability Principle for PTL fails. Claim (Andreas Blass). There is an oracle for which the Weak Definability Principle for PTL fails. Proof. By Theorem 3 it suffices to construct an oracle A and a function f from {0,1}* (or from a P subset of {0,1}*) to {0,1}* such that f is not PTIME computable relative to A whereas the graph of f is. We construct A C{0,I}*, containing exactly one word w of each length n, such that the function; ~n~~~~n f(0 )=w is not PTIME computable relative to A. n Enumerate all (deterministic) PTIME bounded query machines. Let pk be the time bound for a machine Mk. We define A in stages, choosing finitely many wn's k' n at each stage. The kth stage will ensure that MA does not compute f. Stage k. Fix a natural number d that is larger than any n for which w d n tlas already been chosen and so large that Pk(d)<2 -2. Set w =0 for all n<d -- n for which w was not previously chosen. Run Mk with input 0 and oracle {w: n<d}. Let B be the set of queries during the computation. By the time n bound, |Bl<pk(d)<2 -2. Choose wd in {0,} -B such that wd differs from the output (if any) of Mk. If d<2 and,<|x| for some xeB chose wg in {0,1} -B. It is easy to see that M will not compute w on input 0.d lwerk d The computational status of Craig's Interpolation Theorem for propositional logic was explored by Mundici [Mul.

Appendix 1. Monotone versus positive. This appendix is devoted to an important theorem about first-order logic whose status in the finite case is unknown. Definition. Let a be a vocabulary, P be an additional predicate variable of arity Z and ((P,xl,...,xr) be a first-order formula in the vocabulary aU{P} with free individual variables as shown. The formula q is monotonically increasing in P if every a-structure S satisfies the following for every 9-ary predicates P1,P2 on S, if Vx...Vx [P1(xl,...,xQ) + P2 (x,...,x)] then Vx1... Vxr[(P1,x1,... xr) - t(P2,...,'xr ] Define in the obvious way the following: ( is monotonically decreasing in P, P is monotonically increasing in P on finite structures (or, in the finite case), is monotonically decreasing in P on finite structures. We restrict our attention to monotonically increasing behavior; the generalization for monotonically decreasing behavior will be obvious. We say "monotone" for "monotonically increasing". We say that a first-order formula ( is positive in a predicate symbol P if every appearance of P in 4 is positive. A precise definition of positive appearances of a predicate symbol in a first-order formula can be found in [CK]. It is easy to see that f is monotone in P if ( is positive in P. Theorem 1. If a first-order formula is monotone is a predicate symbol P then there is a first-order formula (' such that P' is equivalent to ~ and positive in P. I do not know who was the first to formulate this theorem but it is an obvious consequence of the Lyndon Interpolation Theorem [CK]. Conjecture. Theorem 1 fails in the case of finite structures. The rest of this appendix contains a few remarks related to the conjecture. First we exhibit a sentence which is monotone in a unary predicate symbol P on finite structures but which is not monotone in P in general. Let f be a unary

36 function symbol.. The desired sentence (with equality) says that f is one-to-one and that P is closed under f-predecessors if P is closed under f-successors. Claim 1. Let P be a predicate variable. The following problems are undecideable: (i) Given a first-order sentence tell whether is monotone in P, and (ii) Given a first-order sentence ) tell whether ) is monotone in P on finite structures. Proof. Without loss of generality P is just a propositional variable. Let be a first-order sentence that does not mention P. It is valid (resp. valid in the finite case) iff the sentence P + 4 is monotone (resp. monotone on finite structures) in P. Corollary 1. Let P be a predicate variable. There is no recursive function f from first-order sentences to first-order sentences- such that an arbitrary first-order sentence ) is monotone in P if and only if the sentence f()) is positive in P. Corollary 2. Let P be a predicate variable. There is no partial recursive function f from first-order sentences to first-order sentences such that an arbitrary first-order sentence - is monotone in P on finite structures if and only if f()) is positive in P. In the case of a propositional variable P there is a simple function that, given a first-order sentence ~(P), produces a first-order sentence V'(P) such that' (P) is positive in P and (' (P) is logically equivalent to 4(P) if )(P) is monotone in P. The desired 4' (P) is )(False) v [P & 4(True)]. On the other hand, a routine coding, given an arbitrary first-order formula with a predicate variable P, produces a first-order formula )' in the vocabulary {E,Q} such that E is a binary predicate symbol, Q is a unary predicate symbol and (~ is monotone (respectively, positive) in P iff 4' is monotone (respectively, positive in Q. Moreover, it can be ensured that 4' has a conjunct saying that E is symmetric and irreflexive.

37 I have also checked that Theorem 1 remains true in the case of finite structures if 4 is an cxistential sentence, a universal sentence, a prenex sentence with prefix n3 or a prenex sentence with prefix n V Andreas Blass observed that if ~(P) is positive (resp. monotone, monotone on finite structures) in P then so is q(-)P). Thus, if Theorem 1 is true inthe finite case for prenex sentences 4 with certain prefixes then it is true in the finite case for prenex sentences with the dual prefixes.

38 Appendix 2. Transitive closure is not first-order expressible. Theorem. Connectivity of a given graph is not first-order expressible in the case of finite structures (even in the presence of linear order). Hence the transitive closure of a given binary relation is not first-order expressible in the case of finite structures (even in the presence of linear order). Proof. For every positive integer n let S be the set {Ol,...,n-l} with.the natural order and E (x,y) be the following binary relation on n {O,l,...,n-l}: either y=x+2 or x=n-l and y=O. Note that a graph (S,E ) is n n connected iff n is even, and a relation E is obviously and uniformly in n n expressible in the first-order language of order. Now use Lemma(ii) in ~1.0 The theorem (without mentioning linear order) is due to Fagin [Fa2] and was reproved several times. Gaifman and Vardi wrote even a special paper [GV] with a specially short proof and a brief review of other known proofs. Fagin's proof actually gives more: connectivity is not expressible by an existential second-order sentence where all quantified predicate variables are unary. Yiannis Moschovakis noticed that all those proofs do not work in the presence of linear order and expressed an interest in such results in the presence of linear order.

Appendix 3. The fixed point operators can be powerless. Provisos 1-3 of ~3 are in force here because we will consider structures as inputs for algorithms. On the other hand the natural order of elements of a given structure is not a logical constant here, so that isomorphisms can break the order of elements. We are interested more in isomorphism types of structures than in specific representations. Definition. A global Z-ary predicate'T of some vocabulary a is invariant if for every isomorphism f from a a-structure A onto a a-structure B and A B - every Z-tuple acA, T (a) is equivalent to 7f (fa). Any first-order expressible global predicate is invariant as well as any global predicate expressible in FO + LFP or FO + IFP. All these global predicates are PTIME computable. They do not exhaust, however, the PTIME computable global predicates. The following theorem provides plenty of counterexamples. It speaks about FO + IFP because FO + IFP subsumes FO + LFP. Recall that a first-order theory T is called w-categorical if all countable models of T are isomorphic. Theorem 1. Let T be an w-categorical first-order theory of some vocabulary (J. Then for every formula i(x) in FO + IFP there is a first-order formula' (x) such that the global predicates ~(x) and 1'(x) coincide on the finite models of T. Remark. Actually, the global predicates ~(x) and 1'(x) will coincide on all models of T but we do not care here about infinite models. Proof. Without loss of generality the given formula ~(x) is IFP(P,y; P(y) v 1P(P,y), x) where 1p is first-order. Let af(x)=FALSE and let each ai. (x)=ai(x)/i (ai.,x). By Ryll-Nardzewski's Theorem, there is a finite p such that ap+l(x) is equivalent to a (x) on the infinite models of T. By the compactness theorem, there is a finite m such that,a (x) is equivalent to ap (x) on all models of T of p+l p.

40 size at least m. Hence there is a finite q such that aq l(x) is equivalent to a (x) in T. The first-order formula a is the desired i. C q q Now we are ready to show that some polynomial time computable invariant predicates are not expressible in FO + IFP. Example 1. The first-order theory of equality is w-categorical. The predicate ( if |A| even Tr(A) 1 otherwise is not first-order (see Lemma in ~1). By Theorem 1, rr is not expressible in FO + IFP. (Cf. [CH2, Theorem 6.2].) Example 2. Let F be a finite field. Let T be the first-order theory of vector spaces over F. Obviously, T is W-categorical. Let r be the global A predicate such that for every structure A of the vocabulary of T, i =1 if A is a model of T and dimension(A) is even, and TA =0 otherwise. Using Ehrefeucht games [Eh] it is easy to check that T is not first-order. By Theorem 1 it is not expressible in FO + IFP. It is not difficult to extend FO + LFP in such a way that the predicates of Examples 1 and 2 arc expressible in the extended logic and only polynomial time computable invariant' predicates are expressible in the extended logic. Still, the problem to design a logic that expresses exactly polynomial time computable invariant global predicates is open.

4.1 References [Au] A.V. Aho and J.D. Ullman, "Universality of Data Retrieval Languages", Proc. of 6th ACM Symposium on Principles of Programming Languages, 1979, 110-117. [Be] J. Bennet, "On Spectra", Doctoral Dissertation, Princeton University, N.J., 1962. [Bo] E. Borger, "Spektralproblem and Completeness of Logical Decision Problems", in "Logic and Machines: Decision Problems and Complexity (ed. E. Borger, G. Hasenjaeger, D. R6dding), Springer Lecture Notes in Computer Science, to appear. [CH1] A.K. Chandra and D. Harel, "Computable Queries for Relational Databases", Journal of Computer and System Sciences 21 (1980), 156-178. [CH2] A.K. Chandra and D. Harel, "Structure and Complexity of Relational queries", Journal of Computer and System Sciences 25 (1982), 99-128. [CK] C.C. Chang and H.J. Keisler, "Model Theory", North-Holland, 1977. [CKS] A.K. Chandra, D.C. Kozen and L.J. Stockmeyer, "Alternation", Journal of the ACM 28 (1981), 114-133. [Co] K. Compton, A private communication. [Cr] W. Craig, "Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory", J. Symbolic Logic 22 (1957), 250-268. [Eh] A. Ehrenfeucht, "An Application of Games to the Completeness Problem for Formalized Theories", Fund. Math. 49 (1961), 129-141. [Fal] R. Fagin, "Generalized First-Order Spectra and Polynomial-Time Recognizable Sets", in "Complexity of Computation" (ed. R. Karp), SIAM-AMS Proc. 7 (1974), 43-73. [Fa2.] R. Fagin, "Probabilities on Finite Models", Journal of Symbolic Logic 41 (1976), 50-58. [Fr] Ht. Friedman, "The Complexity of Explicit Definitions", Advances in Mathematics 20 (1976), 18-29. [FV] S. Feferman and R.L. Vaught, "The First-Order Properties of Algebraic Systems", Fund. Math. 47 (1959), 57-103. [GJ] M.R. Garey and D.S. Johnson, "Computers and Intractability: A Guide to the Theory of NP-completeness", Freeman, 1979. [GKLT] Yu. V. Glebskii, D.I. Kogan, M.I. Liogon'kii and V.A. Talanov, "Range and Degree of Relizability of Formulas in the Restricted Predicate Calculus", Cybernetics 5:2 (1969), 17-28; translation (1972), 142-154. [GL] Y. Gurevich and H.R. Lewis, "A Logic for Constant-Depth Circuits", Manuscript, 1983. [GV] H. Gaifman and M.Y. Vardi, "A Simple Proof that Connectivity is not FirstOrder", Manuscript, 1983. [;o] W. Goldfarb, "The Godel Class with Identity is Unsolvable", Journal of Symbolic Logic, to appear.

42 [Gul] Y. Gurevich, "Existential Interpretation", Algebra and Logic, 4:4 (1965), 71-85 (or "Existential Interpretation II", Archiv Math. Logik 22 (1982), 103-120). [Gu2] Y. Gurevich, "Recognizing Satisfiability of Predicate Formulas", Algebra and Logic 5:2 (1966), 25-55; "The Decision Problem for Logic of Predicates and Operations", Algebra and Logic 8 (1969), pages 160-174 of English translation; "The Decision Problem for Standard Classes', Journal of Symbolic Logic 41 (1976), 460-464. [Gu3] Y. Gurevich, "Algebras of Feasible Functions", Proc.. of 24th IEEE Symposium on Foundations of Computer Science, 1983, 210-214. [HU] J.E. Hopcroft and J.D. Ullman, "Introduction tq Automata Theory, Languages and Computation", Addison-Wesley, 1979. [Imi] N. Immerman, "Relational Queries Computable in Polynomial Time", Proc. of 14th ACM Symposium on Theory of Computing, 1982, 147-152. [Im2] N. Immerman, "Languages which Capture Complexity Classes", Proc. of 15th ACM Symposium on Theory of Computing, 1983, 347-354. [JS] N.G. Jones and A.L. Selman, "Turing Machines and the Spectra of First-Order Formulas", Journal of Symbolic Logic 39 (1974), 139-150. [Ko] V.F. Kostyrko, "To the Decision Problem for Predicate Logic", Ph.D. Thesis, Kiev, 1965 (Russian). [Kr] G. Kreisel, Technical Report No. 3, Applied Mathematics and Statistics Labs., Stanford University, January 1961. [Lil] A.B. Livchak, "The Relational Model for Systems of Automatic Testing", Automatic Documentation and Mathematical Linguistics 4 (1982), pages 17-19 of Russian original. [Li2] A.B. Livchak, "The Relational Model for Process Control", Automatic Documentation and Mathematical Linguistics 4 (1983), pages 27-29 of Russian original. [Lin] P. Lindstr6m, "On Extensions of Elementary Logic", Theoria 35 (1969), 1-11. [Mu] D. Mundici, "Complexity of Craig's Interpolation", Annales Societ. Math. Polonae, Series IV: Fundamenta Informaticae, vol. 3-4 (1982);'NP and Craig's Interpolation Theorem", Proc. of Florence Logic Colloquium 1982, North Holland, to appear. [Sa] V. Sazonov, "Polynomial Computability and Recursivity in Finite Domains", Elektronische Informationsverarbeitung and Kybernetik 16 (1980), 319-323. [S9] L.J. Stockmeyer, "The Polynomial - Time Hierarchy", Theoretical Computer Science 3 (1977), 1-22. [Tai] W.W. Tait, "A Counterexample to a Conjecture of Scott and Suppes", Journal of Symbolic Logic 24 (1959), 15-16. [Tar A. Tarski, "A Lattice-Theoretical Fixpoint Theorem and its Application", Pasific Journal of Mathematics 5 (1955), 285-309. [Tr] B.A. Trakhtenbrot, "Impossibility of an Algorithm for the Decision Problem on Finite Classes", Doklady 70 (1950), 569-572.

[UZ] J.D. Ullman, "Principles of Database Systems", Computer Science Press, 1982. [Vap] L.G. Valiant, "Relative Complexity of Checking and Evaluating", Information Processing 5 (1976), 20-23. [Va] M.Y. Vardi, "Complexity of Relational Query Languages", Proc. of 14th ACM Symposium on Theory of Computing, 1982, 137-146. [Zf] M.M. Zloof, "Query-by-Example: a Database Language", IBM Syst. Journal 16 (1977), 324-343.

UNIVERSITY OF MICHIGAN 3 9015 03026 8059 3 9015 03026 8059