Polynomial Calculus sizes over the Boolean and Fourier bases are incomparable

Abstract

Proof theory is a foundational field of modern mathematics, dealing with study of the structure of mathematical proofs. It has a rich history starting with Aristotle’s intuitive notions of a rigorous proof, Euclid’s semi-formal system of logic underlying geometry, Frege’s notions of a formal system of logic with a complete set of inference rules, Hilbert’s attempted program to formalize the whole of mathematics, Gödel’s incompleteness results that put an end to this program, and finally Turing’s seminal paper building on Gödel’s work defining a formal notion of a computer and laying the foundations of most of theoretical computer science as we know it today.

In modern computer science, we are interested in computational aspects of these classical notions. Proof complexity is an area that studies lengths of proofs in formal systems of logic. In this talk, we will go over state of the art lower bounds on proofs in well studied systems of propositional logic proved over the past few decades. We will then touch upon our recent work that proves new connections between known proof systems, and new boundary-pushing lower bounds building on recent developments.

For every $n > 0$, we show the existence of a CNF tautology over $O(n^2)$ variables of width $O(\log n)$ such that it has a Polynomial Calculus Resolution refutation over ${0,1}$ variables of size $O(n^3polylog(n))$ but any Polynomial Calculus refutation over ${+1,-1}$ variables requires size $2^{\Omega(n)}$. This shows that Polynomial Calculus sizes over the ${0,1}$ and ${+1,-1}$ bases are incomparable (since Tseitin tautologies show a separation in the other direction) and answers an open problem posed by Sokolov [Sok20] and Razborov.

Venue: A3 117, Vindhya

Speaker Bio

Dr. Sasank Mouli completed his doctoral studies in Electrical Engineering at UC San Diego under the guidance of Prof Russell Impagliazzo. He completed his undergraduate studies in Electrical Engineering at Indian Institute of Technology, Kanpur. He is currently an assistant professor at Mahindra University, Hyderabad.