Betapa rumitnya teori $2$?

Question

Dimotivasi oleh https://math.stackexchange.com/questions/3757967/are-there-any-sets-of-axioms-that-have-an-efficient-algorithm-for-all-provable-s, Saya ingin bertanya:

Berapa kompleksitas teori orde pertama dari himpunan murni dua elemen $\bf 2$?

(Perhatikan bahwa jawabannya akan sama jika kita mengganti ${\bf 2}$ oleh himpunan murni hingga apa pun dengan lebih dari satu elemen.)

Argumen jawaban saya atas pertanyaan terkait menunjukkan bahwa keduanya $\mathsf{SAT}$ dikurangi menjadi $\Sigma_1$ fragmen masalah ini: ada cara yang efisien untuk mengubah kalimat proposisional $\varphi$ menjadi kalimat urutan pertama $\hat{\varphi}$ seperti yang ${\bf 2}\models\hat{\varphi}$ iff $\varphi$memuaskan. Tentu saja ini berarti$\mathsf{coSAT}$ dikurangi menjadi $\Pi_1$ pecahan.

Mempertimbangkan perilaku menambahkan bilangan, tebakan alami pada jawaban adalah bahwa itu harus persis gabungan level dalam hierarki polinomial, tetapi saya tidak segera melihat detailnya.

Answer 1

Mengingat Rumus Kuantifikasi Boolean lengkap dengan PSPACE dan dapat direduksi menjadi teori orde pertama murni $2$, ini PSPACE-hard. Di sisi lain, itu juga jelas di PSPACE (karena algoritma rekursif yang jelas adalah polinomial dalam penggunaan ruang). Jadi PSPACE sudah lengkap.