The IP = PSPACE Theorem

Let $F$ be a field (Field) and let $m\ge 1$. For a polynomial $P\in F[X_1,\dots ,X_m]$ and an index $1\le i\le m$, write $P{\mathrm{\mid }}_{X_i=0},P{\mathrm{\mid }}_{X_i=1}$ for the two polynomials in $F[X_1,\dots ,X_{i-1},X_{i+1},\dots ,X_m]$ obtained by substituting the field elements $0$ and $1$ for $X_i$. Define the field quantifier operators $A_{X_i}P:=(P{\mathrm{\mid }}_{X_i=0})(P{\mathrm{\mid }}_{X_i=1}),E_{X_i}P:=1-(1-P{\mathrm{\mid }}_{X_i=0})(1-P{\mathrm{\mid }}_{X_i=1}),$ both of which again lie in $F[X_1,\dots ,X_{i-1},X_{i+1},\dots ,X_m]$.

Let $\mathrm{\Phi }=Q_1{x}_1{Q}_2{x}_2\cdots Q_n{x}_n\psi$ be a closed prenex quantified Boolean formula (Quantified Boolean formulas and the language TQBF) with quantifier-free matrix $\psi$, and let $b:=P_{\psi }\in F[X_1,\dots ,X_n]$ be the arithmetization of the matrix (Arithmetization of Boolean formulas). The ordered arithmetization of $\mathrm{\Phi }$ over $F$ is the constant obtained from $b$ by processing the quantifiers from the innermost to the outermost: put $P^{(n)}:=b$ and, for $j=n,n-1,\dots ,1$, put $P^{(j-1)}:=A_{X_j}{P}^{(j)}$ when $Q_j=\mathrm{\forall }$ and $P^{(j-1)}:=E_{X_j}{P}^{(j)}$ when $Q_j=\mathrm{\exists }$. The resulting $P^{(0)}$ is a polynomial in no variables, hence a field element.

• The operators act on the polynomial and the index, not on a formula tree: each specialization is a well-defined polynomial in the remaining variables, and the two displayed expressions are computed in that polynomial ring. No enumeration, decomposition, isomorphism or choice is made in the definition, and no expansion into monomials is required.
• The convention "inner quantifiers first" is used throughout this page: the prefix is read left to right and $Q_n$, the innermost quantifier, is processed first, so $Q_1$ is processed last. The operator list of Multilinearization in one variable refines this ordered convention.
• The field elements $0$ and $1$ are the two Boolean values, and they are distinct in a field. The gate operations reproduce the truth tables only at Boolean inputs; that agreement is the subject of Quantifier polynomials agree with QBF semantics on Boolean assignments, and no such agreement is asserted here.
• The definition itself does not assert a truth-value theorem. For the multilinearized refinement of this sequence in Multilinearization in one variable, agreement with QBF truth is proved in The ordered arithmetization evaluates to the quantified Boolean truth value.
• For $n=0$ the matrix is a formula with no variable occurrences, $b\in F$ is a constant, and $P^{(0)}=b$.

Let $F$ be a field, let $\phi (x,y_1,\dots ,y_m)$ be a quantifier-free Boolean formula on the variables $x,y_1,\dots ,y_m$ with $m\ge 0$, and let $P:=P_{\phi }\in F[X,Y_1,\dots ,Y_m]$ be its arithmetization. Then for every Boolean assignment $a\in \{0,1{\}}^m$ to $y_1,\dots ,y_m$ the two operators of Field arithmetization of QBF quantifiers satisfy $(A_{X}P)(a)=\text{the truth value of }\mathrm{\forall }x\phi (x,a),(E_{X}P)(a)=\text{the truth value of }\mathrm{\exists }x\phi (x,a),$ where Boolean truth values are embedded in $F$ as $0$ and $1$.

