In this work, we establish separation theorems for several subsystems of the Ideal Proof System (IPS), an algebraic proof system introduced by Grochow and Pitassi (J. ACM, 2018). Separation theorems are well-studied in the context of classical complexity theory, Boolean circuit complexity, and algebraic complexity.
In an important work of Forbes, Shpilka, Tzameret, and Wigderson (Theory of Computing, 2021), two proof techniques were introduced to prove lower bounds for subsystems of the IPS, namely the \emph{functional method} and the \emph{multiples method}. We use these techniques and obtain the following results.
\begin{enumerate}
\item \textbf{Hierarchy theorem for constant-depth IPS.} Recently, Limaye, Srinivasan, and Tavenas (J. ACM 2025) proved a hierarchy theorem for constant-depth algebraic circuits. We adapt the result and prove a hierarchy theorem for constant-depth IPS. We show that there is an unsatisfiable multilinear instance refutable by a depth-$\Delta$ IPS such that any depth-($\Delta/10)$ IPS refutation for it must have superpolynomial size. This result is proved by building on the \emph{multiples method}.
\item \textbf{Separation theorems for multilinear IPS.} In an influential work, Raz (Theory of Computing, 2006) unconditionally separated two algebraic complexity classes, namely multilinear $NC^{1}$ from multilinear $NC^{2}$.
In this work, we prove a similar result for a well-studied fragment of multilinear IPS.
Specifically, we present an unsatisfiable instance such that its \emph{functional refutation}, i.e., the unique multilinear polynomial agreeing with the inverse of the polynomial over the Boolean cube, has a small multilinear-$NC^{2}$ circuit. However, any multilinear-$NC^{1}$ IPS refutation ($IPS_{LIN}$) for it must have superpolynomial size.
This result is proved by building on the \emph{functional method}.
\end{enumerate}
Given a polynomial $p(\mathbf{x})$, let $\textsf{Image}(p(\mathbf{x}))$ denote the set of values obtained when $p(\mathbf{x})$ is evaluated over the Boolean cube. Our crucial observation is that if the cardinality of this set is $\mathcal{O}(1)$, then the functional method and multiples method can be used to prove separation theorems for subsystems of the IPS. We obtain such polynomial instances by lifting the hard instances arising from algebraic circuit complexity with \emph{addressing gadgets}.
