RIA
laboria

<figure><img src="image_1.png" /></figure>

laboratoire de recherche
en informatique
et automatique

<figure><img src="image_2.png" /></figure>

The complexity of theories
of the monadic predicate
calculus

Ch. Rackoff

<figure><img src="image_3.png" /></figure>

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
78150 - Le Chesnay
Tél. 954.90.20

Rapport de Recherche n°136
Octobre 1975
<figure><img src="image_4.png" /></figure>

# THE COMPLEXITY OF THEORIES OF THE MONADIC PREDICATE CALCULUS

Ch. Rackoff

IRIA-LABORIA

## Abstract :

We present some results, obtained jointly with Albert Meyer on the complexity of determining satisfiability of formulas in the pure monadic predicate calculus, and of formulas in the monadic predicate calculus with an equivalence relation. We show a lower bound of nondeterministic time $2^{cn/\log n}$ (for some constant c) for the first case, and of nondeterministic time $2^{2cn/\log n}$ for the second. These bounds still hold, and are optimal, if the number of quantifiers is bounded from above.

If quantification over second order variables is permitted as well in the above languages, then satisfiability can be decided in deterministic space, respectively, $2^{dn/\log n}$ and $2^{2dn/\log n}$ for some constant d.

## Résumé :

Nous présentons ici des résultats obtenus conjointement avec A. Meyer concernant la complexité des procédures de décision du calcul des prédicats monadique avec ou sans relation d'équivalence. Nous établissons des bornes inférieures en temps non déterministe de $2^{2cn/\log n}$ dans le premier cas, de $2^{cn/\log n}$ dans le second. Ces résultats sont encore valables, et optimaux, si le nombre de quantificateurs est borné.

Dans le cas où des quantifications du second ordre sont permises, on montre que ces problèmes sont décidables en mémoire au plus $2^{2dn/\log n}$ et $2^{dn/\log n}$ respectivement.
# The Complexity of Theories of the Monadic Predicate Calculus
(preliminary report)

## Section 1 : Introduction

Recent work on the complexity of decision procedures for logical theories [1,2] has shown that although a theory may technically be decidable, it may be impossible to implement any procedure within practical time bounds; in particular, certain theories have been shown to require time which is exponential, double exponential, or worse, as a function of the length of the sentence which is to be decided.

In this paper we report on some lower bounds for decision procedures for satisfiability of sentences of the monadic predicate calculus. Firstly, we consider the first order language $L_1$ where the only formal predicates are $x \in A_0, x \in A_1, ...$; we present a proof of Albert Meyer that any procedure (even non deterministic) that decides whether a given sentence is satisfiable requires for some constant $c$ and infinitely many $n$, time $2^{cn/\log n}$ on some sentence of length $n$. Secondly, we consider the first order language $L_2$ which is the same as $L_1$ except that we now also allow atomic formulas of the form $x_1 \sim x_2$, and only consider structures where $\sim$ is an equivalence relation on the domain. For this case, we present a proof (due to this author and Albert Meyer) of a lower bound of time $2^{2cn/\log n}$ for procedures that decide satisfiability, that is, one exponential higher than the previous result. In fact, both these lower bounds are valid even if one bounds above the number of quantifiers used, and in this sense are *optimal* to within the value of $c$.

In section 2 we explain the outlines of these proofs, each of which consists, essentially, of appropriate versions of three lemmas.

In each case, lemmas 1 and 3 have absolutely nothing to with the logical theories in question, but are rather theorems about the power of Turing machines and ways in which lower bounds can be proved in general. Detailed discussions of these lemmas can be found in [3,4], and we shall not say much about their proofs here. In section 3 we prove, for each of the two theories, an appropriate version of lemma 2, thus completing the proofs of the lower bounds.
Section 4 contains the statements of some results concerning upper bounds on the above theories.

## Section 2 :

We begin by defining the first order languages $L_1$ and $L_2$. Both languages have first order variable symbols of the form $x\omega$ where $\omega \in \{0,1\}^*$ which we shall write informally as $x,x_1,x_2,\dots,y,y_1,\dots$. Both languages have atomic formulas of the form $x\omega \in \underline{A}\omega$ where $\omega,\omega' \in \{0,1\}^*$, but again we shall express this informally as, for example, $x_5 \in \underline{A}_3$.

