Need help in understanding proof "approach" and meaning for "1st order Theory of dense linear orders w/o endpoints is PSPACE complete"

Question

So in my class we are giving a proof for 1st order Theory of dense linear orders w/o endpoints is PSPACE complete.

The proof that it is in PSPACE is basically to reduce TQBF. Let $\phi = \exists x_1 \forall x_2... \exists x_m \ \psi(x_1, x_2, ...x_m)$

So we provide mapping $x_i \mapsto (x_i \geq x_0)$ and $ x' \mapsto (x_i \geq x_o)'$

Let $\phi' = \exists x_1 \exists x_1 \forall x_2... \exists x_m \ \psi'(x_0, x_1, x_2, ...x_m)$

Not sure how we proved it with this mapping.

But what I want to ask here is to how reason about what we need to proof here. I guess it is the first I need to understand before diving into the actual formal proof.

I understand that in order to proof completeness we need to show that the problem is

1. is in PSPACE

2. hard for PSPACE

As I understand PSPACE problem is a problem that can be solved by deterministic TM in order of polynomial space.

So there is a thing that bugs me. What it mean to solve a "problem" by TM where problem is 1st order Theory? So 1st order theory is a set of different logic formulas. What does it mean 1st order Theory to be in PSPACE? Does it mean that we have TM and on input x we can decide whether this formula is in our Theory or it is not in our Theory? If yes, what is the procedure to decide it?

I am confused regarding it A LOT.

Thank you for any help!

Answer 1

The theory $T_{dlo}$ of dense linear orders without endpoints is complete: for every sentence $S$ of the language $\{<\}$, either $T_{dlo}\vdash S$ or $T_{dlo}\vdash \neg S$. In fact, $T_{dlo}$ admits elimination of quantifiers: for every sentence $\varphi$ of the theory there is an open formula $\psi$ such that $T_{dlo}\vdash \varphi \leftrightarrow \psi$.

In their book "The Computational Complexity of Logical Theories" (1979), Ferrante & Rackoff present a related result and many others on the same theme. There they present their algorithm for producing $psi$ from $varphi$ in the theory of $\mathbb{Q}$ as a field. The algorithm is also described in the latter half of this pdf of slides. (Caution: in that pdf, negation symbols render as empty rectangles, for me.) It proceeds by eliminating existential quantifiers and negations. Where their algorithms introduce a new term $(a+b)/2$, an analogous algorithm for $T_{dlo}$ would introduce a new constant $c$ and conjoin $a < c \wedge c < b$ to the formula being constructed.

So there is an effective procedure for determining whether sentences in the language of dense linear orderings without endpoints is a theorem or not.

The statement you're asking about says exactly the two things you mention:

1. (deciding $T_{dlo}$ is in PSPACE) There is a Turing machine $M$ which decides theoremhood for sentences of the language, such that the space complexity of $M$ is polynomial as a function of the "size" of input sentences, and that this is a lower bound, in the sense that
2. (deciding $T_{dlo}$ is PSPACE-hard) There is a reduction of a PSPACE-complete problem (TQBF) the algorithm of 1.