Let $\mathbf{FO^2}$ be the fragment of first-order logic consisting of sentences with at most two variables and no function symbols. It is well known that satisfiability for $\mathbf{FO}^2$ is decidable (see [1], for instance). Furthermore, in that same paper, it is argued that $\mathbf{FO^2}$ satisfiability is $\mathbf{NEXPTIME}$-complete, and that this result follows from these two lemmas:

  1. Satisfiability for $\mathbf{FO^2}$ is in $\mathbf{NTIME}(2^{O(n)})$.
  2. Satisfiability for $\mathbf{FO^2}$ has a lower complexity bound of the form $\mathbf{NTIME}(2^{cn/\log{n}})$ for some positive constant $c$.

I don't have a lot of background in complexity theory, so this has left me with two questions:

  1. Is it easy to see that these two lemmas imply $\mathbf{NEXPTIME}$-completeness?
  2. Is this result not contradictory? By definition, $\mathbf{NEXPTIME} = \bigcup_{k \in \mathbb{N}}\mathbf{NTIME}(2^{n^k})$, and by the non-deterministic time hierarchy theorem we have for any $i, j \in \mathbb{N}$ that $\mathbf{NTIME}(2^{n^i}) \subsetneq \mathbf{NTIME}(2^{n^j})$ if $i < j$. So I'm wondering how a problem complete for the class can lie at the "lowest rung" of the ladder - is this because Karp-reductions can blow-up the size of an input polynomially?


[1] On the Decision Problem for Two-Variable First-Order Logic - Grädel, Kolaitis and Vardi


1 Answer 1


Regarding your first question: I haven't read the paper, but I guess that the proof of the second lemma is by a polynomial time reduction from a generic $\mathbf{NEXPTIME}$-hard problem. This establishes $\mathbf{NEXPTIME}$-hardness. Membership in $\mathbf{NEXPTIME}$ is by the first lemma. Regarding the second question, your guess is correct.

  • $\begingroup$ Thanks for your comments - no such reduction is described in the paper, so I guess it must be in one of the references. I'll do some digging! $\endgroup$ Nov 1, 2019 at 9:37
  • 1
    $\begingroup$ My guess would have been that the proof is by encoding the word problem for linearly exponential-time bounded nondet Turing machines (which is nexptime- hard) into a formula. If this encoding can be computed in quasi linear time, this is the desired reduction... $\endgroup$ Nov 1, 2019 at 9:46
  • 1
    $\begingroup$ It seems like such a reduction is described in Complexity Results for Classes of Quantificational Formulas [Lewis]. $\endgroup$ Nov 1, 2019 at 10:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.