The IP = PSPACE Theorem: Examples and Counterexamples

By [A1] the matrix arithmetization is $X+(1-Y)-X(1-Y)$, which simplifies to $1-Y+XY=:b(X,Y)$. At the four Boolean points it takes the values $b(0,0)=1$, $b(0,1)=0$, $b(1,0)=1$, $b(1,1)=1$, matching $x\vee \mathrm{\neg }y$ in each case.

The reductions do not change $b$, because $b$ is multilinear: $b{\mathrm{\mid }}_{X=0}=1-Y$ and $b{\mathrm{\mid }}_{X=1}=1$ give $R_{X}b=(1-X)(1-Y)+X=1-Y+XY$, and $b{\mathrm{\mid }}_{Y=0}=1$ and $b{\mathrm{\mid }}_{Y=1}=X$ give $R_{Y}b=(1-Y)+YX=1-Y+XY$.

Applying the quantifier operations: $A_{Y}b=(b{\mathrm{\mid }}_{Y=0})(b{\mathrm{\mid }}_{Y=1})=1\cdot X=X$, then $R_{X}X=X$ since $X{\mathrm{\mid }}_{X=0}=0$ and $X{\mathrm{\mid }}_{X=1}=1$, and finally $E_{X}X=1-(1-0)\cdot (1-1)=1$. The constant so obtained is the truth value of $\mathrm{\Phi }$ by [A2] and [A5], and indeed $\mathrm{\Phi }$ is true.

Reading the stages backwards, the honest messages are the restrictions of $G_4=R_{X}X=X$, $G_3=X$, $G_2=R_Y{R}_{X}b=1-Y+XY$ at $x=3$, $G_1=1-Y+XY$ at $x=3$, and $G_0=b$ at $y=5$; that is, in the order of the rounds, $s_1(T)=T$, $s_2(T)=T$, $s_3(T)=1+2T$, $s_4(T)=1+2T$ and $s_5(T)=5T-4$.

The reverse protocol of [A4] therefore processes $E_X$ first, then $R_X$, then $A_Y$, $R_Y$ and $R_X$. Take the challenges in this order to be $2,3,4,5,6$, so that $\sigma (x)$ is set to $2$ and then to $3$ and finally to $6$, and $\sigma (y)$ is set to $4$ and then to $5$.

The verifier's tests pass with these messages: $E_X$ checks $1=0+1-0$; then $R_X$ with $a=2$ checks $2=(1-2)\cdot 0+2\cdot 1$; then $A_Y$ checks $3=1\cdot 3$, where $s_3(0)=1$ and $s_3(1)=3$; then $R_Y$ with $a=4$ checks $9=(1-4)\cdot 1+4\cdot 3$; and finally $R_X$ with $a=3$ checks $11=(1-3)\cdot (-4)+3\cdot 1$. So the claim sequence is $1\to 2\to 3\to 9\to 11\to 26$, where each new claim is obtained by evaluating the sent message at the new challenge.

The point left at the end is $\sigma =(6,5)$, and the terminal comparison gives $b(6,5)=1-5+30=26$, equal to the final claim $26$; the verifier therefore accepts this transcript. All products and sums above are computed in $\mathbb{Z}\mathrm{/}251$, where $(1-4)\cdot 1=-3\equiv 248$ and $248+12=260\equiv 9(\mathrm{m}\mathrm{o}\mathrm{d}251)$, so the intermediate values agree with the field arithmetic.

Substituting $x=0$ gives $P(0,z)=0+0+z=z$, and substituting $x=1$ gives $P(1,z)=z+2+z=2z+2$; both are computed in $\mathbb{Z}\mathrm{/}101$ by [A3].

By [A1] and step 1.1, $R_{x}P=(1-x)z+x(2z+2)=z-xz+2xz+2x=z+x(z+2)$, a polynomial of degree one in $x$ with $x$-coefficient $z+2$ and of degree one in $z$.

Evaluating the result of step 2.1 at the Boolean points: $R_{x}P(0,z)=z+0=z=P(0,z)$ and $R_{x}P(1,z)=z+z+2=2z+2=P(1,z)$, which is the agreement asserted in [A2].

The coefficient of $x$ in $z+x(z+2)$ is $z+2$, which vanishes exactly when $z=-2\equiv 99$ in $\mathbb{Z}\mathrm{/}101$ by [A3]; hence the $x$-degree is one for $z\mathrm{\ne }99$ and zero at $z=99$, and in either case it is at most one, as [A2] requires. The degree in $z$ is one, which does not exceed the $z$-degree one of $P$, and the degree in $x$ dropped from three to one while the values at the Boolean points were preserved.

For $\mathrm{\Phi }=\mathrm{\exists }x(x)$ we have $n=1$, $L=1$, hence $D=\max \{1,2\}=2$ and $T=1\cdot 4\mathrm{/}2=2$; then $N=\max \{2,12\cdot 2\cdot 2+1\}=49$, and the integers $50,51,52$ are inadmissible because $50=2\cdot 25$, $51=3\cdot 17$ and $52=2\cdot 26$ have divisors at most $49$, so the first admissible integer is $p=53$, which is prime by [A3].