$L_2$ also allows atomic formulas of the form $x \sim y$ where x and y are formal variables. The formulas and sentences of $L_1$ and $L_2$ are obtained from the atomic formulas in the usual way using parentheses, the connectives $\wedge, \vee, -, \rightarrow$, and the quantifications $\exists$ and $\forall$ over first order variable symbols.

A structure for $L_1$ is a sequence $D = \langle D, A_1, A_2, \dots \rangle$ where $D \neq \emptyset$ and $A_i \subseteq D$ for $i \in N$. A sentence $F$ of $L_1$ is true in $D$, written $D \models F$, if $F$ is true when quantification is interpreted as ranging over the members of $D$, when $\underline{A}\omega$ is interpreted as $A_i$ where $\omega$ is the binary representation of $i$, and where $\epsilon$ is interpreted as set membership. Similarly, a structure for $L_2$ is a sequence $\langle \overline{D}, \sim, A_1, A_2, \dots \rangle$ where $\overline{D} \subsetneq D$ is an equivalence relation. We denote by $\text{SAT}(L_1)$ and $\text{SAT}(L_2)$ the satisfiable sentences of $L_1$ and $L_2$, where a sentence is said to be satisfiable if it is true in some appropriate structure. For any $i \in N$, we define $L_1^i$ (respectively $L_2^i$) to be those well-formed formulas of $L_1$ ($L_2$) which contain no more than $i$ instances of a quantification symbol.

Since we will be interested in the complexity of deciding membership in $\text{SAT}(L_1)$ and $\text{SAT}(L_2)$ as a function of the length of input, it is important to have a precise notion of the length of a formula in one of these languages. We will say that the length of a formula is the total number of symbols necessary to write it according to our formal definition, keeping in mind that when speaking formally, all subscripts are written in binary. When we write formulas informally in this paper, they correspond to formal objects obtained by using formal variables, etc, where the subscripts are chosen to be as short as possible. For instance, any informally written formula which contains $A_1,A_2,\dots,A_n$ corresponds to a formal object of length at least proportional to $\log n$ (since the sum of the lengths of n different binary numbers must be at least this long).
For the rest of this report, it will be convenient to let $f_1(n)$ represent the function $2^n$, and $f_2(n)$ the function $2^{2^n}$. Our main theorem is:

**Theorem 1** : Let $i \in \{1,2\}$. There exist constants $c,j>0$ such that any non deterministic Turing machine which decides membership in $L_i^j \cap \text{SAT}(L_i)$ requires, for infinitely many $n$, time $f_i(\text{cn/ logn})$ on some member of $L_i^j \cap \text{SAT}(L_i)$ of length $n$.

Theorem 1 will follow from the following three lemmas. Lemma 1 is proved in [3]. Lemma 2 is proved in the next section. We shall present outlines of the proofs of lemma 3 and theorem 1, but for a complete and rigorous discussion of this type of result, the reader is advised to consult [4].

**Lemma 1** : Let $i \in \{1,2\}$. There exists a set $L \subseteq \{1\}^*$ such that

a) there is some non deterministic Turing machine which recognizes $L$ within time $f_i(n)$.

and b) there is no non deterministic Turing machine which recognizes $L$ within time $f_i(n/2)$.

**Lemma 2** : Let $i \in \{1,2\}$. For some constant $k$ and every $n \in \mathbb{N}$, $n>0$, there exists formulas $^+$ of $L_i^k$:

$F_{n,1}^i, F_{n,2}^i(x,y), F_{n,3}^i(x,y), F_{n,4}^i(x), F_{n,5}^i(x,y)$ such that

1) $F_{n,1}^i \in \text{SAT}(L_i)$

2) Let $D$ be a structure for $L_i$ with domain $D$ such that $D \models F_{n,1}^i$. Then:

I) Let $R_1 = \{(a,b) \in D \mid (D,a,b) \models F_{n,2}^i(x,y)\}$. Then $R_1$ is an equivalence relation.

II) Let $R_2 = \{(a,b) \in D \mid (D,a,b) \models F_{n,3}^i(x,y)\}$. Then $R_2$ induces a finite linear order of length $\ge (f_i(n))^2$ on the equivalence classes of $R_1$. (This means, in particular, that $R_2$ is transitive and $[(a,b) \in R_2]$ and $(b,a) \in R_2] \Longleftrightarrow (a,b) \in R_1$).