Let $F$ be a field and let $P\in F[X_1,\dots ,X_m]$ with $m\ge 1$. For $1\le i\le m$ define the multilinearization of $P$ in $X_i$ by $R_{X_i}P:=(1-X_i)(P{\mathrm{\mid }}_{X_i=0})+X_i(P{\mathrm{\mid }}_{X_i=1})\mathrm{.}$ This is a polynomial in $F[X_1,\dots ,X_m]$ of degree at most one in $X_i$; in every other variable its degree is at most the corresponding degree of $P$.

Let $\mathrm{\Phi }=Q_1{x}_1\cdots Q_n{x}_n\psi$ be a closed prenex quantified Boolean formula (Quantified Boolean formulas and the language TQBF) with quantifier-free matrix $\psi$ and matrix arithmetization $b=P_{\psi }$ (Field arithmetization of QBF quantifiers). The multilinearized ordered arithmetization of $\mathrm{\Phi }$ is obtained from $b$ by applying, for $j=n,n-1,\dots ,1$, first the $j$ reductions $R_{X_1},R_{X_2},\dots ,R_{X_j}$ in this order and then the quantifier operator $O_j$, where $O_j:=A_{X_j}$ when $Q_j=\mathrm{\forall }$ and $O_j:=E_{X_j}$ when $Q_j=\mathrm{\exists }$. The operator list of $\mathrm{\Phi }$ is the resulting sequence of operations read in application order, $R_{X_1},\dots ,R_{X_n},O_n,R_{X_1},\dots ,R_{X_{n-1}},O_{n-1},\dots ,R_{X_1},O_1,$ and its length is denoted $T$. Then $T=n(n+1)\mathrm{/}2+n=n(n+3)\mathrm{/}2$, and for $n=0$ the list is empty.

Write $P^{(n)}:=b$. For $j=n,\dots ,1$, write $M_j$ for the polynomial obtained from $P^{(j)}$ by the $j$ reductions of the $j$-th block, and $P^{(j-1)}:=O_j(M_j)$. The final $P^{(0)}$ is a constant.

• Substituting $X_i=0$ into $R_{X_i}P$ gives $(1-0)P{\mathrm{\mid }}_{X_i=0}+0=P{\mathrm{\mid }}_{X_i=0}$, and substituting $X_i=1$ gives $P{\mathrm{\mid }}_{X_i=1}$; so $R_{X_i}P$ agrees with $P$ where the substituted variable is Boolean, and its coefficient of $X_i$ is $P{\mathrm{\mid }}_{X_i=1}-P{\mathrm{\mid }}_{X_i=0}$.
• Reductions in distinct variables commute with one another, because $R_{X_i}$ alters only the $X_i$-dependence. The displayed order is the one the interactive protocol of The Shamir interactive protocol for TQBF reverses; it is recorded here so that the protocol has a definite node list.
• The operator list is not the same as the ordered arithmetization of Field arithmetization of QBF quantifiers: the reductions are inserted before each quantifier operation, and they are what keep the individual degrees of the intermediate polynomials bounded. That bound, together with the agreement of the sequence with the Boolean semantics, is proved in Multilinearization preserves Boolean values and bounds individual degree and The ordered arithmetization evaluates to the quantified Boolean truth value.

Let $F$ be a field and $R_{X_i}$ the reduction of Multilinearization in one variable.

1. For every $P\in F[X_1,\dots ,X_m]$ and $b\in \{0,1\}$, $(R_{X_i}P){\mathrm{\mid }}_{X_i=b}=P{\mathrm{\mid }}_{X_i=b}$. Consequently, if $P$ agrees with a function on the Boolean cube at every Boolean point, then so does $R_{X_i}P$.
2. $R_{X_i}P$ has degree at most one in $X_i$, and degree in every other variable at most that of $P$ there.
3. Let $\mathrm{\Phi }=Q_1{x}_1\cdots Q_n{x}_n\psi$ be a closed prenex quantified Boolean formula whose quantifier-free matrix $\psi$ has $L$ syntax nodes, let $b=P_{\psi }$ and $D:=\max (L,2)$, and let $P^{(j)}$ and $M_j$ be the polynomials of the multilinearized ordered arithmetization. Then each $P^{(j)}$ with $j\le n-1$ has individual degree at most $2$ in each of $x_1,\dots ,x_j$, each $M_j$ is multilinear in $x_1,\dots ,x_j$, and every node polynomial of the operator list, after substituting arbitrary field elements for all variables other than its active variable, has degree at most $D$ in that active variable. The operator list has $T=n(n+3)\mathrm{/}2=O(n^2)$ entries.

