Quão complicada é a teoria de $2$?

Question

Motivado por https://math.stackexchange.com/questions/3757967/are-there-any-sets-of-axioms-that-have-an-efficient-algorithm-for-all-provable-s, Gostaria de perguntar:

Qual é a complexidade da teoria de primeira ordem do conjunto puro de dois elementos $\bf 2$?

(Observe que a resposta será a mesma se substituirmos ${\bf 2}$ por qualquer conjunto puro finito com mais de um elemento.)

O argumento da minha resposta à pergunta vinculada mostra que ambos $\mathsf{SAT}$ reduz ao $\Sigma_1$ fragmento deste problema: há uma maneira eficiente de transformar uma frase proposicional $\varphi$ em uma frase de primeira ordem $\hat{\varphi}$ de tal modo que ${\bf 2}\models\hat{\varphi}$ sse $\varphi$é satisfazível. É claro que isso significa que$\mathsf{coSAT}$ reduz ao $\Pi_1$ fragmento.

Considerando o comportamento de adicionar quantificadores, uma suposição natural em uma resposta é que deveria ser exatamente a união dos níveis na hierarquia polinomial, mas não vejo os detalhes imediatamente.

Answer 1

Dado que Quantified Boolean Formulas é PSPACE-completo e pode ser reduzido à pura teoria de primeira ordem de $2$, é PSPACE-difícil. Por outro lado, também está claramente no PSPACE (já que o algoritmo recursivo óbvio é polinomial no uso do espaço). Portanto, é PSPACE completo.