<footnote>† When we write $F(x,y)$ this means that $x$ and $y$ are variables occuring freely in $F$. $(D,a,b) \models F(x,y)$ means that $D \models F$ when free occurences of $x$ and $y$ are interpreted as a and b.</footnote>
(I) Begins with the initial configuration (of length $f_i(n))$ of $m$ computing on $1^n$; for this we must use $F_{n,4}^i$ and $F_{n,5}^i$.

(II) has the property that every two consecutive blocks of size $f_i(n)$ are consistent with the transition rules of $m$; for this we must use $F_{n,5}^i$, and (III) contains (a representation of) the accepting state of $m$.

With a bit of care, the construction of $G_n^i$ will only use polynomial time, space order of $n \log n$, and a number of quantifiers independent of $n$ and $m$.

**Outline of proof of Theorem 1:** Let $i \in \{1,2\}$, let $L$ be as in Lemma 1, and let $m$ be a non deterministic Turing machine which recognizes $L$ within time $f_i(n)$.

Let $m_0$ be a non deterministic machine which recognizes $SAT(L_1^k)$ where $k$ is as in Lemma 3. Define $m'_0$ to be the non deterministic machine which on input $1^n$ does the following : $m'_0$ computes $G_n^i$ as in Lemma 3, and then applies $m_0$. Clearly $m'_0$ accepts exactly $L$. If $m_0$ runs within time $f_i(\text{dn/logn})$ for some constant $d$, then by part 2 of Lemma 3, $m'_0$ runs within time $f_i(\text{dd'n})$ for some constant $d$'independent of $d$. By part 2 of Lemma 1, no $m_0$ which recognizes $SAT(L_1^k)$ runs within time $f_i(\text{cn/logn})$, for some constant $c$.

**Section 3:**

We will first prove Lemma 2 for $i=1$. Let $n>0$ be fixed; we will construct formulas of $L_1$ in six stages. The reader can check that they can all be constructed in time polynomial in $n$ and space (including the size of the formulas) proportional to $n \log n$, and that they all belong to some fixed $L_1^k$. The idea of the construction is as follows : in any given structure, an element can be viewed as corresponding to a binary sequence of length $2n$, determined by the membership properties of that element with respect to $A_1, A_2, \dots, A_{2n}$; there are $2^{2n}$ such sequences and they have a natural order, and it is therefore the case that in some structures we can pick out in a natural way a sequence of length $2^{2n} = (2^n)^2$.

**Definition:** Let $D = \langle D, A_1, A_2, \dots \rangle$ be a structure. If $x \in D$, then define $\text{num}(x) \in \{0,1,2,\dots,2^{2n}-1\}$ to be the integer whose binary representation is $w_{2n} \dots w_2 w_1$ where $w_i = 1$ iff $x \in A_i$, for $1 \le i \le 2n$. We say that $D$ is *complete* if for every $m \in \{0,1,2,\dots,2^{2n}-1\}$ there exists an $x \in D$ such that $\text{num}(x) = m$.
III) $\{a \in D | (D,a) = F_{n,4}^i(x)\}$ is exactly the $n^{th}$ element in the ordering represented by $R_2$.

and IV) $\{(a,b) \in D \times D | (D,a,b) = F_{n,5}^i(x,y)\}$ is exactly the set of (a,b) such that the $R_1$ class of b is exactly distance $f_i(n)$ after the $R_1$ class of a, in the ordering $R_2$.

3) There is some (deterministic) procedure which given $n$ constructs $F_{n,1}^i, F_{n,2}^i, F_{n,3}^i, F_{n,4}^i, F_{n,5}^i$ within time a fixed polynomial in $n$ and space proportional to $n \log n$.

**Lemma 3** : Let $i \in \{1,2\}$. Let $m$ be a non deterministic Turing machine with input alphabet $\{1\}^*$ which runs within time $f_i(n)$. Then for some constant $k$ independent of $m$ and every $n \in N, n>0$, there is a sentence $G_n^i$ of $L_i^k$ such that

$$1) \ m \text{ accepts } 1^n \iff G_n^i \in \text{SAT}(L_i)$$

and 2) there is some procedure which given $n$ constructs $G_n^i$ within time a fixed polynomial in $n$ and space proportional to $n \log n$.

