Finite Model Theory and Proof Complexity revisited: Distinguishing graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus

TL;DR

This paper establishes a connection between finite model theory and proof complexity by showing that graph distinguishability in Choiceless Polynomial Time implies similar distinguishability in the extended polynomial calculus, offering new insights into their computational limits.

Contribution

It demonstrates that graph distinguishability in CPT can be transferred to EPC, enabling lower bounds in proof complexity to inform about CPT's limitations.

Findings

CPT distinguishability implies EPC distinguishability with comparable resource bounds.

A super-polynomial EPC lower bound for a PTIME graph separates CPT from PTIME.

Provides a model theoretic proof for the separation of polynomial calculus variants.

Abstract

This paper extends prior work on the connections between logics from finite model theory and propositional/algebraic proof systems. We show that if all non-isomorphic graphs in a given graph class can be distinguished in the logic Choiceless Polynomial Time with counting (CPT), then they can also be distinguished in the bounded-degree extended polynomial calculus (EPC), and the refutations have roughly the same size as the resource consumption of the CPT-sentence. This allows to transfer lower bounds for EPC to CPT and thus constitutes a new potential approach towards better understanding the limits of CPT. A super-polynomial EPC lower bound for a PTIME-instance of the graph isomorphism problem would separate CPT from PTIME and thus solve a major open question in finite model theory. Further, using our result, we provide a model theoretic proof for the separation of bounded-degree polynomial calculus and bounded-degree extended polynomial calculus.