TQBF is PSPACE-complete

Parse a TQBF input of length $N$, rejecting violations of the statement's syntax. Keep the parsed formula and a table of assigned bits. Recursively assign the next quantified variable 0, evaluate the remaining prefix, save that answer bit, then assign it 1 and evaluate again using the same child workspace. Combine with OR or AND as indicated and undo the assignment. A frame stores an input position and the saved bit; at most $N$ frames and a size-$O(N^2)$ parsed representation suffice. Matrix evaluation likewise uses at most $O(N^2)$ cells. Every recursive call decreases the remaining prefix length; the finite matrix recursion terminates. The empty prefix evaluates the variable-free matrix directly. Counting input cells as well still gives polynomial space.

Fix a decider $M$ of $L$ and a known integer polynomial $S(n)\ge n+k+1$ bounding its visited cells on every input. On input $x$, represent each tape by its first $S=S(\mathrm{\mid }x\mathrm{\mid })$ symbols and its head offset, together with the state. All actual configurations fit because each tape's visited prefix is at most $S$ and the complete input fits too. Use fixed-width fields and add a tag for one special accepting vertex $a_{\ast }$. Invalid state/symbol codes and head offsets outside $0,\dots ,S-1$ are excluded; the special vertex has all remaining fields zero. Choose one common bit length $m=O_M(S)$ for all these vertices. This is the explicit full-prefix variant of F3's bounded coding. There are at most $2^m$ vertices, including $a_{\ast }$. The initial vertex $s_x$ is written directly from $x$.