**Outline of Proof** : Let $i, m$, and $n$ be given. A+ any time in a computation of $m$ on $1^n$, the instantaneous configuration of $m$ can be represented by a sequence of $f_i(n)$ symbols which contain information as to the contents of the first $f_i(n)$ squares of the tape, the symbol representing the square which currently contains the head having a special mark indicating the current state of $m$. A computation of $m$ of $f_i(n)$ steps can be represented as a string of length $(f_i(n))^2$, that is, the concatenation of the first $f_i(n)$ configurations. This will be a string over some finite alphabet independent of $n$, say $\{0,1\}^J$.

Let $F_{n,1}^i, \dots, F_{n,5}^i$ be as in Lemma 2. Consider a structure satisfying $F_{n,1}^i$; the formulas $F_{n,2}^i$ and $F_{n,3}^i$ define a linear ordering of length $\ge (f_i(n))^2$, and any subset $A$ of the domain corresponds therefore to a binary string of length $\ge (f_i(n))^2$. A J-tuple $(A_1, \dots, A_J)$ of subsets represents a string over $\{0,1\}^J$ of length $\ge (f_i(n))^2$. The sentence $G_n^i$ will "say" essentially that $A_1, \dots, A_J$ represent a string, which represents an accepting computation of $m$ on $n$. Assuming $A_1, \dots, A_i$ do not appear in $F_{n,1}^i, \dots, F_{n,5}^i$, it will be the case that $G_n^i \in \text{SAT}(L_i) \iff m$ accepts $1^n$. $G_n^i$ will say that the string over $\{0,1\}^J$ represented by $(A_1, \dots, A_J)$:
**Stage 1:** The formulas ZERO(x), ONE(x), EN(x), EXP(x), TOP(x) can be constructed such that: (D,a) $\models$ ZERO(x) $\Leftrightarrow$ num(a)=0, (D,a) $\models$ ONE(x) $\Leftrightarrow$ num(a)=1, (D,a) $\models$ EN(x) $\Leftrightarrow$ num(a)=n, (D,a) $\models$ EXP(x) $\Leftrightarrow$ num(a)=2^n, (D,a) $\models$ TOP(a)=2^{2n}-1.

These formulas are easy to construct, in fact without using any quantifiers; for example, EXP(x) can be written as

¬ (x ∈ A₁) ∧ ¬ (x ∈ A₂) ∧ ... ∧ ¬ (x ∈ Aₙ) ∧ (x ∈ Aᵣ+₁) ∧ ... ∧ (x ∈ Aᵣ+₂) ∧ ...

**Stage 2 :** ADD(x,y,z). We will construct ADD such that
(D,a,b,c) ⊢ ADD (x,y,z) ⇔ num(c) = num(a) + num(b). In order that
ADD be sufficiently short, we note the following fact : say that a,b, and c
are integers such that when written in binary, a=a₂ⁿ...a₂a₁, b=b₂ⁿ...b₂b₁,
and c=c₂ⁿ...c₂c₁; then c=a+b ⇔ c₁=a₁+b₁ mod 2, and for 1<i≤2ⁿ,
cᵢ=aᵢ+bᵢ+fdᵢ mod 2 where dᵢ=0 if cᵢ-1=aᵢ-₁+bᵢ-₁ and dᵢ=1 if cᵢ-1 ≠ aᵢ-₁+bᵢ-₁
(dᵢ is the carry from column i-1). Rather than explicitly writing ADD, we
simply remark that ADD(x,y,z) can be expressed as the conjunction
F₁(x,y,z) ∧ F₂(x,y,z) ∧ ... ∧ F₂ⁿ(x,y,z) where F₁ involves only A₁, and for
1<i≤2ⁿ, Fᵢ involves only Aᵢ and Aᵢ-₁, and each Fᵢ has length order of log n.

**Stage 3 :** COMP. We will construct the sentence COMP such that D ⊢ COMP ⇔ D
is complete. COMP can be written as :
∃x₀ ∃x₁ (ZERO(x₀) ∧ ONE(x₁) ∧ ∀x ∃y ((⊳ TOP(x)) → ADD(x,x₁,y))).

