# On satisfiability for 2-variable FOL being NEXPTIME-complete

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?

REFERENCES

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

## 1 Answer

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.

• 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! – Guy Paterson-Jones Nov 1 '19 at 9:37
• 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... – Hermann Gruber Nov 1 '19 at 9:46
• It seems like such a reduction is described in Complexity Results for Classes of Quantificational Formulas [Lewis]. – Guy Paterson-Jones Nov 1 '19 at 10:13