Cut-free proofs in ZFC

Question

If a statement $P$ has a ZFC proof of length $n$, must it also have a cut-free ZFC proof of length polynomial in $n$?

By a cut-free ZFC proof, I mean a proof in sequent calculus without cut rule of some sequent "finite set of ZFC axioms $\implies P$ ". This is arguably nonstandard and different from a cut-free proof in sequent calculus augmented with ZFC axioms in that we essentially allow a single cut on ZFC axioms as the final step.

Background: Every statement provable in predicate calculus is provable in sequent calculus without the cut rule, but sometimes with an iterated exponential increase in proof size. However, ZFC is not finitely axiomatizable, and for every finite fragment $T$ of ZFC and statement $P$, it proves "if $T$ proves $P$ , then $P$ " (this property also holds for many other theories such as $\mathrm{PA}$ and $\mathrm{Z}_2$, and one can also ask this question for those systems), and the question is whether this can be used to circumvent the slowdown from cut elimination by changing a proof of "finite fragment of ZFC $\implies P$ " into a cut-free proof of "a bigger finite fragment of ZFC $\implies P$ ".

An answer may give us some insight about to what extent polynomial length cut-free proofs are a well-behaved quantity, avoiding short proofs that every cut includes $2^k_n$ but working somewhat well otherwise.

Answer 1

Yes, one can eliminate cuts polynomially for proofs in ZFC, PA, and similar theories that have nontrivial axiom schemata allowing arbitrary formulas.

For PA, replace a cut $$\color{blue}{\dfrac{\Gamma\implies A,\Delta\qquad\Gamma,A\implies\Delta}{\Gamma\implies\Delta}}$$ with a cut-free subderivation $$\dfrac{\dfrac{\color{blue}{\Gamma,A\implies\Delta}}{\Gamma,\forall x\,A\implies\Delta}\qquad\dfrac{{\atop\displaystyle\strut\color{blue}{\Gamma\implies A,\Delta}}\qquad\dfrac{\dfrac{\dfrac{}{\Gamma,A\implies A,\Delta}}{\Gamma\implies A\to A,\Delta}}{\Gamma\implies\forall x\,(A\to A),\Delta}}{\Gamma\implies A\land\forall x\,(A\to A),\Delta}}{\dfrac{\Gamma,A\land\forall x\,(A\to A)\to\forall x\,A\implies\Delta}{\color{blue}{\Gamma,\color{red}{\forall\vec y\,(A\land\forall x\,(A\to A)\to\forall x\,A)}\implies\Delta}}},$$ where $\vec y$ is the list of free variables of $A$, and $x$ is a fresh variable. The extra red formula is now a (dummy) instance of an induction axiom, and we let it pass through to the final sequent.

For ZFC, we may abuse replacement or separation axioms in a similar way.