**Stage 4 :** NUM(x,y). We will construct NUM(x,y) such that (D,a,b) $\models$ NUM(x,y) $\Leftrightarrow$ num(a)=num(b). NUM can be written as : $(x \in A_1 \leftrightarrow y \in A_1) \wedge \dots \wedge (x \in A_{2n} \leftrightarrow y \in A_{2n})$.

**Stage 5 :** ORD(x,y). We will construct ORD such that if D is complete then
(D,a,b) ⊢ ORD ⇔ num(a) ≤ num(b). ORD can be written as : ∃z ADD(x,z,y).

**Stage 6 :** DIST(x,y). We will construct DIST such that if D is complete, then
(D,a,b) ⊢ DIST(x,y) ⇔ num(b) = num(a) + 2ⁿ. DIST can be written as :
∃z (EXP(z) ∧ ADD(x,z,y)).
We now observe that the formulas COMP, NUM(x,y), ORD(x,y), EN(x), DIST(x,y) suffice to prove Lemma 2 when i = 1.

We will now prove Lemma 2 for i=2. Let $n>0$ be fixed; we will construct formulas of $L_2$ in eight stages. The reader can check that they can all be constructed within time polynomial in $n$ and space proportional to $\log n$, and that they all belong to some fixed $L_2^k$. The idea of the construction is as follows : consider a structure $D$ for $L_2$ which is complete (when viewed as a structure for $L_1$) in the sense of the above definition ; the function num divides the domain $D$ into $2^{2n}$ pieces, and so each ~ equivalence class corresponds to a binary string of length $2^{2n}$ depending upon which of these $2^{2n}$ pieces it intersects ; there are $2^{2^{2n}}$ such strings, and it is therefore the case that in some structures we can pick out in a natural way a sequence of length $(2^{2^{2n}} - 1) > (2^{2^n})^2$. (We subtract 1, because no ~ class can be empty).

**Definition:** Let $D = \langle D, \sim, A_1, A_2, \dots \rangle$ be a structure for $L_2$. If $x \in D$, then define

$$ \mathrm{num}'(x) \in \{1, 2, \dots, 2^{2^{2n}} - 1\} $$

to be the integer $w_l \dots w_2 w_1$ where $l=2^{2n}$ and where for $1 \le i \le l$, $w_i=1$ iff for some $y \in D$, $y \sim x$ and $\mathrm{num}(y)=i$. We say that $D$ is *super-complete* if

a) For each $i \in \{1, 2, \dots, 2^{2^{2n}} - 1\}$ there is some $x \in D$ such that $\mathrm{num}'(x)=i$.
and b) For $1 \le i \le n$, $A_{2n+i} \ne \emptyset$ and $x \in A_{2n+i} \Rightarrow \mathrm{num}'(x)=i$.

**Stage 1 :** $\mathrm{MEM}(x,y)$. We will construct $\mathrm{MEM}$ such that $(D,a,b) \models \mathrm{MEM}(x,y) \iff$ if $\mathrm{num}(a)=j$ and $\mathrm{num}'(b)=m$, $\ell \dots m_2 m_1$ (in binary), then $m_j=1$. $\mathrm{MEM}(x,y)$ can be written simply as :

$$ \exists y' (y \sim y' \text{ and } \mathrm{NUM}(x,y)). $$

**Stage 2 :** $\mathrm{ONE}'(y), \mathrm{EXP}'(y), \mathrm{TOP}'(y)$. We will construct these formulas such that if $D$ is a complete structure then $(D,a) \models \mathrm{ONE}'(y) \iff \mathrm{num}'(a)=1$; $(D,a) \models \mathrm{EXP}'(y) \iff \mathrm{num}'(a)=2^{2^n}$; $(D,a) \models \mathrm{TOP}'(y) \iff \mathrm{num}'(a)=2^{2^{2n}}-1$. We can write $\mathrm{ONE}(y)$ as $\forall x (\mathrm{MEM}(x,y) \leftarrow \rightarrow \mathrm{ONE}(x))$. We can write $\mathrm{EXP}'(y)$ as $\exists x_1 \exists x_2 \exists x_3 (\mathrm{ONE}(x_1) \land \mathrm{EXP}(x_2) \land \mathrm{ADD}(x_1, x_2, x_3) \land \forall x (\mathrm{MEM}(x,y) \leftarrow \rightarrow \mathrm{NUM}(x, x_3)))$. We can write $\mathrm{TOP}'(y)$ as $\forall x (\mathrm{MEM}(x,y))$.
**Stage 3 :** ADD'(y₁,y₂,y₃) We will construct ADD' such that if D is complete then (D,a,b,c) ⊨ ADD'(y₁,y₂,y₃) ⇔ num'(c) = num'(a) + num'(b). When constructing the formula ADD, we thought of a,b, and c as corresponding to binary strings of length 2n, and we wrote ADD as a conjunction of 2n formulas -- One for each of the 2n places. We now similarly think of a,b, and c as corresponding to binary strings of length 2$^{2n}$, and we wish to write ADD' as a conjunction of 2$^{2n}$ formulas -- One for each of the 2$^{2n}$ places. We clearly cannot write ADD' explicitly as a conjunction of 2$^{2n}$ formulas (for it would be too long), but we can use the quantifiers of L₂ to quantify over the 2$^{2n}$ places. We can therefore write ADD' in the form :

