TQBF is in PSPACE

If $\mathrm{\Phi }$ has no quantifiers, then by [L1] one only needs to evaluate a quantifier-free Boolean formula under a fully specified truth assignment. That can be done by a deterministic left-to-right parse using space polynomial in $\mathrm{\mid }\mathrm{\Phi }\mathrm{\mid }$.

Suppose $\mathrm{\Phi }$ begins with $\mathrm{\exists }x\mathrm{\Psi }(x)$. Recursively evaluate $\mathrm{\Psi }(0)$ and, if necessary, $\mathrm{\Psi }(1)$; accept exactly when at least one branch returns true. If instead $\mathrm{\Phi }$ begins with $\mathrm{\forall }x\mathrm{\Psi }(x)$, recursively evaluate both $\mathrm{\Psi }(0)$ and $\mathrm{\Psi }(1)$ and accept exactly when both are true. By [L1], this is exactly the truth definition of the quantified formula.

The recursion depth is at most the number of quantified variables, hence at most $\mathrm{\mid }\mathrm{\Phi }\mathrm{\mid }$. At each level the machine stores the current parse position and the current partial assignment, both of polynomial size. So the whole depth-first evaluation uses polynomial space, even though it may take exponential time.

By [L2], the deterministic recursive evaluator places TQBF in PSPACE.