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:


Satisfiability for $\mathbf{FO^2}$ is in $\mathbf{NTIME}(2^{O(n)})$.
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:


Is it easy to see that these two lemmas imply $\mathbf{NEXPTIME}$-completeness?
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 &lt; 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
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.