Motivated by this question, I'd like to ask:
What is the complexity of the first-order theory of the two-element pure set $\bf 2$?
(Note that the answer will be the same if we replace ${\bf 2}$ by any finite pure set with more than one element.)
The argument of my answer to the linked question shows that both $\mathsf{SAT}$ reduces to the $\Sigma_1$ fragment of this problem: there is an efficient way to transform a propositional sentence $\varphi$ into a first-order sentence $\hat{\varphi}$ such that ${\bf 2}\models\hat{\varphi}$ iff $\varphi$ is satisfiable. Dually of course this means that $\mathsf{coSAT}$ reduces to the $\Pi_1$ fragment.
Considering the behavior of adding quantifiers, a natural guess at an answer is that it should be exactly the union of the levels in the polynomial hierarchy, but I don't immediately see the details.
Given that Quantified Boolean Formulas is PSPACE-complete and can be reduced to the pure first-order theory of $2$, it's PSPACE-hard. On the other hand, it's also clearly in PSPACE (since the obvious recursive algorithm is polynomial in space usage). So it's PSPACE-complete.