Symmetric Proofs in the Ideal Proof System
Anuj Dawar, Erich Grädel, Leon Kullmann, Benedikt Pago
TL;DR
The paper formalizes symmetry in the Ideal Proof System (IPS) and shows that Gamma-symmetric IPS is complete, linking its expressive power to fixed-point logic with counting (FPC) and Choiceless Polynomial Time (CPT). It establishes that bounded-degree symmetric IPS corresponds to FPC, while CPT-level proofs may require unbounded degree, and it uses this framework to analyze graph isomorphism and standard tautologies. The authors derive concrete upper bounds for symmetric refutations on families such as the Cai-Fürer-Immerman (CFI) equations, the subset-sum problem, and the pigeonhole principle (PHP), revealing both separations and potential avenues for lower bounds via symmetry and functional techniques. Overall, the work lays foundational connections between symmetry in algebraic proofs, descriptive complexity, and graph isomorphism, with explicit constructions and bounds that motivate further investigation into lower bounds and circuit-theoretic tradeoffs in symmetric IPS.
Abstract
We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing lower bounds in other symmetric models of computation. We link the existence of symmetric IPS proofs to the expressive power of logics such as fixed-point logic with counting and Choiceless Polynomial Time, specifically regarding the graph isomorphism problem. We identify relationships and tradeoffs between the symmetry of proofs and other parameters of IPS proofs such as size, degree and linearity. We study these on a number of standard families of tautologies from proof complexity and finite model theory such as the pigeonhole principle, the subset sum problem and the Cai-Fürer-Immerman graphs, exhibiting non-trivial upper bounds on the size of symmetric IPS proofs.