Let $F$ be a field, let $\mathrm{\Phi }=Q_1{x}_1\cdots Q_n{x}_n\psi$ be a closed prenex quantified Boolean formula with quantifier-free matrix $\psi$ (Quantified Boolean formulas and the language TQBF), let $b=P_{\psi }$ be its matrix arithmetization (Arithmetization of Boolean formulas), and let $P^{(n)}=b,P^{(n-1)},\dots ,P^{(0)}$ be the multilinearized ordered arithmetization of $\mathrm{\Phi }$ (Multilinearization in one variable). For $0\le j\le n$ put ${\mathrm{\Psi }}_j:=Q_{j+1}{x}_{j+1}\cdots Q_n{x}_n\psi ,$ so that ${\mathrm{\Psi }}_n=\psi$ and ${\mathrm{\Psi }}_0=\mathrm{\Phi }$, and ${\mathrm{\Psi }}_j$ has free variables $x_1,\dots ,x_j$. Then for every $j$ and every Boolean assignment $a\in \{0,1{\}}^j$, $P^{(j)}(a)=\text{the Boolean value of }{\mathrm{\Psi }}_j\text{ at }a,$ the truth values being embedded in $F$ as $0$ and $1$. In particular $P^{(0)}$, a constant, is the truth value of $\mathrm{\Phi }$.

Let $T\ge 1$ and $D\ge 1$ be integers and put $N:=\max \{2,12TD+1\}$. Then:

1. (Existence and size.) There is a prime $p$ with $N<p<2N$, and every such prime satisfies $p>12TD$ and $p<2N\le \max \{4,24TD+2\}$. Hence $p=O(TD)$ and $\lceil {\log }_{2}p\rceil =O(\log (TD))$.
2. (Deterministic search.) Call an integer $m$ with $N<m<2N$ admissible when no integer $d$ with $2\le d\le N$ divides $m$. The first admissible $m$ in the order $N+1,N+2,\dots ,2N-1$ is prime; a search that tests every candidate against every such $d$ performs at most $N^2$ trial divisions and $O(N^2{\log }^{2}N)$ bit operations, using no randomness and no primality test.
3. (Residue arithmetic.) In $F:=\mathbb{Z}\mathrm{/}p$ addition and multiplication make $F$ a field in which each class has exactly one representative in $\{0,1,\dots ,p-1\}$; representatives are stored in $\lceil {\log }_{2}p\rceil$ bits, adding or subtracting two representatives costs $O(\log p)$ bit operations and multiplying them costs $O({\log }^{2}p)$ bit operations. Consequently Horner evaluation of a polynomial of degree at most $D$ at a point of $F$ costs $O(D)$ operations in $F$, hence $O(D{\log }^{2}p)$ bit operations.
4. (Sampler with point mass at most $2\mathrm{/}p$.) Let $k:=2\lceil {\log }_{2}p\rceil$, let $U$ be uniform on $\{0,1{\}}^k$ and let $r$ be the integer $U\in \{0,\dots ,2^k-1\}$ reduced modulo $p$. Then $\mathrm{Pr}[r=a]\le 2\mathrm{/}p$ for each $a\in \{0,\dots ,p-1\}$, and $\mathrm{Pr}[r\in S]\le 2\mathrm{\mid }S\mathrm{\mid }\mathrm{/}p$ for every set $S$ of residues.

