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
is in PSPACE
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!