$$ \forall x_1 \forall x_2 \forall x_3 ((\text{ONE}(x_1) \wedge \text{ADD}(x_1, x_2, x_3)) \longrightarrow F(x_1, x_2, x_3, y_1, y_2, y_3)) $$

where F is simply a boolean combination of the formulas $MEM(x_i, y_j)$, $1 \le i, j \le 3$.

**Stage 4 :** COMP'. We will construct the sentence COMP' such that $D \models COMP' \Longleftrightarrow D$ is super-complete. We can write COMP' as :

$$ \begin{array}{l} \mathrm{COMP} \wedge \exists y_1[ \\ \quad \mathrm{ONE'}(y_1) \wedge \forall y (\neg \mathrm{TOP'}(y) \longrightarrow \exists z (\mathrm{ADD'}(y, y_1, z))) \\ \quad \wedge y_1 \in \underline{A}_{2n+1} \wedge \forall y \exists z ((y \in \underline{A}_{2n+1} \longrightarrow z \in \underline{A}_{2n+2}) \wedge (y \in \underline{A}_{2n+2} \longrightarrow z \in \underline{A}_{2n+3}) \\ \qquad \qquad \qquad \qquad \wedge \dots \wedge (y \in \underline{A}_{3n-1} \longrightarrow z \in \underline{A}_{3n})) \\ \quad \wedge \forall y \forall z ([ (y \in \underline{A}_{2n+1} \wedge z \in \underline{A}_{2n+2}) \vee (y \in \underline{A}_{2n+2} \wedge z \in \underline{A}_{2n+3}) \vee \dots \vee (y \in \underline{A}_{3n-1} \wedge z \in \underline{A}_{3n}) ] \\ \qquad \longrightarrow \mathrm{ADD'}(y, y_1, z))] \end{array} $$

**Stage 5 :** NUM'(y₁,y₂). We will construct NUM' such that

(D,a,b) ⊨ NUM'(y₁,y₂) ⇔ num'(a) = num'(b). We can write NUM'(y₁,y₂) as : $\forall x (MEM(x,y_1) \longleftrightarrow MEM(x,y_2))$.

**Stage 6 :** ORD'(y₁,y₂). We will construct ORD' such that if D is super-complete then (D,a,b) ⊨ ORD'(y₁,y₂) ⇔ num'(a) ≤ num'(b). We can write ORD'(y₁,y₂) as : $\exists y \mathrm{ADD'}(y_1,y,y_2)$.

**Stage 7 :** EN'(y). We will construct EN' such that if D is super-complete then

(D,a) ⊨ EN'(y) ⇔ num'(a)=n. We can write EN'(y) as $\exists z (z \in \underline{A}_{3n} \wedge \mathrm{NUM'}(y,z))$.
**Stage 8 :** $DIST'(y_1, y_2)$. We will construct $DIST'$ such that if $D$ super-complete then $(D, a, b) \models DIST'(y_1, y_2) \iff \text{num}'(b) = \text{num}'(a) + 2^{2^n}$. We can write $DIST'(y_1, y_2)$ as : $\exists z (\text{EXP}'(z) \land \text{ADD}'(y_1, z, y_2))$.

We now observe that the formulas $COMP', NUM', ORD', EN'$; and $DIST'$ suffice to prove Lemma 2 when $i=2$.

**Section 4 :**