Let $\mathrm{\Phi }=Q_1{x}_1{Q}_2{x}_2\cdots Q_n{x}_n\psi$ be a closed prenex quantified Boolean formula (Quantified Boolean formulas and the language TQBF) whose quantifier-free matrix $\psi$ has $L$ syntax nodes, let $b:=P_{\psi }$ be the arithmetization of the matrix (Arithmetization of Boolean formulas), and put $D:=\max \{L,2\},T:=n(n+3)\mathrm{/}2.$ Let $N:=\max \{2,12TD+1\}$. If $T=0$, put $p:=3$; if $T\ge 1$, let $p$ be the first admissible integer of the search of A polynomial-size prime field meets the soundness budget. In either case $p$ is prime and $12TD<p<2N$; put $F:=\mathbb{Z}\mathrm{/}p$, a field with the residue operations (For every prime $p$, the two operations on $\mathbb{Z}\mathrm{/}p$ make it a field), and $k:=2\lceil {\log }_{2}p\rceil$. Let $N_1,N_2,\dots ,N_T$ be the operator list of the multilinearized ordered arithmetization of $\mathrm{\Phi }$ in application order, with $N_t$ acting in its active variable, and let $G_0:=b,G_t:=N_t(G_{t-1})(t=1,\dots ,T),$ so that $G_T$ is the arithmetized value of $\mathrm{\Phi }$ (Multilinearization in one variable, Field arithmetization of QBF quantifiers). Recall that each node is either a reduction $R_{X_i}$ or the quantifier operator $O_j$ of a block $j$, and that the operator list ends with $R_{X_1},O_1$. The operators make the individual degree of the node polynomials bounded by $D$ in the following sense: for every $t$ and every substitution of arbitrary field elements for all variables of $G_{t-1}$ other than its active variable, the resulting univariate polynomial over $F$ has degree at most $D$ (Multilinearization preserves Boolean values and bounds individual degree).

The Shamir protocol for $\mathrm{\Phi }$. The protocol runs for $T$ rounds. The verifier $V$ holds two pieces of state: a claim $c\in F$ and a current point $\sigma$, a partial function from $\{1,\dots ,n\}$ to $F$; initially $c:=1\text{and}\sigma :=\mathrm{\varnothing },$ the empty assignment. On an input that is not the encoding of a closed prenex quantified Boolean formula, $V$ rejects immediately; this convention makes $V$ total.

Round $t$. The rounds run for $t=T,T-1,\dots ,1$, so that the nodes are processed in the reverse of the application order; let $M:=N_t$ and let $x_i$ be the active variable of $M$.

1. Prover message. The prover sends a list $(a_0,a_1,\dots ,a_D)\in F^{D+1}$ of field elements, read as the coefficient vector of the univariate polynomial $s(X):=a_0+a_{1}X+\cdots +a_D{X}^D\mathrm{.}$ A message that is not such a list, or a list whose entries are not elements of $F$, is rejected.
2. Verifier check. If $M$ is the quantifier node $O_j$ of block $j$, then $V$ tests $c=s(0)s(1)\text{when }{Q}_j=\mathrm{\forall },c=s(0)+s(1)-s(0)s(1)\text{when }{Q}_j=\mathrm{\exists }\mathrm{.}$ If $M$ is a reduction $R_{X_i}$, then $V$ tests $c=(1-a)s(0)+as(1)\text{where }a:=\sigma (i),$ and if $\sigma (i)$ is undefined, $V$ rejects. If the applicable test fails, $V$ rejects and the exchange stops.
3. Challenge and update. If the test passes, $V$ reads the next $k$ bits of its random tape, forming the block $U_t\in \{0,1{\}}^k$, sets $r_t:=\text{(the integer denoted by }{U}_t\text{) mod }p,\sigma (i):=r_t,c:=s(r_t),$ and proceeds to the next round. Assigning $\sigma (i):=r_t$ replaces any value assigned to $x_i$ earlier in the exchange.

