Quanto è complicata la teoria di $2$?

Question

Motivato da https://math.stackexchange.com/questions/3757967/are-there-any-sets-of-axioms-that-have-an-efficient-algorithm-for-all-provable-s, Vorrei chiedere:

Qual è la complessità della teoria del primo ordine dell'insieme puro a due elementi $\bf 2$?

(Nota che la risposta sarà la stessa se sostituiamo ${\bf 2}$ da qualsiasi insieme puro finito con più di un elemento.)

L'argomento della mia risposta alla domanda collegata mostra che entrambi $\mathsf{SAT}$ si riduce al $\Sigma_1$ frammento di questo problema: esiste un modo efficiente per trasformare una frase proposizionale $\varphi$ in una frase del primo ordine $\hat{\varphi}$ tale che ${\bf 2}\models\hat{\varphi}$ iff $\varphi$è soddisfacente. Ovviamente questo significa che$\mathsf{coSAT}$ si riduce al $\Pi_1$ frammento.

Considerando il comportamento dell'aggiunta di quantificatori, una risposta naturale è che dovrebbe essere esattamente l'unione dei livelli nella gerarchia polinomiale, ma non vedo immediatamente i dettagli.

Answer 1

Dato che Quantified Boolean Formulas è PSPACE-completo e può essere ridotto alla pura teoria del primo ordine di $2$, è difficile per PSPACE. D'altra parte, è anche chiaramente in PSPACE (poiché l'ovvio algoritmo ricorsivo è polinomiale nell'uso dello spazio). Quindi è completo per PSPACE.