In this section we state some further results. Theorem 2, due to Albert Meyer, strengthens Lemma 2 for the case $i=1$.

**Theorem 2 :** There exist constants $c, j>0$ such that the following is true : Let $m$ be a non deterministic Turing machine which recognizes $SAT(L_1^i)$; then for infinitely many $n$ there is a sentence $F \in SAT(L_1^i)$ of length $n$ such that any accepting computation of $m$ on $F$ uses either space $2^{cn/\log n}$ or time $2^{(cn/\log n)^2}$.

We now discuss some upper bounds on $SAT(L_1^k)$. Let $k$ be fixed. One can show using an Ehrenfeucht-game argument [5] that for some constant $d$, if $F \in SAT(L_1^k)$ is of length $n$, then $F$ is true in some structure whose domain is of size $\le 2^{2dn/\log n}$. Richard Tenney [6] shows that if $F \in SAT(L_2^k)$, then $F$ is true in some structure with domain of size $\le 2^{2dn/\log n}$. These theorems can be used to construct a nondeterministic machine $m_i$ which recognizes $SAT(L_1^{k_i})$ as follows : If the input is a sentence $F$ of length $n$, $m_i$ "guesses" a structure for $L_i$ with domain of size $\le f_i(\text{dn/}\log n)$, and explicit writes down this guess (keeping in mind that $m_i$ only guesses an interpretation of $A_j$ if $\underline{A}_j$ actually appaers in $F$) ; $m_i$ then checks whether or not $F$ is true in this structure, and if so, accepts $F$. Using only a bit of care, we can obtain :

**Theorem 3 :** Let $i \in \{1, 2\}$ and $k \in N$. The for some constant $d$ there exists a non deterministic Turing machine which recognizes $SAT(L_1^k)$, and which operates within time $f_i(\text{dn/}\log n)$.

It should be remarked here that theorem 3 remains true even if we permit $L_1$ and $L_2$ to have in addition atomic formulas of the form $x_1=x_2$ and $A_1 \in A_2$.
We now define $L_1$ and $L_2$ to be the languages obtained from $L_1$ and $L_2$ by permitting quantification over the monadic predicates $A_j$ as well as over the individual variables. A structure for $L_1$ is a set $D$ where the quantified individual variables range over $D$ as before and where the quantified set predicates now range over subsets of $D$, and a structure for $L_2$ is a pair $<D, \sim>$ defined similarly. The sentences of $L_1$ and $L_2$ are formulas where all occurrences of variables and set predicates are bound by quantifiers. For $i \in \{1,2\}$, let $S_i$ be the set of sentences of $L_i$ which are satisfiable, i.e., true in some structure.

At present, we see no way of taking advantage of non determinism in deciding membership in $S_1$ or $S_2$, and hence the best procedures we can come up with in theorem 4 have running times considerably worse than the times stated in theorem 3. The techniques of [5,6] suffice to prove results a bit weaker than below, but considerable subtleties have to be introduced in the case of both $S_1$ and $S_2$ in order to prove theorem 4.

**Theorem 4**: Let $i \in \{1,2\}$. There exists a deterministic Turing machine which recognizes $S_i$ within space $f_i(\text{dn/logn})$ for some constant $d$, and hence within time $\frac{f_i(\text{en/logn})}{2}$ for some constant $e$.
References :

[1] Fischer, M.J and Rabin M.O., "Super-exponential complexity of Presburger arithmetic", Proc. AMS. Symp. On Complexity of Real Computational Processes, 1974, to appear ; also, MAC Tech. Memo. 43, M.I.T., 1974.

[2] Meyer, A.R., "Weak monadic second order theory of successor is not elementary-recursive", Boston Univ. Logic Colloquium Proc., to appear 1974 ; also MAC Tech. Memo 38, M.I.T., 1973.

[3] Seiferas, J., Nondeterministic time and space complexity classes", Project MAC Tech. Report 137, M.I.T., 1974

[4] Stockmeyer, L.J., "The complexity of decision problems in automata theory and logic", Project MAC Tech. Report 133, M.I.T., 1974.

[5] Ehrenfeucht, A., "An application of games to the complet problem for formalized theories", Fund. Math. 49 1961, 129-141.

[6] Tenney, R.L., "Decidable pairing functions", Dept. Comp. Sci, Cornell Univ., Tech. Report 72-136, 1972.