The operator list of $\mathrm{\Phi }$ is $R_X,E_X$, so the stage polynomials are $G_0=b=X$, $G_1=R_{X}X=(1-X)\cdot 0+X\cdot 1=X$ and $G_2=E_{X}X=1-(1-0)(1-1)=1$; the last value is the truth value of the true formula $\mathrm{\Phi }$, and the protocol processes the nodes in the reverse order $E_X$, then $R_X$.

In the round for $E_X$ the claim is $c=1$ and the honest message is the restriction of $G_1$, namely $s(T)=T$. The existential test reads $s(0)+s(1)-s(0)s(1)=0+1-0=1=c$, so it passes; the verifier then draws its challenge $r$, sets $\sigma (x)=r$ and $c=s(r)=r$.

In the round for $R_X$ the current value of the reduced variable is $a=\sigma (x)=r$ and the honest message is the restriction of $G_0$, again $s(T)=T$. The reduction test reads $(1-a)s(0)+as(1)=(1-r)\cdot 0+r\cdot 1=r=c$, so it passes; the verifier draws a fresh challenge $r^{\mathrm{\prime }}$, sets $\sigma (x)=r^{\mathrm{\prime }}$ and $c=s(r^{\mathrm{\prime }})=r^{\mathrm{\prime }}$.

The terminal comparison is $c=b(\sigma )=r^{\mathrm{\prime }}$, which holds; so for every pair $(r,r^{\mathrm{\prime }})$ of challenges the honest prover is accepted, and since the challenges range over all of $\mathbb{Z}\mathrm{/}53\times \mathbb{Z}\mathrm{/}53$ the acceptance probability is $1$. This is an instance of the perfect completeness asserted in [A1] and [A2].

For contrast, the false instance ${\mathrm{\Phi }}^{\mathrm{\prime }}=\mathrm{\exists }x(x\wedge \mathrm{\neg }x)$ has matrix $X(1-X)$ with $L=4$ syntax nodes, so $D=4$, $T=2$, $N=97$ and the protocol prime is $101$; the soundness bound of [A2] evaluates there as $2TD\mathrm{/}p=16\mathrm{/}101<1\mathrm{/}3$. This numerical evaluation quotes the theorem's bound and does not reprove soundness.

Every ${\mathrm{\Phi }}_k$ is a closed prenex quantified Boolean formula: its prefix is the $k+1$ quantifiers $\mathrm{\exists }y,\mathrm{\forall }{x}_1,\dots ,\mathrm{\forall }{x}_k$ read left to right and its matrix is the variable leaf $(y)$, so it has $k+2$ syntax nodes. Fix the explicit binary-index encoding that writes each $x_i$ using its binary index and fixed punctuation. This is a fixed effective encoding allowed by [A3]; its length $m_k$ satisfies $m_k\ge k+1$ and $m_k=O(k\log (k+1))$. By [A2] the arithmetization of the matrix $(y)$ is $b=Y$. Each ${\mathrm{\Phi }}_k$ is also true, since the assignment $y=1$ makes the matrix $(y)$ true under every assignment to $x_1,\dots ,x_k$, so $\mathrm{\forall }{x}_1\cdots \mathrm{\forall }{x}_k(y)$ holds and then $\mathrm{\exists }y$ holds by [A3].

By the inner-to-outer rule of [A1] the naive sequence of ${\mathrm{\Phi }}_k$ applies the $k$ universal operators first, in the order $A_{x_k},A_{x_{k-1}},\dots ,A_{x_1}$, and applies the outer existential operator $E_y$ for the variable $y$ last, no reduction $R_{X_i}$ being inserted.

Base case of the induction on $j$: after zero universal operators the carried polynomial is $b=Y=Y^{2^0}$ by step 1.1.

Induction hypothesis: for some $0\le j<k$, after the first $j$ universal operators of the sequence of step 2.1 the carried polynomial is $Y^{2^j}$.

Under the hypothesis of step 3.1 the polynomial $Y^{2^j}$ involves none of the variables $X_1,\dots ,X_k$, so both specializations at the next variable $X_i$ coincide with $Y^{2^j}$, and the operator $A_{X_i}$ of [A1] returns the product $Y^{2^j}\cdot Y^{2^j}=Y^{2^{j+1}}$; hence the hypothesis holds again at $j+1$.

Steps 2.2, 3.1 and 4.1 give, after all $k$ universal operators, the carried polynomial $Y^{2^k}$, which is the polynomial immediately before the outer quantifier on $y$ is processed; the protocol's message at the node for $\mathrm{\exists }y$ is the restriction of this polynomial in the active variable $y$, namely the univariate polynomial with value $y^{2^k}$ and $2^k+1$ coefficients, so its degree in the active variable is exactly $2^k$. Since $m_k=O(k\log (k+1))$ for the fixed encoding of step 1.1, for every polynomial $q$ one has $2^k>q(m_k)$ for all sufficiently large $k$, so the degree bound asserted in [A4] fails for this allowed encoding: the exponential degree is witnessed on instances that are true, and the failure is therefore one of degree and not of Boolean semantics. No length bound is inferred from syntax-node count alone.