Terminal step. After round $t=1$, $V$ evaluates the matrix arithmetization $b$ at the point $\sigma$, using the arithmetic circuit of the formula $\psi$ and $O(L)$ operations in $F$ (Formula degree and point-evaluation cost), and $V\text{ accepts}⟺c=b(\sigma )\mathrm{.}$ This terminal evaluation is the only place in the protocol where the formula $\psi$ and the polynomial $b$ are used; every earlier test involves only the claim, the current point and the prover's last message.

The honest prover. In the round with node $M=N_t$ and active variable $x_i$, the honest prover $P_h$ sends the coefficient vector of $q_i(X):=G_{t-1}{\mid }_{x_j:=\sigma (j)\text{ for }j\mathrm{\ne }i,x_i:=X},$ the restriction of the current node polynomial $G_{t-1}$ to the current point, in the variable $X$ ranging over $F$. By the degree bound recalled above, $q_i$ has degree at most $D$, so this is a legal message; $P_h$'s choice depends only on the messages exchanged so far, which determine $\sigma$ and $c$.

• A run has at most $T$ prover messages and at most $T$ verifier challenges $r_T,r_{T-1},\dots ,r_1$; a failed check stops before its challenge is drawn, while a run that passes every check has all $T$ challenges and then the terminal step. The residue challenges are sent to the prover, so its strategy uses the public residue transcript. This residue protocol does not reveal the full random blocks $U_t$; the public-coin variant of TQBF has a polynomial-round interactive proof sends each whole block.
• The order of the rounds is the reverse of the operator list, which is what makes the checks local: each check relates the current claim to the received polynomial at the two Boolean points $0,1$, and, for a reduction, to the current value $a$ of the reduced variable. Processing $O_j$ before the reductions of block $j$ is what lets the reductions of a block see a value for $x_j$; the reductions of block $j$ then overwrite $x_j,x_{j-1},\dots ,x_1$, so at the end every variable carries the last challenge drawn for it.
• The verifier never evaluates the matrix before the terminal step, and the prover is never required to be efficient: only the number of rounds, the message lengths and the verifier's work are bounded, as required by Completeness and soundness of an interactive protocol.
• Both displayed forms of the existential test agree, since $s(0)+s(1)-s(0)s(1)=1-(1-s(0))(1-s(1))$ in every field; the second is the form used in Field arithmetization of QBF quantifiers for the operator $E_{X_j}$, and the first is the form used by Shen.
• For $n=0$ the operator list is empty, $T=0$, there are no messages, $\sigma$ is the empty assignment and the protocol reduces to the test $1=b$, where $b$ is the constant value of the arithmetization of a quantifier-free closed formula. For $n=1$, $T=2$ and the two rounds process first the quantifier node $O_1$ and then the reduction $R_{X_1}$; both cases are covered by the statements below.
• The prime $p$ is a function of the input alone: $D$ and $T$ depend only on the formula and the search of A polynomial-size prime field meets the soundness budget is deterministic, so the verifier makes no choice here. The only randomness in the protocol is at most $Tk$ bits of the random tape, read in blocks of $k$ bits only after passed checks; by the point-mass bound of that lemma every residue is sampled with probability at most $2\mathrm{/}p$, and the challenge is drawn after the prover's message has been fixed.
• The degree bound $D$ is the cap the verifier enforces on the received polynomial; the honest prover always meets it, and a prover that sends a longer or malformed list is rejected before any test is made. The factorization of the verifier's work into $O(TD)$ field operations for the rounds and $O(L)$ for the terminal evaluation, and the completeness and soundness of the protocol, are established in Honest prover maintains the field-value claim, Explicit communication, round, and evaluation bounds, Shamir protocol has perfect completeness, A false field claim becomes true in one round with bounded probability, Total TQBF soundness by the first repaired claim and Shamir verifier runs in polynomial time.