Grochow and Pitassi (2018) introduced the algebraic proof system, the Ideal Proof System (IPS), which connects algebraic circuit complexity to propositional proof complexity. They showed that propositional proof systems such as Extended Frege (Frege) are equivalent to circuit IPS (formula IPS) if the correctness of PIT for circuits (formulas) can be proved in Extended Frege (Frege). Along the same lines, the work of Li, Tzameret, and Wang (2018) gives a quasi-polynomial (unconditional) equivalence between noncommutative formula IPS and Frege (over GF(2)) by proving the correctness of the noncommutative formula (ABP) PIT algorithm of Raz and Shpilka (2005) in Frege.

We extend this line of work beyond the fully noncommutative setting. We consider a partially commutative model in which the variables are partitioned into two sets: variables within each set are noncommuting while they commute across the sets. We show that the same quasi-polynomial equivalence with Frege continues to hold in this setting, even when both sets have unbounded size.

Enroute to the main result, we give a new deterministic polynomial time PIT algorithm for partially commutative formulas (ABPs) over such mixed variables and show that the correctness of the algorithm can be efficiently verified in Frege. To the best of our knowledge, this is the strongest known class of algebraic formulas for which Frege efficiently proves identity testing. Our approach uses tools from skew field theory (Cohn 1995), which may be of independent interest in algebraic proof complexity.