Field arithmetization of QBF quantifiers

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$.