Насколько сложна теория $2$?

Question

Мотивировано https://math.stackexchange.com/questions/3757967/are-there-any-sets-of-axioms-that-have-an-efficient-algorithm-for-all-provable-s, Хочу спросить:

В чем сложность теории первого порядка двухэлементного чистого множества $\bf 2$?

(Обратите внимание, что ответ будет таким же, если мы заменим ${\bf 2}$ любым конечным чистым множеством с более чем одним элементом.)

Аргумент моего ответа на связанный вопрос показывает, что оба $\mathsf{SAT}$ сводится к $\Sigma_1$ фрагмент этой проблемы: есть эффективный способ преобразовать пропозициональное предложение $\varphi$ в предложение первого порядка $\hat{\varphi}$ такой, что ${\bf 2}\models\hat{\varphi}$ если только $\varphi$выполнимо. Вдвойне конечно это означает, что$\mathsf{coSAT}$ сводится к $\Pi_1$ фрагмент.

Рассматривая поведение добавления кванторов, естественное предположение о том, что ответ должен быть в точности объединением уровней в полиномиальной иерархии, но я не сразу вижу детали.

Answer 1

Учитывая, что квантифицированные логические формулы являются PSPACE-полными и могут быть сведены к чистой теории первого порядка $2$, это PSPACE-сложно. С другой стороны, это также явно в PSPACE (поскольку очевидный рекурсивный алгоритм полиномиален в использовании пространства). Так что это PSPACE-complete.