0
$\begingroup$

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!

$\endgroup$
0
$\begingroup$

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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.