Unprovability of circuit upper bounds in Cook's theory PV

TL;DR

This paper proves that for any polynomial degree, there exists a language in P that cannot be proven to have small circuit size within Cook's theory PV, highlighting fundamental limits of formal proof systems.

Contribution

It establishes the unprovability of certain circuit upper bounds in PV for all polynomial degrees, using a non-constructive argument.

Findings

Existence of languages in P unprovable to have small circuits in PV

Unconditional proof of unprovability results

Non-constructive nature of the argument

Abstract

We establish unconditionally that for every integer $k \geq 1$ there is a language $L \in \mbox{P}$ such that it is consistent with Cook's theory PV that $L \notin Size(n^k)$. Our argument is non-constructive and does not provide an explicit description of this language.