The quantified formula expressing reachability between two configurations

Fix a family of vertices encoded by bit strings of length $m$, together with a chosen quantifier-free formula $\mathrm{Next}(U,V)$ of size $O(m)$ asserting that the encoded vertex $V$ is reachable from $U$ by one legal graph edge. In the application to PSPACE-hardness, $\mathrm{Next}$ is the one-step configuration predicate for a fixed machine on a fixed input length. Let ${\mathrm{Eq}}_m(U,V)$ be the quantifier-free formula asserting bitwise equality of the strings $U$ and $V$, and abbreviate ${\mathrm{PairEq}}_m((Y,Z),(U,V)):={\mathrm{Eq}}_m(Y,U)\wedge {\mathrm{Eq}}_m(Z,V)\mathrm{.}$

For each $i\in \mathbb{N}$, define an open prenex formula ${\mathrm{\Theta }}_i(U,V)$, whose only free variables are the endpoint blocks $U,V$, recursively as follows:

${\mathrm{\Theta }}_0(U,V):={\mathrm{Eq}}_m(U,V)\vee \mathrm{Next}(U,V),$

and for $i\ge 1$, first write the already prenex previous formula, after renaming all its bound variables freshly, as ${\mathrm{\Theta }}_{i-1}(Y,Z)=Q_1{X}_1\cdots Q_t{X}_t{\rho }_{i-1}(Y,Z,X_1,\dots ,X_t),$ where ${\rho }_{i-1}$ is quantifier-free, and set ${\mathrm{\Theta }}_i(U,V):=\mathrm{\exists }W\mathrm{\forall }b\mathrm{\exists }Y\mathrm{\exists }Z{Q}_1{X}_1\cdots Q_t{X}_t(((b=0)\to {\mathrm{PairEq}}_m((Y,Z),(U,W)))\wedge ((b=1)\to {\mathrm{PairEq}}_m((Y,Z),(W,V)))\wedge {\rho }_{i-1}(Y,Z,X_1,\dots ,X_t))\mathrm{.}$

The variable $W$ is the midpoint candidate, the one-bit variable $b$ chooses left or right half, and the variables $Y,Z$ feed the single recursive copy of ${\mathrm{\Theta }}_{i-1}$.

• The symbols $b=0$, $b=1$, and $P\to Q$ abbreviate quantifier-free Boolean formulas built from $0,1,\mathrm{\neg },\wedge ,\vee$. Thus the displayed construction is genuinely prenex. After the endpoint blocks $U,V$ are replaced by fixed bit strings, ${\mathrm{\Theta }}_i(U,V)$ is a closed quantified Boolean formula in the sense of Quantified Boolean formulas and the language TQBF.
• The naive formula $\mathrm{\exists }W({\mathrm{\Theta }}_{i-1}(U,W)\wedge {\mathrm{\Theta }}_{i-1}(W,V))$ duplicates the previous level. The present definition is the size-controlled version used for the PSPACE-hardness proof.
• The intended meaning is that ${\mathrm{\Theta }}_i(U,V)$ says that $V$ is reachable from $U$ by a path of length at most $2^i$.