Construct a Boolean formula $E(X,Y)$ for edges of this finite graph. For every possible state, scanned-symbol tuple and head-offset tuple, enumerate the finitely specified instruction of $M$, assert those source fields, the target state and the componentwise head offsets (using F4's clamped-left rule on each right-infinite tape), the prescribed written symbols, and equality of every unscanned tape cell. Conjoin validity of both endpoint codes. There are $O_M(S^k)$ cases and $O_M(S)$ field comparisons in each, with $O(\log (S+1))$ bits per offset. Thus the disjunction has polynomial encoded size and is produced by polynomial finite loops. Omit transitions leaving the represented interval. Add edges from every ordinary accepting configuration to $a_{\ast }$, and a self-loop at $a_{\ast }$. Rejecting configurations have no outgoing edges. This supplies a unique terminal target without assuming a physical tape-erasing normalization. From the initial vertex, ordinary edges are exactly M's steps; actual runs never leave the interval. Thus $a_{\ast }$ is reachable exactly when M accepts $x$.

Let $R_0(X,Y)$ be $\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{i}\mathrm{d}(X)\wedge \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{i}\mathrm{d}(Y)\wedge (X=Y\vee E(X,Y))$. For each next level introduce fresh $m$-bit vectors $Z,U,V$ and a fresh bit $b$. Set $G=(\mathrm{\neg }b\wedge U=X\wedge V=Z)\vee (b\wedge U=Z\wedge V=Y)$, and define $R_{i+1}(X,Y)=\mathrm{\exists }Z\mathrm{\forall }b\mathrm{\forall }U\mathrm{\forall }V(\mathrm{\neg }G\vee R_i(U,V))$. Here equality means conjunction of bit equalities, each expanded with AND, OR and NOT. There is just one occurrence of $R_i$.

For all bit vectors $X,Y$, $R_i(X,Y)$ holds iff they are valid vertices joined by a path of length at most $2^i$. At level zero this follows from its definition, including the length-zero path. For the successor, a true formula supplies a midpoint $Z$. Specializing the universals to $b=0,(U,V)=(X,Z)$ and $b=1,(U,V)=(Z,Y)$ forces both shorter paths by the induction hypothesis; concatenate them. Conversely split a path of length $h\le 2^{i+1}$ after $\min (h,2^i)$ edges. Both portions have length at most $2^i$, so their midpoint works. For any universal assignment either $G$ is false, making the implication true, or it selects one of these two paths. Invalid midpoints cannot pass either selected base validity condition. This proves the induction in both directions.

Any reachable vertex has a path without a repeated vertex: delete the segment between two equal vertices and retain its subsequent edges, reducing the length until no repetition remains. Its length is less than $2^m$. Therefore $R_m(s_x,a_{\ast })$ is true exactly when $x\in L$. If $s_x$ already equals a target in another instance, the equality part of $R_0$ handles it; here the distinct special tag keeps the actual initial and accepting target separate.

Each recursion level introduces $3m+1$ bound bits and $O(m)$ equality/connective occurrences. Distinct variable names across $m$ levels use $O(\log (m+2))$ bits, so the total encoded size is the polynomial base size plus $O(m^2\log (m+2))$. Put the formula in prenex form without duplication: if $z$ is fresh for $A$, then $A\vee (QzB)$ and $Qz(A\vee B)$ have the same truth value, for either quantifier, by checking whether $A$ is true or false and using the nonempty domain $\{0,1\}$. Apply this identity to pull each inner prefix through its outer guard. Fresh naming prevents capture. Each matrix connective remains once. Finite generation of the base cases, guards and prefix requires polynomial time and space, including substituting constant start/target bits. This proves the total reduction and, with step 1.1, PSPACE-completeness. All selections were finite enumerations or existential witnesses to a single formula; AC is unnecessary.

The same reduction may use a 3CNF or 3DNF matrix if desired. For each gate $v=\mathrm{\neg }u$, use $(v\vee u)\wedge (\mathrm{\neg }v\vee \mathrm{\neg }u)$; for $v=u\wedge w$, use $(\mathrm{\neg }v\vee u)\wedge (\mathrm{\neg }v\vee w)\wedge (v\vee \mathrm{\neg }u\vee \mathrm{\neg }w)$; for OR, dualize the AND clauses. Pin a constant by a unit clause and require the output by a unit clause. These are clauses of width at most three. For each assignment to the old variables, a gate-by-gate induction shows that exactly one assignment to the fresh gate variables satisfies all gate equations, and it satisfies the output unit exactly when $F=1$. This proves the pointwise property rather than inferring it from F7's mere equisatisfiability. Append existential quantifiers for the fresh gate bits after the old prefix; the resulting 3CNF preserves truth through every old quantifier. Alternatively apply this construction to $\mathrm{\neg }F$. Then $F=1$ iff every gate assignment falsifies $C_{\mathrm{\neg }F}$. Append universal gate quantifiers and use the matrix $\mathrm{\neg }{C}_{\mathrm{\neg }F}$, a disjunction of terms each containing at most three literals by De Morgan's laws. These conversions preserve the truth of the quantified formula in both directions, including constant matrices. They do not assert a polynomial DNF for unquantified equality without extra variables.

Here is also precise workspace accounting for generation: with read-only input and write-only output excluded from the auxiliary workspace measure, the fixed-M reduction uses $O_M(\log (n+2))$ auxiliary cells. Compute the fixed polynomial S and m in binary with a constant number of $O(\log (n+2))$-bit registers. The base edge formula is output by loops over k head offsets, finite states/symbols, tape cells and bit positions, all polynomially bounded; k is fixed, so the number of loop registers is constant. Initial-configuration bits are obtained by rescanning x with a binary position counter. Output the prenex prefix with one descending level counter; output the guards in the same order, using the current level to name its endpoint vectors, then the base formula, then the required closing symbols by a counter. The one-copy recurrence never requires storing a stack of levels. Every emitted variable name is computed from its level, vector type and bit offset, all polynomially bounded integers.

If a restricted matrix is requested, generate its gate clauses using rescans of that regular unquantified matrix. Number connective occurrences by their positions. Find a node's children by scanning its prefix-encoded subtree with a pending-child counter: reading a node changes the counter by its arity minus one, and zero marks the end of the subtree. Constants have arity zero. All indices and counters are bounded by the polynomial output length. Each requested matrix symbol can be recomputed by restarting the generator of step 7.2 and counting its output; save the constant number of current position registers on separate tracks. Thus iterating over gate positions and their children uses only a constant number of logarithmic registers, with polynomial repeated-scan time. Output F7's clauses, or their De Morgan negations with the appropriate new quantifiers from step 7.1. This proves regular logspace generation under the explicitly stated input/output-excluding convention, without claiming an all-tape visited-space bound smaller than n.