# Is PSPACE closed under the following forall-there-exists construction?

Suppose I have a language $L$ (over alphabet $\Sigma$), such that $$w \in L \iff (\forall x \in \Sigma^*) (\exists y \in \Sigma^*) P(x,y,w).$$ and I can give a turing machine that decides $P(x,y,w)$ in polynomial space in $w$, where $x$ and $y$ are given as separate read-only, forward-only tapes. That is, on input $x$ in tape 1, $y$ in tape 2, and $w$ in tape 3, I use only a polynomial-in-$w$ amount of tape 3's space, and I only move forwards in tape 1 and tape 2.

Does this imply $L \in \text{PSPACE}$?

I feel it should, because if there were only one quantifier, say ($\exists y \in \Sigma^*) P(y,w)$, then $\text{NPSPACE} = \text{coNPSPACE} = \text{PSPACE}$ implies the result. But somehow for two quantifiers I can't figure out how to prove this. I should be able to eliminate the tape $y$ using $\text{NPSPACE} = \text{PSPACE}$, but I don't know if this result still holds in the presence of the additional tape $x$.

• How is the titular question the same as the one in the body? – Raphael Apr 17 '17 at 19:52
• @Raphael what do you mean? The body gives a precise description of my question, and the title attempts to summarize that (but without all the precise details). – 6005 Apr 18 '17 at 1:11
• Closure properties are of the form $L \in A \implies f(L) \in A$ (in the unary case). What is $L$ here? (Your $L$ is my $f(L)$.) – Raphael Apr 18 '17 at 7:58
• @Raphael Think of the closure property prefix: $w\in P \Leftrightarrow (\exists y\in\Sigma^*) wy\in L$. Only here the closure is from ternary predicate to unary predicate (which is a language). Seems OK to me. – Hendrik Jan Apr 18 '17 at 12:24