Unsat Taut

#  From Proof Complexity to Circuit Complexity
via Interactive Protocols

Noel Arteche111Lund University and University of Copenhagen,
<EMAIL_ADDRESS>Erfan Khaniki222Institute of Mathematics of the Czech
Academy of Sciences<EMAIL_ADDRESS>Ján Pich333University of Oxford,
<EMAIL_ADDRESS>Rahul Santhanam444University of Oxford,
<EMAIL_ADDRESS>
###### Abstract

Folklore in complexity theory suspects that circuit lower bounds against
$\NC^{1}$ or $\P/\poly$, currently out of reach, are a necessary step towards
proving strong proof complexity lower bounds for systems like Frege or
Extended Frege. Establishing such a connection formally, however, is already
daunting, as it would imply the breakthrough separation
$\NEXP\not\subseteq\P/\poly$, as recently observed by [PS23] [PS23].

We show such a connection conditionally for the Implicit Extended Frege proof
system ($\mathsf{iEF}$) introduced by [Kra04a] [Kra04a], capable of
formalizing most of contemporary complexity theory. In particular, we show
that if $\mathsf{iEF}$ proves efficiently the standard derandomization
assumption that a concrete Boolean function is hard on average for
subexponential-size circuits, then any superpolynomial lower bound on the
length of $\mathsf{iEF}$ proofs implies $\\#\P\not\subseteq\FP/\poly$ (which
would in turn imply, for example, $\PSPACE\not\subseteq\P/\poly$). Our proof
exploits the formalization inside $\mathsf{iEF}$ of the soundness of the sum-
check protocol of Lund, Fortnow, Karloff, and Nisan [LFKN92]. This has
consequences for the self-provability of circuit upper bounds in
$\mathsf{iEF}$. Interestingly, further improving our result seems to require
progress in constructing interactive proof systems with more efficient
provers.

##  1 Introduction

At a high level, both circuit complexity and proof complexity can be thought
of as an approach towards the $\P$ versus $\NP$ question. The circuit
complexity program, which met with considerable success in the 1980s, tries to
prove lower bounds against gradually larger circuit classes, hoping to
eventually show $\NP\not\subseteq\P/\poly$. Proof complexity, often identified
with the so-called Cook-Reckhow program, intends to show $\NP\neq\coNP$ and,
in turn, $\P\neq\NP$, by proving lower bounds against gradually more powerful
proof systems for propositional logic.

While both enterprises share the motivation to study _concrete_ computational
models of increasing power hoping to build up techniques to attack the long-
sought separations, there exist notable differences. Circuit complexity looks
at deterministic models of computation, while proof complexity deals with
proof systems, which are inherently non-deterministic. Furthermore, while
circuit complexity has a clear end-goal (lower bounds against general Boolean
circuits), it remains wide open whether the Cook-Reckhow program can be
realized even in principle. It is not known whether lower bounds against
strong systems like Extended Frege can imply lower bounds for every other
system and, as such, one could potentially keep proving lower bounds for ever-
stronger systems without ever settling whether $\NP\neq\coNP$.

The parallels between circuit complexity and proof complexity are made clearer
by Frege systems. For each circuit complexity class $\mathcal{C}$, one can
define the proof system $\mathcal{C}$-Frege, in which proof lines are
restricted to be circuits from $\mathcal{C}$. In this setting strong systems
like Frege and Extended Frege correspond to $\NC^{1}$-Frege and
$\P/\poly$-Frege, respectively, and thus the natural question arises: Can we
turn explicit lower bounds for $\mathcal{C}$ circuits into lower bounds for
$\mathcal{C}$-Frege systems, and vice versa?

While the question is essentially open, work on weaker systems and circuit
classes has proven successful. In one direction, the method of feasible
interpolation [Kra94, Raz95, Kra97] (see [Kra19, §17.9.1] for the history of
the method) has been extensively applied to obtain proof complexity lower
bounds. The framework of feasible interpolation formalizes the idea of
extracting computational content from proofs: given short proofs in a given
system, one can extract a small Boolean circuit in some restricted classes for
a related interpolant function. Contrapositively, circuit lower bounds for
such functions (often coming from unconditional results such as lower bounds
against monotone circuits [Raz85, And85, AB87]), turn into lower bounds for
proofs systems like Resolution [Kra97] or Cutting Planes [Pud97] (and
conditionally for other systems, such as Polynomial Calculus or Sum-of-Squares
[Hak20]). Unfortunately, this connection breaks for stronger proof systems:
already $\AC^{0}$-Frege and $\TC^{0}$-Frege are known to lack feasible
interpolation properties555Some of these systems are known to admit some form
of interpolation by stronger computational models, see e.g. [Pud20, DR23], but
we are interested in Boolean circuits. under standard cryptographic hardness
assumptions [KP98, BPR00, BDG+04], and this holds even if we allow feasible
interpolation by quantum circuits [ACG24].

In the other direction (circuit complexity from proof complexity), the theory
of lifting has unveiled deep connections between proofs, circuits and
communication protocols. Here, so-called query-to-communication lifting
theorems translate query complexity lower bounds (corresponding to weak
systems, like Resolution) into communication complexity lower bounds (e.g.
[RM97, LMM+22]). The latter provide restricted circuit lower bounds, such as
for monotone circuits (see e.g. [GGKS18, DMN+20, dRGR22] and references
therein). It is, however, not known how to derive non-monotone lower bounds
for unrestricted Boolean circuits by lifting proof complexity lower bounds.

For proper Frege systems, the connection has worked mostly in one direction,
from circuits to proofs, particularly at the level of techniques. The method
of random restrictions and the celebrated switching lemmas used to show
constant-depth circuit lower bounds in the 1980s [FSS84, Ajt83, Hås86] were
successfully transferred into $\AC^{0}$-Frege lower bounds shortly after
[Ajt94, BPU92, Kra94, BIK+92, PBI93, KPW95]. This suggests that understanding
what makes proof lines large might be necessary to understand why proofs are
long. Intriguingly, understanding the proof lines alone does not seem to
suffice: the $\AC^{0}[p]$ lower bounds of Razborov and Smolensky [Raz87,
Smo87] are yet to be successfuly translated to proof complexity, with lower
bounds for $\AC^{0}[2]$-Frege being one of the prominent frontier problems in
the field.

The current situation seems to suggest that in order to make progress towards
proof complexity lower bounds, it is _necessary_ (though seemingly not
sufficient) to first obtain strong enough circuit lower bounds. In particular,
under this folklore belief, circuit lower bounds against $\NC^{1}$ or
$\P/\poly$, currently out or reach, would be a necessary step towards proving
strong proof complexity lower bounds for systems like Frege or Extended Frege.
However, the suspicion remains unproven, and no generic way of deriving
explicit circuit lower bounds for unrestricted Boolean circuits from proof
complexity lower bounds for concrete propositional proof systems has been
discovered666We note that the issue lies in establishing such a connection for
a _concrete_ system. Of course, the statement there is a proof system $S$ such
that if $S$ is not polynomially bounded, then $\P\neq\NP$ is true: if
$\NP=\coNP$ the implication is vacuously true by taking a polynomially bounded
proof system; if $\NP\neq\coNP$, then $\P\neq\NP$ and thus the statement holds
for any proof system. It would be dramatically different to obtain such a
connection for a concrete system..

The first result giving such a connection under relatively conventional
assumptions which are presumably weaker than the conclusion of the connection
itself was presented recently by [PS23] [PS23]. Specifically, they showed that
any superpolynomial lower bound on the length of tautologies in the Extended
Frege system $\mathsf{EF}$ implies $\NP\not\subseteq\Ppoly$ assuming
hypotheses (I) and (II) below:

  * I.

(Provable circuit lower bound.) $\mathsf{EF}$ proves efficiently that a
concrete Boolean function in $\E$ is average-case hard for subexponential-size
circuits.

  * II.

(Provable reduction of OWFs to $\P\neq\NP$.) $\mathsf{EF}$ proves efficiently
that a polynomial-time function transforms circuits breaking one-way functions
into circuits solving $\SAT$.

We remark that Hypothesis I above presupposes $\E\not\subseteq\Ppoly$, which
is however believed to be a significantly weaker statement than
$\NP\not\subseteq\Ppoly$. Alternatively, Hypotheses I and II can be replaced
by a single assumption on the feasible provability of the existence of
anticheckers in $\mathsf{EF}$. These results remain valid even if we replace
$\mathsf{EF}$ by an essentially arbitrary proof system simulating
$\mathsf{EF}$.

Crucially, improving this and related results by dropping the hypotheses is
surprisingly daunting. As noted by [PS23] [PS23, Prop. 1], if one
unconditionally establishes the implication if $S$ is not polynomially
bounded, then $\NP\not\subseteq\Ppoly$ for a concrete proof system $S$, then
the breakthrough separation $\NP\not\subseteq\SIZE[n^{k}]$, for every fixed
$k$ (and $\NEXP\not\subseteq\P/\poly$) follows!

In short, proving a formal connection between proof complexity and circuit
complexity provably requires breakthrough circuit lower bounds! Despite this
setback, one can still hope to get evidence that points at these connections,
possibly by shifting some of the components of the ingredients. Namely, one
may try to (a) adopt some hardness assumption, in the style of [PS23]; (b)
conclude lower bounds weaker than $\NP\not\subseteq\Ppoly$; or (c) look at
non-Cook-Reckhow proof systems (such as MA proof systems or proof systems for
languages beyond $\coNP$).

In this style, [GP18] [GP18] showed that the Ideal Proof System
($\mathsf{IPS}$) does satisfy such a connection, to _algebraic_ circuit
complexity. Indeed, any superpolynomial lower bound in the length of proofs in
$\mathsf{IPS}_{\mathbb{F}}$ implies $\VP_{\mathbb{F}}\neq\VNP_{\mathbb{F}}$.
[GP18] avoid the Pich-Santhanam barrier by means of (b) and (c) above: first,
$\mathsf{IPS}$ is not known to be a Cook-Reckhow system, since proofs are
verified by randomized machines via polynomial identity testing; second, the
lower bounds are algebraic and not Boolean. Recall that while separating $\VP$
and $\VNP$ is a necessary step777Unconditionally over finite fields, and
assuming the Generalized Riemann Hypothesis for infinite fields. towards
$\NP\not\subseteq\Ppoly$ [Bür00], the converse is not known.

Another interesting connection has been established in the realm of quantified
Boolean formulas, where the connection can be made essentially optimal.
Beyersdorff, Bonacina, Chew, and Pich [BBCP20] showed that for every circuit
class $\mathcal{C}$, the quantified system
$\mathcal{C}\text{-Frege}+\forall\mathsf{red}$ is not polynomially bounded if
and only if either $\PSPACE\not\subseteq\mathcal{C}$ or $\mathcal{C}$-Frege is
not polynomially bounded. Here, $\mathcal{C}\text{-Frege}+\forall\mathsf{red}$
stands for the natural quantified system obtained by extending
$\mathcal{C}$-Frege with a universal reduction rule, which takes care of
universal quantifiers by instantiating concrete values for its variables in
the hope of refuting the formula. The reason this avoids the Pich-Santhanam
barrier is the disjunct in the conclusion. That is, in the context of QBF the
statement of the Pich-Santhanam barrier becomes that if
$\mathcal{C}\text{-Frege}+\forall\mathsf{red}$ is not polynomially bounded
implies $\PSPACE\not\subseteq\mathcal{C}$ or $\mathcal{C}$-Frege is not
polynomially bounded, then it already holds that either
$\NEXP\not\subseteq\Ppoly$ or $\mathcal{C}$-Frege is not polynomially bounded.
But this disjunction is no breakthrough, since it follows directly by a
diagonalization argument anyway: if a propositional system is polynomially
bounded, then $\NEXP$ is hard for $\Ppoly$ [Kra04].

### Contributions

We prove a new conditional connection between proof complexity and circuit
complexity, giving further evidence that strong proof complexity lower bounds
require circuit lower bounds. This constitutes the first example of a natural
proof system that is conditionally Cook-Reckhow and whose lower bounds imply
Boolean circuit lower bounds.

The system in question is (an extension of) the Implicit Extended Frege
($\mathsf{iEF}$) proof system of [Kra04a] [Kra04a], capable of formalizing
most of contemporary complexity theory. Our result can be informally stated as
follows, where $\mathsf{iEF}^{\operatorname{tt}(h)}$ stands for the proof
system extending $\mathsf{iEF}$ by axioms
$\operatorname*{tt}^{\operatorname{avg}}_{1/4}(h_{n},2^{n/4})$ claiming there
are no circuits of size $2^{n/4}$ approximating a concrete function $h$ on
more than a $(1/2+1/{2^{n/4}})$-fraction of the inputs.888For technical
reasons, we define $\mathsf{iEF}^{\operatorname{tt}(h)}$ using a system which
is polynomially equivalent to $\mathsf{iEF}$ instead of $\mathsf{iEF}$ itself,
see Definition 3.9.

######  Theorem 1.1 (Main theorem, informal).

Suppose there exists a Boolean function $h\in\NE\cap\coNE$ that is hard on
average for subexponential-size circuits. If the Cook-Reckhow proof system
$\mathsf{iEF}^{\operatorname{tt}(h)}$ is not polynomially bounded, then
$\\#\P\not\subseteq\FP/\poly$.

In the theorem above one could instead consider the system
$\mathsf{iEF}^{\operatorname{tt}(h)}$ for some unconditionally hard function
family $h$ that is guaranteed to exist. The only problem in this case is that
we might need non-uniform advice to verify the proofs, and so the system would
not be Cook-Reckhow (we refer to [CK07] [CK07] for a systematic treatment of
non-uniform proof systems).

One can interpret our theorem as improving on the connection of [PS23] [PS23]
from proof complexity to circuit complexity. Our result improves that of
[PS23] by completely dropping their second assumption (the one about
$\mathsf{EF}$ proving the existence of one-way functions under $\P\neq\NP$).
The price to pay for these changes is two-fold:

  1. 1.

we need to replace $\mathsf{EF}$ by the seemingly stronger Implicit Extended
Frege system ($\mathsf{iEF}$). Informally, $\mathsf{iEF}$ extends
$\mathsf{EF}$ with an extra rule allowing us to derive a formula $\varphi$
after we have derived that a truth table of a given circuit encodes an
$\mathsf{EF}$-proof of $\varphi$. Such a circuit is called an _implicit_
proof;

  2. 2.

we can conclude only $\\#\P\not\subseteq\FP/\poly$ from $\mathsf{iEF}$ lower
bounds, instead of $\NP\not\subseteq\Ppoly$.

One may also compare our result to that of [GP18] [GP18], who showed
$\VP\neq\VNP$ (and hence hardness of computing the permanent) would follow
from $\mathsf{IPS}$ lower bounds. Like our result, the $\mathsf{IPS}$ proof
system is only conditionally Cook-Reckhow. Indeed, $\mathsf{IPS}$ is a Merlin-
Arthur proof system which can be derandomized999In fact, derandomizing
$\mathsf{IPS}$ at all by simulating it by a Cook-Reckhow system implies a non-
trivial derandomization of polynomial identity testing to $\NP$ [Gro23]; this,
in turn, implies some circuit lower bounds, as shown by Kabanets and
Impagliazzo [KI04]. under standard assumptions, like $\E$ being hard to
approximate by subexponential-size circuits. Our result is in some sense
stronger in that the lower bounds obtained are Boolean rather than algebraic.
However, we seem to be getting to lower bounds for the same problem as Grochow
and Pitassi, since computing the permanent is both $\VNP$-complete and
$\\#\P$-complete.

We note that the requirement that $h\in\NE\cap\coNE$ is not strictly needed
and, in fact, one can phrase the result in a more general style (as we do in
the technical part) in which the connection holds for any extension of
$\mathsf{iEF}$ by truth table formulas for any hard function. Observe,
however, that $\mathsf{iEF}$ is a very strong proof system, conjectured to be
strictly stronger than the standard $\mathsf{EF}$ and capable of formalizing
most of computational complexity theory, with its bounded arithmetic
counterpart being the theory $\mathsf{V^{1}_{2}}$ (or
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$, in the first-order setting), and
so it is plausible that $\mathsf{iEF}$ already proves such a circuit lower
bound. Indeed, the existing formalizations of complexity-theoretic statements
support the assumption that $\mathsf{iEF}$ is able to prove efficiently
practically everything we can prove in complexity theory today (or, more
precisely, every $\coNP$ statement of that kind). For example, already
$\mathsf{EF}$ can prove efficiently the PCP theorem [Pic15], $\AC^{0}$,
$\AC^{0}[2]$ and monotone circuit lower bounds [Raz95a, MP20], or the hardness
amplification producing average-case hard functions in $\E$ from worst-case
hard functions in $\E$ [Jeř05]. Furthermore, $\mathsf{iEF}$ proves efficiently
the correctness of Zhuk’s algorithm from a CSP dichotomy [Gay22, Gay24]. Hence
it is plausible to imagine that if circuit lower bounds are at all provable,
they may well be provable already in $\mathsf{iEF}$. If that turned out to be
the case, then the concrete proof system in our main theorem becomes
$\mathsf{iEF}$ itself.

######  Corollary 1.2.

(Main theorem, restated) Assume that $\mathsf{iEF}$ proves efficiently
$\operatorname*{tt}^{\operatorname{avg}}_{1/4}(h_{n},2^{n/4})$ for some
function family $h$ and each sufficiently big $n$. Then, if $\mathsf{iEF}$ is
not polynomially bounded, $\\#\P\not\subseteq\FP/\poly$.

Let us note that one cannot make big improvements to this result without
hitting the Pich-Santhanam barrier that implies $\NEXP\not\subseteq\Ppoly$
unconditionally: if we managed to prove Theorem 1.1 for a Cook-Reckhow proof
system, then $\NEXP\not\subseteq\Ppoly$ would follow unconditionally. On the
other hand, if our final goal is to prove $\FP\neq\\#\P$, then the assumption
of Theorem 1.1 is given to us for free even for some hard $h\in\E$, as
otherwise, if $\E$ can be computed by subexponential-size circuits, it is not
hard to show that $\P\neq\NP$ [Kra04].

### Consequences for self-provability of circuit upper bounds

Our result has consequences for the self-provability of circuit upper bounds.
Suppose that $\\#\P\subseteq\FP/\poly$. Then, there is a sequence of
polynomial-size circuits $\\{C_{n}\\}_{n\in\mathbb{N}}$ that on input a
formula $\varphi$ of size $n$, outputs a satisfying assignment if one exists.
This means that the propositional formula
$\SAT_{n}(\varphi,\alpha)\rightarrow\SAT_{n}(\varphi,C_{n}(\varphi))$ claiming
the correctness of $C_{n}$ as a SAT solver is tautological (where $\SAT_{n}$
is the satisfiability predicate, taking a formula $\varphi$ and an assignment
$\alpha$ and evaluating the formula). But by Theorem 1.1,
$\mathsf{iEF}^{\operatorname{tt}}$ is now polynomially bounded, and so the
proof system is able to efficiently argue for the correctness of the circuits.
Namely, the mere validity of the upper bound $\\#\P\subseteq\FP/\poly$ would
imply the efficient propositional provability of $\SAT\in\Ppoly$.

### Outline of the proof

Our main result follows from a derandomization of the known fact that
$\coNP\not\subseteq\MA$ implies $\\#\P\not\subseteq\FP/\poly$ (see, for
example, [AB09, Thm. 8.22]), together with a formalization of the underlying
MA system in a suitable theory of bounded arithmetic. The implication holds,
actually, for the MA system given by the sum-check protocol of Lund, Fortnow,
Karloff, and Nisan [LFKN92] in which proofs consist of circuit simulating the
moves of the Prover in the protocol, so that given such a circuit, the
Verifier can simulate the entire protocol on their own with the aid of
randomness. If $\\#\P\subseteq\FP/\poly$, then the $\\#\P$-powerful Prover in
the sum-check protocol can be replaced by a polynomial-size circuit and thus
the system is a polynomially bounded Merlin-Arthur system. Clearly, lower
bounds on the length of proofs in this system are exactly circuit lower bounds
against $\\#\P$.

Since $\MA$ can be derandomized under standard hardness assumptions, assuming,
for example, that $\E$ is hard for subexponential-size circuits, the proof
system $R$ based on the sum-check protocol above becomes a Cook-Reckhow system
such that if $R$ is not polynomially bounded, then
$\\#\P\not\subseteq\FP/\poly$. This is almost our goal. Our task now is to
replace this system by a different more standard Cook-Reckhow system $S$. This
can be achieved by proving efficiently the reflection principle of the system
$R$ in $S$, which essentially amounts to proving the soundness of the sum-
check protocol in $S$. Here, we employ a recent work of [Kha23a] [Kha23a], in
which the soundness of the sum-check protocol was formalized in
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$.

In order to translate the formalization inside
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ into propositional logic, we need
to express the soundness of the sum-check protocol by propositional formulas.
This is achieved using the machinery of approximate counting of [Jeř07]
[Jeř07], which exploits Nisan-Wigderson generators based on a hard Boolean
function.

### Open problems

Improving our result seems to require significant conceptual work. Of course,
simultaneously dropping the circuit lower bound assumption as well as getting
the stronger separation $\NP\not\subseteq\Ppoly$ would already imply
$\NEXP\not\subseteq\Ppoly$, but one may hope to improve the existing
connection by improving on one of the two fronts only. Interestingly, this
seems to require progress in some of the central open questions in the theory
of interactive proof systems or in hardness magnification.

##### The power of the prover.

Is it possible to strengthen the conclusion of the main theorem all the way
down to $\NP\not\subseteq\Ppoly$? This would follow, for example, if we
managed to design an interactive protocol for $\TAUT$ with a prover solving
only $\NP$ problems and prove its correctness in $\mathsf{iEF}$ (unlike the
current situation, where the prover is required to compute a $\\#\P$-complete
function). The general question of constructing a protocol for a language $L$
where the prover’s power is limited to $\P^{L}$ is a well-known open problem
in the theory of interactive proof systems (see, for example, [AB09, §8.4]).

Note, of course, that the existence of such a protocol does not suffice, since
its soundness must be provable inside $\mathsf{iEF}$. In fact, the reason why
we require $\mathsf{iEF}$ (or $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$) to
carry out the formalization of the existing sum-check protocol is that one
cannot feasibly talk about $\\#\SAT$ directly in $\mathsf{EF}$ or
$\mathsf{S^{1}_{2}}$ (unless $\FP=\\#\P$).

##### Hardness magnification.

Is it possible to replace $\mathsf{iEF}$ in the main theorem by Gentzen’s
system $\mathsf{G}$, or even by Extended Frege? One option would be to carry
out the existing formalization inside $\mathsf{EF}$, as mentioned above. The
caveat would be, however, that we would then have to make the assumption on
truth table tautologies for $\mathsf{EF}$. Whether $\mathsf{EF}$ can prove
general circuit lower bounds at all seems much less believable than for
$\mathsf{iEF}$, and so the plausibility of our hypotheses seems affected.

Instead, one may choose to keep everything in $\mathsf{iEF}$ and obtain the
connection indirectly for $\mathsf{EF}$ via hardness magnification. Is there a
natural class of formulas over which $\mathsf{EF}$ simulates $\mathsf{iEF}$
(and which are believably hard for $\mathsf{EF}$)? If so, assuming hardness of
these formulas for $\mathsf{EF}$ would imply $\mathsf{iEF}$ lower bounds. By
our main theorem, $\\#\P\not\subseteq\Ppoly$ would follow. To the best of our
knowledge, no such type of hardness magnification is known for strong proof
systems.

##  2 Preliminaries

We assume familiarity with the central concepts of computational complexity
theory, propositional proof complexity and mathematical logic. Some of our
work relies on formalizing standard text-book material on computational
complexity in different theories of arithmetic; for the standard proofs of
these results, we refer the reader to [AB09] [AB09]. Below we review the
central concepts of proof complexity and bounded theories of arithmetic and
fix some notation.

###  2.1 Proof complexity

Following Cook and Reckhow [CR79], a _propositional proof system_ $S$ for the
language $\TAUT$ of propositional tautologies is a polynomial-time surjective
function $S:\\{0,1\\}^{*}\to\TAUT$. We shall think of $S$ as a proof checker
taking as input a proof $\pi\in\\{0,1\\}^{*}$ and outputting $S(\pi)=\varphi$,
the theorem that $\pi$ proves. Note that soundness follows from the fact that
the range is exactly $\TAUT$, and implicational completeness is guaranteed by
the fact that $S$ is surjective. We sometimes drop the term _proof_ in _proof
system_ and use the term _system_ alone to refer to a function $S$ that is not
guaranteed to be a Cook-Reckhow proof system (perhaps because it is unsound,
or not deterministically computable).

We denote by $\mathsf{size}_{S}(\varphi)$ the _size_ of the smallest $S$-proof
of $\varphi$ plus the size of $\varphi$. A proof system $S$ is _polynomially-
bounded_ if for every $\varphi\in\TAUT$,
$\mathsf{size}_{S}(\varphi)\leq|\varphi|^{O(1)}$. We say that a proof system
$S$ _polynomially simulates_ a system $Q$, written $S\geq Q$, if for every
$\varphi\in\TAUT$,
$\mathsf{size}_{S}(\varphi)\leq\mathsf{size}_{Q}(\varphi)^{O(1)}$. Note that
the notion of size and the definition of simulation do not exploit the
soundness requirement of Cook-Reckhow systems. These notions are well-defined
for any function whose range contains $\TAUT$. In particular, an unsound
system can be polynomially bounded and simulate every other system. In some
cases simulations hold only for some set $T$ of tautologies, such as the set
of tautologies written as 3DNFs, and not for all formulas, and then we say
that $S$ polynomially simulates $Q$ over $T$. Given a family
$\\{\varphi_{n}\\}_{n\in\mathbb{N}}$ of propositional tautologies, we write
$S\vdash\varphi_{n}$ whenever
$\mathsf{size}_{S}(\varphi_{n})\leq|\varphi_{n}|^{O(1)}$.

####  2.1.1 Frege systems

Proof complexity studies a wide variety of proof systems. The most important
ones for us are _Frege systems_. A Frege system is a finite set of axiom
schemas and inference rules that are sound and implicationally complete for
the language of propositional tautologies built from the Boolean connectives
negation ($\neg$), conjunction ($\land$), and disjunction ($\lor$). A Frege
proof is a sequence of formulas where each formula is obtained by either
substitution of an axiom schema or by application of an inference rule on
previously derived formulas. The specific choice of rules does not affect
proof size up to polynomial factors, as long as there are only finitely many
rules and these are sound and implicationally complete. Indeed, Frege systems
polynomially simulate each other [Kra19, Thm. 4.4.13]. Alternatively, one may
choose to think of Frege systems as some variant of Natural Deduction or the
Sequent Calculus for classical propositional logic.

Particularly important for us is the Extended Frege ($\mathsf{EF}$) system, in
which proof lines can be Boolean circuits and not just formulas, which would
allow in principle for more succinct proofs. We shall often consider
extensions of Extended Frege by sets of additional axioms. For a set
$A\subseteq\TAUT$ of tautologies recognizable in polynomial time, the system
$\mathsf{EF}+A$ refers to Extended Frege extended with substitution instances
of any formula in $A$. Note that if $A$ were to contain contingent formulas,
then $\mathsf{EF}+A$ would not be sound; in particular, it would not be a
Cook-Reckhow system, though it would be polynomially bounded.

A useful property of $\mathsf{EF}$ is the fact that, for every propositional
system $S$, $\mathsf{EF}+\operatorname{Ref}_{S}\geq S$ [KP90]. Here
$\operatorname{Ref}_{S}$ is the sequence of tautologies encoding the
_reflection principle for $S$_, which states that $S$ is sound. Namely,
$\operatorname{Ref}_{S}\coloneqq\\{\operatorname{Ref}_{S,n,m}\\}_{n,m\in\mathbb{N}}$
where
$\operatorname{Ref}_{S,{n,m}}\coloneqq\operatorname{Prf}_{S,n,m}(\pi,\varphi)\to\operatorname{Sat}_{n,m}(\varphi,\alpha)$,
and $\varphi$ is a formula of size $n$, $\pi$ is a purported $S$-proof of size
$m$ and $\alpha$ is an assignment to the variables in $\varphi$, which are all
encoded by free variables. The formula $\operatorname{Prf}_{S,n,m}$ encodes
that $\pi$ is a correct $S$-proof of $\varphi$, and
$\operatorname{Sat}_{n,m}(\varphi,\alpha)$ encodes the standard satisfaction
relation for propositional formulas. Alternatively, one may exploit the same
relation with respect to the _consistency_ of $S$,
$\operatorname{Con}_{S}\coloneqq\\{\operatorname{Con}_{S,m}\\}_{m\in\mathbb{N}}$,
where
$\operatorname{Con}_{S,m}\coloneqq\neg\operatorname{Prf}_{S,1,m}(\pi,\bot)$
and $\pi$ encodes a purported proof of size $m$.

####  2.1.2 Quantified propositional systems

The focus of proof complexity is on proof systems for propositional
tautologies, but it is often convenient to operate on systems capable of
reasoning with _quantified_ Boolean formulas, where the quantification ranges
over $\\{0,1\\}$. We denote by $\Sigma^{q}_{i}$ (respectively, $\Pi^{q}_{i}$)
the class of quantified Boolean formulas with $i$ alternations between
existential and universal quantifiers, starting with an existential
(respectively, universal) one. In this context, the true formulas in
$\Pi_{1}^{q}$ correspond to the usual propositional tautologies.

We are particularly interested in Gentzen’s Sequent Calculus for quantified
propositional logic. The system extends the usual propositional Sequent
Calculus by four new rules to handle quantifiers (see [Kra19, Def. 4.1.2] for
a formal definition of the rules). We denote this system by $\mathsf{G}$, and
by $\mathsf{G^{*}}$ its tree-like counterpart. The system $\mathsf{G}_{i}$,
for $i\in\mathbb{N}$, corresponds to $\mathsf{G}$ where the quantified
formulas appearing in the sequents can only be in the class
$\Sigma_{i}^{q}\cup\Pi_{i}^{q}$. The tree-like counterpart of $\mathsf{G}_{i}$
is naturally denoted $\mathsf{G}^{*}_{i}$. It is useful to know that
$\mathsf{EF}$ and $\mathsf{G^{*}_{1}}$ are polynomially equivalent with
respect to $\Pi^{q}_{1}$ formulas [Kra19, Thm. 4.1.3].

####  2.1.3 Implicit proof systems

_Implicit proof systems_ constitute a systematic way of obtaining, for every
proof system $S$, a potentially stronger system $S^{\prime}$, and were
introduced by [Kra04a] [Kra04a]. The essential idea is to encode a given proof
in the system $S$ as a multi-output Boolean circuit taking as input a number
$i$ in binary and outputting the $i$-th step of the proof. More formally,
given propositional proof systems $S$ and $Q$, a proof of a tautology
$\varphi$ in the _implicit system_ $[S,Q]$ is a pair $(\pi,C)$ consisting of a
proof and a circuit, such that the truth table of $C$ encodes a valid
$Q$-proof of $\varphi$ (the _implicit_ proof), while $\pi$ is an _explicit_
$S$-proof of the formula $\operatorname{Correct}_{Q}(\varphi,C)$, which is the
formula stating that the truth table of $C$ is a correct $Q$-proof of
$\varphi$. If $S$ and $Q$ are Cook-Reckhow proof systems, then so is $[S,Q]$.

For a system $S$, the implicit system $[S,S]$ is denoted by $\mathsf{i}S$. In
particular, we shall work with the _Implicit Extended Frege_ proof system,
$\mathsf{iEF}\coloneqq[\mathsf{EF},\mathsf{EF}]$. The system $\mathsf{iEF}$ is
particularly strong, and it can in fact simulate all of $\mathsf{G}$ with
respect to propositional tautologies [Kra04a, Cor. 2.4].

###  2.2 Bounded arithmetic

Our proofs extensively exploit the connections between propositional proof
complexity and theories of bounded arithmetic. Below we cover the essential
preliminaries needed in our formalizations, which should be accessible to any
reader with basic knowledge of first-order logic.

####  2.2.1 The theories $\mathsf{S^{1}_{2}}$ and
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$

Theories of bounded arithmetic capture various levels of feasible reasoning
and act as a uniform counterpart of propositional systems. Intuitively,
feasibility is achieved by restricting the complexity of formulas over which
one can apply general reasoning schemes like induction.

The central theory for us is Buss’s $\mathsf{S^{1}_{2}}$, which we think of as
corresponding to polynomial-time reasoning. In this context, we work over the
first-order language of bounded arithmetic,
$\mathcal{L}_{\text{BA}}\coloneqq\\{0,S,+,\cdot,<,|x|,\lfloor
x/2\rfloor,x\\#y\\}$, which extends the language of Peano Arithmetic by the
symbols $|x|$, $\lfloor x/2\rfloor$ and $x\\#y$. The standard interpretation
of $\lfloor x/2\rfloor$ is clear. The notation $|x|$ denotes the length of the
binary encoding of the number $x$, $\lceil\log(x+1)\rceil$, while the _smash
symbol_ $x\\#y$ stands for $2^{|x|\cdot|y|}$.

The definition of _bounded formulas_ , is analogous to the bounded
quantification one encounters in the Polynomial Hierarchy. For a quantifier
$Q\in\\{\exists,\forall\\}$ and a term $t$ in the language of bounded
arithmetic, a formula of the form $Qx<t.\varphi(x)$ stands for either $\forall
x.(x<t\to\varphi(x))$ or $\exists x.(x<t\land\varphi(x))$. These are called
_bounded quantifiers_. Whenever the bounded quantifier is of the form $Q<|s|$
for some term $s$, we talk about _sharply bounded quantifiers_. The hierarchy
of _bounded formulas_ consists of the classes $\Sigma_{n}^{b}$ and
$\Pi_{n}^{b}$, for $n\geq 1$, which are defined by counting the alternations
of bounded quantifiers ignoring the sharply bounded ones, starting with an
existential (respectively, universal) one. The class $\Delta_{n}^{b}$ consists
of all formulas that admit an equivalent definition in both $\Sigma_{n}^{b}$
and $\Pi_{n}^{b}$. In particular, the class $\Delta_{0}^{b}$ stands for all
formulas with sharply bounded quantifiers only.

The theory $\mathsf{S^{1}_{2}}$ of [Bus85] [Bus85] extends Robinson’s
arithmetic $\mathsf{Q}$ by some basic axioms for the new function symbols and
the polynomial induction scheme (PInd) for $\Sigma_{1}^{b}$-formulas: for
every $\varphi\in\Sigma_{1}^{b}$, the theory contains the axiom

$\varphi(0)\land\forall x(\varphi(\lfloor x/2\rfloor)\to\varphi(x))\to\forall
x\varphi(x).$ (PInd)

An alternative system intended to capture polynomial-time reasoning is Cook’s
equational theory $\mathsf{PV}$ [Coo75]. In the formalism of $\mathsf{PV}$ one
has some basic function symbols and introduces new ones recursively by
composition and limited recursion on notation, in the style of Cobham’s
functional definition of $\FP$ [Cob64]. In this way, the function symbols
obtained in $\mathsf{PV}$ are precisely those of all polynomial-time functions
over the naturals. The first-order version of $\mathsf{PV}$ is
$\mathsf{PV_{1}}$ [KPT91, Bus95, Coo96]. Without loss of generality, we shall
work in the theory $\mathsf{S^{1}_{2}}(\mathsf{PV})$, which is the theory
$\mathsf{S^{1}_{2}}$ in the language of bounded arithmetic extended by all
$\mathsf{PV}$ function symbols, meaning that we have a fresh symbol for each
function in $\FP$, and induction is now available for all
$\Sigma_{1}^{b}(\mathsf{PV})$ formulas. We abuse notation and refer to this
directly as $\mathsf{S^{1}_{2}}$.

While $\mathsf{S^{1}_{2}}$ is able to formalize a significant amount of
complexity theory and some mathematics, it suffers from the drawback of being
unable to even state the existence of exponentially large objects. For certain
more elaborate arguments we shall work instead inside
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$, which patches this issue. We
follow here the definition of [Kra04a] [Kra04a, Cor. 2.2]: we write
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}\vdash\forall x\varphi(x)$ for some
arithmetic formula $\varphi$ if there exists a term $t$ such that

$\mathsf{S^{1}_{2}}\vdash\forall x\forall y(t(x)\leq|y|\to\varphi(x)).$

The definition is somewhat indirect and may be hard to grasp at first glance.
Intuitively, it allows one to derive properties about $x$ under the assumption
that $y=2^{x}$ exists.

The theory $\mathsf{S^{1}_{2}}$ corresponds to polynomial-time computations in
the sense that the provably total relations in $\mathsf{S^{1}_{2}}$ are
precisely the polynomial-time-computable ones. The same relation holds for
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ and the complexity class $\EXP$.

####  2.2.2 Approximate counting

Many of the formalizations carried out in bounded arithmetic require the
ability to count. In some cases, small sets can be counted _exactly_ , but one
often requires more sophisticated machinery for _approximate counting_ ,
needed to formalize many probabilistic arguments.

For $a\in\mathbb{N}$, a _bounded definable set_ is a set of naturals
$X=\\{x<a\mid\varphi(x)\\}\subseteq[0,a)$, where
$\varphi\in\Sigma_{\infty}^{b}$ is some arithmetic formula. For $X\subseteq a$
and $Y\subseteq b$, we define $X\times Y\coloneqq\\{bx+y\mid x\in X,y\in
Y\\}\subseteq ab$ and $X\mathbin{\dot{\cup}}Y\coloneqq X\cup\\{y+a\mid y\in
Y\\}\subseteq a+b$. Rational numbers are assumed to be represented by pairs of
integers in the natural way. We also use the unfortunate but standard _Log-
notation_ widespread in bounded arithmetic, by which $n\in\operatorname{Log}$
stands for the formula $\exists x(n=|x|)$ and $n\in\operatorname{LogLog}$
stands for $\exists x(n=||x||)$.

Intuitively, from the point of view of the theory, numbers in
$\operatorname{Log}$ are small numbers. For a circuit $C:2^{k}\to 2$, where we
adopt the set-theoretic custom of identifying $\\{0,1\\}$ with the number $2$,
we can consider the bounded definable set $X_{C}\coloneqq\\{x<2^{k}\mid
C(x)=1\\}$, and ask about the task of counting the size of $X_{C}$.

There exists a $\mathsf{PV}$-function
$\operatorname{Count}(C,y)=|X_{C}\cap|y||$. This means that if
$2^{k}\in\operatorname{Log}$, then one can do _exact counting_ of $|X_{C}|$
efficiently. We use the notation $\Pr_{x<|y|}[C(x)=1]\leq z/w$ for the
$\mathsf{PV}$-relation $w\cdot\operatorname{Count}(C,y)\leq|y|\cdot z$.

If $2^{k}\not\in\operatorname{Log}$, exact counting becomes problematic. To
avoid this, [Jeř07] [Jeř05, Jeř07] systematically developed the theory
$\mathsf{APC_{1}}$ capturing probabilistic polynomial-time reasoning by means
of approximate counting. The theory $\mathsf{APC_{1}}$ is defined as
$\mathsf{PV_{1}}+\operatorname{dWPHP}(\mathsf{PV})$ where
$\operatorname{dWPHP}(\mathsf{PV})$ stands for the _dual (surjective)
pigeonhole principle_ for all $\mathsf{PV}$-functions. That is, the set of all
formulas

$x>0\rightarrow\exists v<x(|y|+1).\forall u<x|y|.\ f(u)\neq v,$
($\operatorname{dWPHP}$)

where $f$ is a $\mathsf{PV}$-function which might involve other parameters not
explicitly shown.

We write $C:X\twoheadrightarrow Y$ if $C$ is a surjective mapping from $X$ to
$Y$. Let $X,Y\subseteq 2^{n}$ be definable sets, and $\epsilon\leq 1$. The
size of $X$ is _approximately less than the size of $Y$ with error
$\epsilon$_, written as $X\preceq_{\epsilon}Y$, if there exists a circuit $C$,
and $v\neq 0$ such that

$C:v\times(Y\mathbin{\dot{\cup}}\epsilon 2^{n})\twoheadrightarrow v\times X.$

In this context, the notation $X\approx_{\epsilon}Y$ stands for
$X\preceq_{\epsilon}Y$ and $Y\preceq_{\epsilon}X$. As with exact counting, the
notation $\Pr_{x<y}[C(x)=1]\circ_{\epsilon}z/w$ stands for $w\cdot(X_{C}\cap
y)\circ_{\epsilon}y\cdot z$, for $\circ\in\\{\preceq,\approx\\}$. Since a
number $s$ is identified with the interval $[0,s)$, $X\preceq_{\epsilon}s$
means that the size of $X$ is at most $s$ with error $\epsilon$.

The definition of $X\preceq_{\epsilon}Y$ is an unbounded $\exists\Pi^{b}_{2}$
formula even if $X$ and $Y$ are defined by circuits, so it cannot be used
freely in bounded induction. This problem can be solved by working in ${\sf
sHARD}^{\text{A}}$, defined as the relativized theory
$\mathsf{S^{1}_{2}}(\alpha)$ extended with axioms postulating that $\alpha(x)$
is a truth table of a function on $||x||$ variables hard on average for
circuits of size $2^{||x||/4}$. In ${\sf sHARD}^{\text{A}}$ there is a
$\mathsf{PV}(\alpha)$ function $\operatorname{Size}$ approximating the size of
any set $X\subseteq 2^{n}$ defined by a circuit $C$ so that
$X\approx_{\epsilon}\operatorname{Size}(\alpha,C,2^{n},2^{\epsilon^{-1}})$ for
$\epsilon^{-1}\in\operatorname{Log}$ (by combination of [Jeř07, Lemma 2.14]
and [Jeř04, Cor. 3.6]).

The following key definition allows us to express that a function is indeed
hard on average.

######  Definition 2.1 ($\operatorname{Hard}^{\text{A}}_{\epsilon}(f)$, in
$\mathsf{PV_{1}}$ [Jeř07]).

Let $f:2^{k}\rightarrow 2$ be a truth table of a Boolean function with $k$
inputs (with $f$ encoded as a string of $2^{k}$ bits, and hence with
$k\in\operatorname{LogLog}$). We say that $f$ is _average-case
$\epsilon$-hard_, written as $\operatorname{Hard}^{\text{A}}_{\epsilon}(f)$,
if for every circuit $C$ of size at most $2^{\epsilon k}$,

$|\\{u<2^{k}\mid C(u)=f(u)\\}|<(1/2+2^{-\epsilon k})2^{k}.$

Note that $\operatorname{Hard}^{\text{A}}_{\epsilon}(f)$ is
$\Pi_{1}^{b}$-definable in $\mathsf{PV_{1}}$.

We write $\operatorname{tt}^{\text{avg}}_{\epsilon}(f_{k},2^{\epsilon
k})\coloneqq||\operatorname{Hard}^{\text{A}}_{\epsilon}(f)||_{m}$ for the
propositional translation (see Section 2.2.3) of the formula
$\operatorname{Hard}^{\text{A}}_{\epsilon}(f)$ above, and an appropriately
chosen parameter $m$ depending on $k$ and $\epsilon$. We also consider the
polynomial-time function $\operatorname{CorrectFracTT}^{\delta}(s,n,C,f)$,
that checks whether $f$ is a string of length $2^{n}$, $C$ encodes a circuit
of size at most $s$, and finally verifies whether the fraction of accepted
inputs is larger than $(1/2+2^{-\delta n})2^{n}$.

The theory $\mathsf{APC_{1}}$ is strong enough to show that hard-on-average
functions do exist.

######  Proposition 2.2 ([Jeř07] [Jeř04]).

For every rational constant $\epsilon<1/3$, there exists a constant $c$ such
that $\mathsf{APC_{1}}$ proves that for every $k\in\operatorname{LogLog}$ such
that $k\geq c$, there exist a function $f:2^{k}\rightarrow 2$ that is average-
case $\epsilon$-hard.

The theory $\mathsf{S^{1}_{2}}$ can be relativized to
$\mathsf{S^{1}_{2}}(\alpha)$. This means, in particular, that the language of
$\mathsf{S^{1}_{2}}(\alpha)$, denoted also $\mathsf{S^{1}_{2}}(\alpha)$,
contains symbols for all polynomial-time machines with access to the oracle
$\alpha$.

######  Definition 2.3 (${\sf sHARD}^{\text{A}}$ [Jeř04]).

The theory ${\sf sHARD}^{\text{A}}$ is an extension of the theory
$\mathsf{S^{1}_{2}}(\alpha)$ by the axioms stating

  1. 1.

the number $\alpha(x)$ encodes the truth table of a Boolean function in
$||x||$ variables;

  2. 2.

$x\geq c\rightarrow\operatorname{Hard}^{\text{A}}_{1/4}(\alpha(x))$, where $c$
is the constant from the previous proposition;

  3. 3.

$||x||=||y||\rightarrow\alpha(x)=\alpha(y)$.

The key technical tool from the framework of approximate counting is the
following theorem by [Jeř07].

######  Theorem 2.4 ([Jeř07] [Jeř07]).

There is a $\mathsf{PV}(\alpha)$-function $\operatorname{Size}$ such that
${\sf sHARD}^{\text{A}}$ proves that if $X\subseteq 2^{n}$ is definable by a
circuit $C$, then $X\approx_{\epsilon}\operatorname{Size}(\alpha,C,2^{n},e)$,
where $\epsilon=|e|^{-1}$.

For a circuit $C:2^{n}\to 2$, we introduce the notation

$\Pr_{x<y}[C(x)=1]\preceq_{\epsilon}^{f}\frac{z}{w}$

to mean $w\cdot\operatorname{Size}(f,C,2^{n},e)\leq y\cdot z$, where
$\epsilon=|e|^{-1}$.

####  2.2.3 Correspondences and propositional translations

While our formalizations are comfortably carried out in the first-order
theories presented above, we are able to transfer our results back to
propositional logic thanks to the existence of _propositional translations_.
Following [Kra19] [Kra19], we say that a theory $T$ _corresponds_ to a
propositional proof system $S$ if (i) $T$ can prove the soundness of $S$ and
(ii) every universal consequence $\forall x\varphi(x)$ of $T$, where $\varphi$
is quantifier-free, admits polynomial-size proofs in $S$ when grounded into a
sequence of propositional formulas. [Pud20] alternatively says that $S$ is the
_weak system_ of the theory $T$ [Pud20]. More formally, for such a universal
formula $\varphi$, we denote by $||\varphi||_{n}$ the propositional
translation for models of size $n$. Sometimes we abuse the notation and write
$||\varphi||$ dropping the subscript $n$. We refer the reader to standard
texts like those of [Kra19] [Kra19] or [CN10] [CN10] for formal definitions of
the translation.

The key fact for us is that universal theorems of $\mathsf{S^{1}_{2}}$ admit
short propositional proofs in Extended Frege. More importantly,
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ corresponds to Implicit Extended
Frege.

######  Theorem 2.5 (Correspondence of
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ and $\mathsf{iEF}$ [Kra04a, Thm.
2.1]).

The proof system $\mathsf{iEF}$ corresponds to
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$. That is,

  1. (i)

the theory $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ proves the soundness
of $\mathsf{iEF}$;

  2. (ii)

whenever a $\forall\Pi_{1}^{b}$-sentence $\forall x\varphi(x)$ is provable in
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$, there are polynomial-size
$\mathsf{iEF}$-proofs of the sequence of tautologies
$\\{||\varphi||_{n}\\}_{n\in\mathbb{N}}$;

  3. (iii)

if $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ proves the soundness of some
propositional system $S$, then $\mathsf{iEF}\geq S$.

The translation also works for formulas beyond $\forall\Pi^{b}_{1}$ as long as
we translate into a quantified propositional system. The definition of the
translation is straightforward, and we note that $\Sigma^{b}_{1}$ consequences
of $\mathsf{S^{1}_{2}}$ translated as $\Sigma_{1}^{q}$ formulas admit
polynomial-size proofs in $\mathsf{G^{*}_{1}}$.

######  Theorem 2.6 (Correspondence of $\mathsf{S^{1}_{2}}$ and
$\mathsf{G^{*}_{1}}$ [KP90]).

Whenever a $\forall\Sigma_{1}^{b}$-sentence $\forall x\exists y\leq
t.\varphi(x,y)$ is provable in $\mathsf{S^{1}_{2}}$, there are polynomial-size
proofs of the sequence of $\Sigma^{q}_{1}$-formulas $\\{||\exists
x\varphi(x,y)||_{n}\\}_{n\in\mathbb{N}}$ in $\mathsf{G^{*}_{1}}$.

###  2.3 Interactive proof systems and the sum-sheck protocol

While our focus is on propositional proof systems in the sense of Cook and
Reckhow, our work exploits relations to more lax notions of provability.
Following [Bab85] [Bab85], an _Merlin-Arthur proof system_ or _Merlin-Arthur
protocol_ for a language $L\subseteq\\{0,1\\}^{*}$ is a polynomial-time
function $S$ together with some constant $c$ such that the two following
properties are satisfied for every $x\in\\{0,1\\}^{*}$. Namely,

  1. 1.

if $x\in L$, then there exists some $\pi\in\\{0,1\\}^{*}$ such that
$\Pr_{r\in\\{0,1\\}^{(|x|+|\pi|)^{c}}}[S(x,\pi,r)=1]=1$;

  2. 2.

if $x\not\in L$, then for every $\pi\in\\{0,1\\}^{*}$,
$\Pr_{r\in\\{0,1\\}^{(|x|+|\pi|)^{c}}}[S(x,\pi,r)=1]<1/3$.

The first condition formalizes _completeness_ , while the second corresponds
to _soundness_. The complexity class $\MA$ contains all languages that admit a
polynomially-bounded Merlin-Arthur protocol, meaning that there exists a
constant $d$ such that the completness guarantee is strengthened to proofs
$\pi\in\\{0,1\\}^{|x|^{d}}$. One should think of MA proof systems as Cook-
Reckhow systems where the verifier is randomized and may thus accept some
incorrect proofs with small probability.

We recall that, under the standard derandomization assumption that there
exists a Boolean function family in $\E$ that is wort-case hard for
subexponential-size circuits, every Merlin-Arthur system derandomizes into a
Cook-Reckhow system and, in particular, $\MA=\NP$ [NW94, IW97].

Our proofs rely on a particular interactive protocol, the _Sum-Check Protocol_
of Lund, Fortnow, Karloff, and Nisan [LFKN92] for the language of
unsatisfiable 3CNFs. Unlike Merlin-Arthur protocols, this is an interactive
protocol running for multiple rounds between a Prover and a Verifier, before
the Verifier makes a decision. We now recall the details of the protocol.

##### The Sum-Check Protocol [LFKN92]

The protocol considers a 3CNF $\varphi(x_{1},\dots,x_{n})$ over $m$ clauses,
known to both the Verifier and the Prover.

  1. 1.

The Prover generates a prime number101010The constant $c_{p}$ in the exponent
comes from the formalization of the soundness of the sum-check protocol inside
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ in a recent work of [Kha23a]
[Kha23a]; while we do not need such details in our proofs, we leave it here to
be faithful to the formalization.
$p\in(2^{2n^{3}+n},2^{{(2n^{3}+n)}^{c_{p}}}]$ together with a Pratt
certificate111111A _Pratt certificate_ is a succinct witness for primality
checkable in polynomial time [Pra75]. The details are not relevant for our
results, but it is important that the Verifier can be convinced of $p$ being a
prime. on the primality of $p$ and sends them to the Verifier, who checks for
correctness of the certificate, and aborts if incorrect.

  2. 2.

The Prover and the Verifier arithmetize $\varphi$ into a polynomial
$P_{\varphi}(x_{1},\dots,x_{n})$ of degree at most $3m$ over $\mathbb{F}_{p}$
in the usual way: a clause like $(x\lor\neg y\lor z)$ is turned into
$1-(1-x)y(1-z)$, and one then takes the product of all such arithmetized
clauses. In this way, for all $x\in\\{0,1\\}^{n}$, $\varphi(x)=1$ if and only
if $P_{\varphi}(x)=1$.

  3. 3.

The Verifier sets $(a_{1},\dots,a_{n})\coloneqq(0,\dots,0)$, $Q_{0}(a_{0}):=0$
and for $i\in\\{1,\dots n\\}$, the following interaction is carried out:

    1. (a)

Leaving $x_{i}$ free, the Prover computes the coefficients of the following
univariate polynomial over $\mathbb{F}_{p}$,
$Q_{i}(x_{i})\coloneqq\sum_{x_{i+1}\in\\{0,1\\}}\dots\sum_{x_{n}\in\\{0,1\\}}P_{\varphi}(a_{1},\dots,a_{i-1},x_{i},x_{i+1},\dots,x_{n})$
and sends the $O(m)$ coefficients of $Q_{i}$ to the Verifier.

    2. (b)

The Verifier checks whether $Q_{i}(0)+Q_{i}(1)=Q_{i-1}(a_{i-1})$. If the check
fails, the Verifier rejects. Otherwise, it samples a random
$a_{i}\in\mathbb{F}_{p}$ and sends it to the Prover.

    3. (c)

In the final round, instead of sending $a_{n}$ to the Prover, the Verifier
checks whether $P_{\varphi}(a_{1},\dots,a_{n})=Q_{n}(a_{n})$ and accepts or
rejects based on this.

##  3 Main result

Our proof exploits the known fact that if $\\#\P\subseteq\FP/\poly$, then
$\coNP\subseteq\MA$. Indeed, if $\\#\P$ has small circuits one can provide
polynomial-size circuits that simulate the Prover’s movements in the Sum-Check
protocol for $\UNSAT$, since one can consider the MA proof system in which
Arthur receives from Merlin a circuit claiming to be the circuit that the
Prover used to carry out their strategy, and with the aid of randomness,
Arthur can execute this on his own and decide based on the outcome of this
simulation.

Let us make this formal.

######  Definition 3.1 (The $\mathsf{SC}$ proof system).

Let $V(p,u,\varphi,C,r)$ be the polynomial-time function carrying out the
simulation of the Sum-Check protocol. Namely, $p$ is intended to be a prime in
$(2^{2n^{3}+n},2^{{(2n^{3}+n)}^{c_{p}}}]$, $u$ a Pratt certificate for $p$,
$\varphi$ a 3CNF over $n$ variables, $r$ a string of random bits, and $C$ a
multi-output circuit providing the Prover’s responses in the interactions with
the Verifier in the Sum-Check protocol.

The _Sum-Check Proof System_ , denoted by $\mathsf{SC}$, is a Merlin-Arthur
proof system for proving 3DNF tautologies. An $\mathsf{SC}$ proof of $\varphi$
is a tuple $\langle p,u,C\rangle$ such that $p$ is indeed a prime in the
interval above, correctly certified by the Pratt certificate $u$, and such
that $\Pr_{r\in\mathbb{F}_{p}^{n}}\big{[}V(p,u,\neg\varphi,C,r)=1\big{]}=1$.

The following is just a rephrasing of the fact that $\\#\P\subseteq\FP/\poly$
implies $\coNP\subseteq\MA$, in terms of the Merlin-Arthur system
$\mathsf{SC}$.

######  Lemma 3.2.

If $\\#\P\subseteq\FP/\poly$, then $\mathsf{SC}$ is polynomially bounded over
3DNF tautologies.

###### Proof.

Suppose $\\#\P\subseteq\FP/\poly$ and observe closely the computational tasks
of the Prover in the Sum-Check protocol. On input a formula $\varphi$ over $n$
variables, the Prover sends a prime number in the range
$(2^{2n^{3}+n},2^{{(2n^{3}+n)}^{c_{p}}}]$. Note that the well-known Betrand’s
postulate in number theory states that for every $a>3$, there is a prime in
the interval $(a,2a-2)$. Since $2^{{(2n^{3}+n)}^{c_{p}}}>2\cdot
2^{2n^{3}+n}-2$, such a prime $p$ always exists in our interval, which we fix
for all our proofs of formulas over $n$ variables.

We shall now argue that, on inputs of size $n$, there is a multi-output
circuit $C_{n}$ taking as input the number of the round in the protocol and
the information sent by the Verifier, and which outputs the coefficients of
the polynomial $Q_{i}$. Note that for formulas over $m$ clauses, this is an
$O(m)$-degree polynomial, and thus it suffices to evaluate it at $O(m)$ points
in the field (say, the first $O(m)$ elements in $\mathbb{F}_{p}$) and then
solve a system of linear equations to learn the coefficients. The hard task is
to evaluate the polynomial $Q_{i}$, but this is precisely a $\\#\P$ task,
since it amounts to adding the outputs of the function
$P_{\varphi}(a_{1},\dots,a_{i-1},x_{i},x_{i+1},\dots,x_{n})$, which can be
efficiently evaluated, for every possible
$(x_{i+1},\dots,x_{n})\in\\{0,1\\}^{n-i}$. Since $\\#\P\subseteq\FP/\poly$,
there is a small circuit taking care of this task, which we use inside our
circuit $C_{n}$. Then, the prime $p$ for inputs of size $n$, together with a
suitable Pratt certificate (which is always small) and the polynomial-size
circuit $C_{n}$ constitute a polynomial-size $\mathsf{SC}$ proof of the
formula $\varphi$. ∎

At this point, our goal is to extend the previous lemma from $\mathsf{SC}$ to
a concrete and natural Cook-Reckhow system. Our goal is to do this for
Implicit Extended Frege. The idea again is that $\mathsf{iEF}$ (or rather its
first-order counterpart, $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$) can
prove the soundness of this system and thus simulate it. We shall then
derandomize the $\mathsf{SC}$ protocol inside $\mathsf{iEF}$, to argue that
$\mathsf{iEF}$ must satisfy the same connection to lower bounds as
$\mathsf{SC}$ does in the lemma above.

Fortunately for us, the soundness of the Sum-Check protocol was recently
proven by Khaniki in the right theory of bounded arithmetic.

######  Theorem 3.3 (Soundness of the sum-check protocol [Kha23, Thm. 15.3]).

There are constants $c,k\in\mathbb{N}$ such that $\mathsf{S^{1}_{2}}$ proves
the following sentence: for every $n,\varphi,a,p,u,C$, if it holds that (i)
$\varphi$ is a 3CNF in $n$ variables where $n\geq c$, and (ii) $\varphi(a)=1$
and, (iii) $2^{2n^{3}+n}<p\leq 2^{{(2n^{3}+n)}^{c_{p}}}$ and, (iv)
$n^{k}\in\operatorname{Log}\operatorname{Log}$, then

$\operatorname*{Pr}_{r\in\mathbb{F}_{p}^{n}}\big{[}V(p,u,\varphi,C,r)=1\big{]}\leq\frac{n\binom{2n}{3}}{p}.$

Based on the soundness of the interactive protocol, we can now formalize the
soundness of the $\mathsf{SC}$ proof system from Definition 3.1. The arguments
that follow can be seen as a concrete application of more sophisticated
techniques employed by [Kha23a] [Kha23a, Kha23], who has studied interactive
protocols in the context of defining new jump operators in proof complexity.

######  Definition 3.4 (The $\operatorname{Sound}_{c}(\mathsf{SC})$ formula).

We denote by $\operatorname{Sound}_{c}(\mathsf{SC})$ the following
$\forall\Sigma^{b}_{1}$ sentence, claiming the soundness of $\mathsf{SC}$: for
all $\varphi,a,p,u,C,f$, where $|\varphi|>c$, there is a circuit $D$ of size
$\leq\lceil|f|^{1/4}\rceil$ such that if

$\neg\left(\operatorname*{Pr}_{r\in\mathbb{F}_{p}^{n}}[V(p,u,\neg\varphi,C,r)=1]\preceq^{f}_{\epsilon}\frac{3}{8}\right)$

holds, then at least one of the following conditions holds:

  1. (i)

$|f|\neq|C|^{k_{a}}+k^{\prime}_{a}$ or,

  2. (ii)

$\operatorname{CorrectFracTT}^{1/4}(\lceil|f|^{1/4}\rceil,||f||,D,f)=1$ or,

  3. (iii)

$p\not\in(2^{2n^{3}+n},2^{{(2n^{3}+n)}^{c_{p}}}]$ or,

  4. (iv)

$\varphi(a)=1$,

where $k_{a},k^{\prime}_{a}$ are the constants from Theorem 2.4 ensuring that
$\operatorname{Size}$ function works properly (see the remark below),
$\epsilon={1/16}$ and $n$ is the number of variables of $\varphi$. In the
definition of the displayed probability, we assume that $y=p^{n}$, that the
circuit defining the set of strings accepted by $V$ has $m$ inputs, for the
smallest integer $m$ such that $2^{m}\geq p^{n}$, and that it rejects all
$r\geq p^{n}$.

A couple of remarks are in place. First, note that even if $V$ accepts with
probability 1, the probability can be approximated in Definition 3.4 by a
significantly smaller value because of the difference between $p^{n}$ and
$2^{m}$. Another relevant point is that, as a closer look at the proof of
Theorem 2.4 reveals, for each $C,2^{n},e$, the function
$\operatorname{Size}(\alpha,C,2^{n},e)$ calls $\alpha$ only once. In fact, it
calls $\alpha$ on an input $x$ which depends only on $|C|,n,|e|$. This is
needed for the formula $\operatorname{Sound}_{c}(\mathsf{SC})$ to be well-
defined: in Definition 3.4 we do not supply the Size function with an oracle
generating truth tables but with a single truth table $f$ representing a
single answer of the oracle.

It now suffices to verify that the encoding of the soundness of $\mathsf{SC}$
is indeed provable in $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$.

######  Proposition 3.5 (Soundness of $\mathsf{SC}$ inside
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$).

There is a constant $c\in\mathbb{N}$ such that
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}\vdash\operatorname{Sound}_{c}(\mathsf{SC})$.

###### Proof.

Let $c\in\mathbb{N}$ be a big enough constant that can be computed from the
rest of the argument and

$\operatorname{Sound}_{c}(\mathsf{SC})\coloneqq\forall\varphi,a,p,u,C,f\exists
D\Phi(\varphi,a,p,u,C,f,D)$

the soundness formula in Definition 3.4 above. Let $\varphi$ be a 3DNF in $n$
variables such that $|\varphi|>c$, and consider $a,p,u,C,f$. Then the
following cases can happen:

  1. (a)

If $|f|\neq|C|^{k_{a}}+k^{\prime}_{a}$ or
$p\not\in(2^{2n^{3}+n},2^{{(2n^{3}+n)}^{c_{p}}}]$, then
$\Phi(\varphi,a,p,u,C,f,0)$ is trivially true.

  2. (b)

If there is a circuit $D$ of size $\leq\lceil|f|^{1/4}\rceil$ such that
$\operatorname{CorrectFracTT}^{1/4}(\lceil|f|^{1/4}\rceil,||f||,D,f)=1$, then
the formula $\Phi(\varphi,a,p,u,C,f,D)$ is trivially true.

  3. (c)

If the previous cases do not happen and moreover

$\neg\left(\operatorname*{Pr}_{r\in\mathbb{F}_{p}^{n}}[V(p,u,\neg\varphi,C,r)=1]\preceq^{f}_{\epsilon}\frac{3}{8}\right)$

holds, then we have that $8\cdot\operatorname{Size}(f,C^{*},2^{m},e)>3p^{n}$,
where $m$ is the smallest integer such that $2^{m}\geq p^{n}$,
$\epsilon\coloneqq|e|^{-1}$ and $C^{*}(r)\coloneqq V(p,u,\neg\varphi,C,r)$. By
the assumption $\operatorname{Hard}_{1/4}^{\text{A}}(f)$ holds and by the fact
that we are over $\mathsf{S^{1}_{2}}$ and we can use $f$ as a parameter in
polynomial induction for $\Sigma^{b}_{1}$ formulas, we can do approximate
counting using Theorem 2.4. (Here, we use also the fact that in order to
derive the conclusion of Theorem 2.4, the axioms postulating the properties of
$\alpha(x)$ for $x$’s not queried by $\operatorname{Size}$ are not needed.)
Hence there is a circuit $G$ and some $v\leq\poly(m\epsilon^{-1}|C^{*}|)$ such
that

$G:v\times(X_{C^{*}}\mathbin{\dot{\cup}}\>\epsilon 2^{m})\twoheadrightarrow
v\times\operatorname{Size}(f,C^{*},2^{m},e).$

As we work in $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ and $G$ is
surjective, we can find a subset $A\subseteq
v\times(X_{C^{*}}\mathbin{\dot{\cup}}\>\epsilon 2^{m})$ such that $G$
restricted to $A$ is a one-to-one function from $A$ to
$v\times\operatorname{Size}(f,C^{*},2^{m},e)$. Now we can apply exact counting
(as we have $\mathsf{1\textsf{-}EXP}$) and show that

$\operatorname{Size}(f,C^{*},2^{m},e)\leq|X_{C^{*}}|+\epsilon 2^{m}.$

By the fact that $8\cdot\operatorname{Size}(f,C^{*},2^{m},e)>3p^{n}>3\cdot
2^{m}/2$, we have ${2^{m}}/{8}<|X_{C^{*}}|$. Now if $\varphi(a)=0$, by Theorem
3.3 we get

$\operatorname*{Pr}_{r\in\mathbb{F}_{p}^{n}}\big{[}V(p,u,\neg\varphi,\pi,r)=1\big{]}\leq\frac{n\binom{2n}{3}}{p}.$

Note that $|\varphi|>c$ which implies that $n$ is big enough and as
$p>2^{2n^{3}+n}$ we get that ${n\binom{2n}{3}}/{p}\leq{1/8}$, which implies

$\operatorname*{Pr}_{r\in\mathbb{F}_{p}^{n}}\big{[}V(p,u,\neg\varphi,\pi,r)=1\big{]}\leq{\frac{1}{8}}.$

As $C^{*}$ rejects all $r\geq p^{n}$, this implies that
$|X_{C^{*}}|\leq{2^{m}}/{8}$ which leads to a contradiction, so
$\varphi(a)=1$.

∎

The main technical issue now is that $\operatorname{Sound}_{c}(\mathsf{SC})$
is a $\forall\Sigma^{b}_{1}$ sentence and thus it does not translate into a
propositional formula that $\mathsf{iEF}$ can reason about. Instead, we shall
work on a quantified propositional system, but for this to make sense we need
to know the quantified propositional proof system associated with
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$.

We invoke the following known $\TFNP$ characterization of the $\Sigma^{b}_{1}$
consequences of $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$, which identifies
a complete $\Sigma^{b}_{1}$ sentence $\Psi$ such that any other
$\Sigma^{b}_{1}$ consequence of $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$
reduces to it in $\mathsf{G^{*}_{1}}$.

######  Theorem 3.6 ([Kra90, KNT11, Kra16, BB17]).

There is a $\forall\Sigma^{b}_{1}$ sentence $\Psi\coloneqq\forall x\exists
y\psi(x,y)$ (the bound on $y$ is implicit in $\psi$) such that the following
statements are true:

  1. (i)

$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}\vdash\forall x\exists y\psi(x,y)$;

  2. (ii)

for any $\forall\Sigma^{b}_{1}$ sentence $\forall x\exists y\alpha(x,y)$ such
that $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}\vdash\forall x\exists
y\alpha(x,y)$, there are $\mathsf{PV}$ functions $f$ and $g$ such that
$\mathsf{S^{1}_{2}}\vdash\forall x,y(\psi(f(x),y)\to\alpha(x,g(x,y))).$

In what follows, we shall work with Gentzen’s system $\mathsf{G}$ extended
with the propositional translation of the sentence $\Psi$ in the theorem
above. We denote this system by
$\mathsf{G_{EXP}}\coloneqq\mathsf{G^{*}_{1}}+||\Psi||$ and prove the following
key properties about it.

######  Corollary 3.7.

The following statements about $\mathsf{G_{EXP}}$ hold:

  1. (i)

$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}\vdash\Sigma^{q}_{1}\text{-}\operatorname{Ref}(\mathsf{G_{EXP}})$,
i.e. the reflection principle for $\mathsf{G_{EXP}}$ and $\Sigma^{q}_{1}$
formulas is provable in $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$;

  2. (ii)

for every $\forall\Sigma^{b}_{1}$-sentence $\forall x\exists y\alpha(x,y)$, if
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}\vdash\forall x\exists
y\alpha(x,y)$, then there are polynomial-size $\mathsf{G_{EXP}}$-proofs of the
sequence of $\Sigma^{q}_{1}$-tautologies $\\{||\exists
y\alpha(y)||_{n}\\}_{n\in\mathbb{N}}$;

  3. (iii)

if $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ proves the soundness of a
propositional proof system $S$, then $\mathsf{G_{EXP}}\geq S$.

###### Proof.

The proof of this corollary is standard and it is similar to the case of the
usual correspondence for propositional proof systems and theories (see, for
example, [Pud20]). Here we only sketch the proof item by item.

  1. (i)

Working in $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$, let $\pi$ be a
$\mathsf{G_{EXP}}$-proof of $\exists\bar{q}\varphi(\bar{p},\bar{q})$ and $a$
be an assignment for the $\bar{p}$ variables. Let
$\psi^{\prime}_{1},...,\psi^{\prime}_{k}$ be the substitution instances of
$||\Psi||$ that are used in $\pi$. This means that there is a
$\mathsf{G^{*}_{1}}$-proof $\pi^{\prime}$ of the formula
$\bigvee^{k}_{i=1}\neg\psi^{\prime}_{i}\lor\exists\bar{q}\varphi(\bar{p},\bar{q})$.
Since $\mathsf{S^{1}_{2}}$ proves the reflection principle for
$\mathsf{G^{*}_{1}}$ for $\Sigma^{q}_{1}$-formulas [Kra95], it knows that the
formula is true. Moreover, by Theorem 3.6 the sentence $\Psi$ is provable in
$\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ which immediately implies that
$\left(\bigvee^{k}_{i=1}\neg\psi^{\prime}_{i}\right)[a/\bar{p}]$ is false and
hence $\exists\bar{q}\varphi(a,\bar{q})$ is true.

  2. (ii)

Suppose $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}\vdash\forall x\exists
y\alpha(x,y)$ where $\forall x\exists y\alpha(x,y)$ is a $\Sigma^{b}_{1}$
sentence. Then by Theorem 3.6, there are $\mathsf{PV}$ functions $f$ and $g$
such that $\mathsf{S^{1}_{2}}\vdash\forall
x,y(\psi(f(x),y)\to\alpha(x,g(x,y)))$. Then by Theorem 2.6 there are
polynomial-size $\mathsf{G^{*}_{1}}$-proofs of

$\\{||\forall x,y(\psi(f(x),y)\to\alpha(x,g(x,y)))||_{n}\\}_{n\in\mathbb{N}}.$

Note that $\mathsf{G_{EXP}}$ has substitution instances of $||\Psi||$ which
implies that using the rules of $\mathsf{G^{*}_{1}}$ we get polynomial-size
$\mathsf{G_{EXP}}$-proofs of the sequence $\\{||\forall x\exists
y\alpha(x,y)||_{n}\\}_{n\in\mathbb{N}}$.

  3. (iii)

If $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ proves
$\operatorname{Ref}(S)$, then by the previous item, $\mathsf{G_{EXP}}$ has
polynomial-size proofs of the family
$\\{||\operatorname{Ref}(S)||_{n}\\}_{n\in\mathbb{N}}$ and so
$\mathsf{G_{EXP}}\geq S$ (see Section 2.1.1 for details on correspondences and
simulations).

∎

Let us observe that $\mathsf{G_{EXP}}$ is in fact equivalent to
$\mathsf{iEF}$.

######  Lemma 3.8.

The proof systems $\mathsf{iEF},\mathsf{EF}+\operatorname{Ref}_{\mathsf{iEF}}$
and $\mathsf{G_{EXP}}$ are polynomially equivalent over propositional
tautologies.

###### Proof.

By item (iii) of Corollary 3.7 and item (iii) Theorem 2.5, $\mathsf{iEF}$ and
$\mathsf{G_{EXP}}$ polynomially simulate each other. As mentioned in Section
2.1.1, $\mathsf{EF}+\operatorname{Ref}_{\mathsf{iEF}}\geq\mathsf{iEF}$. It is
also easy to see that $\mathsf{S^{1}_{2}}+\mathsf{1\textsf{-}EXP}$ proves the
soundness of $\mathsf{EF}+\operatorname{Ref}_{\mathsf{iEF}}$, which by item
(iii) of Theorem 2.5 gives us
$\mathsf{iEF}\geq\mathsf{EF}+\operatorname{Ref}_{\mathsf{iEF}}$. ∎

We are now ready to define the extension of $\mathsf{iEF}$ for which our main
theorem holds. Recall that the propositional formulas
$\operatorname*{tt}^{\text{avg}}_{1/4}(h_{n},2^{n/4})$ were defined in Section
2.2.2 and state the average-case hardness of a Boolean function $h_{n}$
represented as a truth table (hence the name tt).

######  Definition 3.9 (The systems $\mathsf{iEF}^{\operatorname{tt}}$).

Let $h=\\{h_{n}\\}_{n\in\mathbb{N}}$ be some family of Boolean functions, and
let $n_{0}\in\mathbb{N}$. We denote by
$\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}\coloneqq\mathsf{G_{EXP}}+\\{\operatorname*{tt}^{\text{avg}}_{1/4}(h_{n},2^{n/4})\\}_{n\geq
n_{0}}$ the system that extends $\mathsf{G_{EXP}}$ by the axioms claiming the
hardness of $h_{n}$, for $n\geq n_{0}$.

Note that $\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$ is a family of proof
systems, parameterized by a Boolean function family $h$ and some threshold
parameter $n_{0}$. Observe that depending on the choice of $h$ and $n_{0}$,
the system $\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$ may not be a Cook-
Reckhow system: if $h$ is not a hard function, or $n_{0}$ is not large enough,
we will be adding axioms which are not tautologies, and the system will be
inconsistent; and even if $h$ is hard and $n_{0}$ is large enough, the system
may require advice in order to verify the proofs. As we shall see, however,
these degenerate instantiations of $\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$
are not a problem.

What is more important, the systems
$\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$, regardless of their consistency,
always simulate $\mathsf{SC}$.

######  Lemma 3.10.

Let $h$ be family of Boolean functions and let $n_{0}\in\mathbb{N}$. The
system $\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$ polynomially simulates
$\mathsf{SC}$ over 3DNF tautologies.

###### Proof.

If the system $\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$ is unsound because
the added axioms are not tautologies, then the system is trivially
polynomially bounded and so it simulates every other proof system.

Suppose the added axioms are indeed tautologies, meaning that the function $h$
is indeed hard on average.

Let $\varphi_{1}$ be a 3DNF in $n_{1}$ variables and
$\left<p_{1},u_{1},C_{1}\right>$ be a $\mathsf{SC}$-proof of $\varphi_{1}$.
This means

$2^{2n_{1}^{3}+n_{1}}<p_{1}\leq
2^{{(2n_{1}^{3}+n_{1})}^{c_{p}}}\land\operatorname*{Pr}_{r\in\mathbb{F}_{p_{1}}^{n_{1}}}\big{[}V(p_{1},u_{1},\neg\varphi_{1},C_{1},r)=1\big{]}=1.$

Note that by Theorem 3.3 and Corollary 3.7, there are $\mathsf{PV}$ functions
$l,g$ such that

$\mathsf{S^{1}_{2}}\vdash\forall\varphi,a,p,u,C,f\left(\psi(l(\varphi,a,p,u,C,f),y)\to\Phi(\varphi,a,p,u,C,f,g(\varphi,a,p,u,C,f,y))\right),$

where
$\operatorname{Sound}_{c}(\mathsf{SC})\coloneqq\forall\varphi,a,p,u,C,f\exists
D\Phi(\varphi,a,p,u,C,f,D)$. Let $s\coloneqq|\left<p,u,C\right>|$. Then by
Theorem 2.6 there is a $s^{O(1)}$-size $\mathsf{G^{*}_{1}}$-proof of

$||\forall\varphi,a,p,u,C,f\left(\psi(l(\varphi,a,p,u,C,f),y)\to\Phi(\varphi,a,p,u,C,f,g(\varphi,a,p,u,C,f,y))\right)||_{s^{\prime}},$

where $s^{\prime}\coloneqq\poly(s)$. Let us rewrite the previous quantified
propositional formula as $||\Psi^{\prime}||\to||\Phi^{\prime}||$ with the
right range of parameters such that $p_{1},u_{1},\varphi_{1},C_{1}$ are
substituted in the formula in their corresponding places. Now we take the
substitution instance
$\operatorname*{tt}^{\operatorname{avg}}_{1/4}(h_{n^{\prime}},2^{n^{\prime}/4})$
where $|h_{n^{\prime}}|\coloneqq|C_{1}|^{k_{a}}+k^{\prime}_{a}$ and we
substitute $h_{n^{\prime}}$ to the variables corresponding to $f$ and
therefore the disjunct which corresponds to $\operatorname{CorrectFracTT}$
disappears from $||\Phi^{\prime}||$ when we apply the rules of
$\mathsf{G^{*}_{1}}$. Moreover, it is not hard to verify that after the
substitutions every other disjunct which corresponds to subformulas of
$\operatorname{Sound}_{c}(\mathsf{SC})$ from Definition 3.4 disappears except
$\varphi_{1}$. So what we have is $\mathsf{G^{*}_{1}}$-proof of
$||\Psi^{\prime\prime}||(\bar{x},\bar{y})\to\varphi_{1}(\bar{x})$ ($\bar{x}$
and $\bar{y}$ are disjoint variables) where $||\Psi^{\prime\prime}||$ is a
substitution instance of $||\Psi^{\prime}||$. Since we are working in
$\mathsf{G_{EXP}}$, we have the substitution instance
$\exists\bar{y}||\Psi^{\prime\prime}||(\bar{x},\bar{y})$ and therefore using
the rules of $\mathsf{G^{*}_{1}}$ we get a short $\mathsf{G_{EXP}}$-proof of
$\varphi_{1}(\bar{x})$. ∎

Our main theorem now easily follows.

######  Theorem 3.11 (Main theorem).

Let $h$ be a family of Boolean functions and let $n_{0}\in\mathbb{N}$. If the
system $\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$ is not polynomially
bounded, then $\\#\P\not\subseteq\FP/\poly$.

###### Proof.

By Lemma 3.10 above, for every choice of $h$ and $n_{0}$, the system
$\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$ polynomially simulates
$\mathsf{SC}$, so if $\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$ is not
polynomially bounded, then $\mathsf{SC}$ is not either. Then, by the
contrapositive of Lemma 3.2, $\\#\P\not\subseteq\FP/\poly$. ∎

As discussed, depending on the choice of $h$ and $n_{0}$, the system
$\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$ may not be sound and thus possibly
not a Cook-Reckhow system. However, for any fixed choice of a uniform
candidate hard function, the system is concrete and exhibits the desired
connection that proof complexity lower bounds for it imply strong circuit
lower bounds. In particular, if there exist functions in $\NE\cap\coNE$
average-case hard for subexponential-size circuits, then we recover the
version of the theorem presented in the introduction (Theorem 1.1).

We note that there is the possibility that $\mathsf{iEF}$, given its strength,
already proves such strong circuit lower bounds for some Boolean function. It
is thus worth to mention the following corollary.

######  Corollary 3.12.

Suppose there exists a sequence of Boolean functions
$\\{h_{n}\\}_{n\in\mathbb{N}}$ for which $\mathsf{iEF}$ has polynomial-size
proofs of the formula family
$\\{\operatorname*{tt}^{\operatorname{avg}}_{1/4}(h_{n},2^{n/4})\\}_{n\geq
n_{0}}$ for some sufficiently large $n_{0}\in\mathbb{N}$. If $\mathsf{iEF}$ is
not polynomially bounded, then $\\#\P\not\subseteq\FP/\poly$.

###### Proof.

If there is such a function $h$ and threshold $n_{0}$, then
$\mathsf{iEF}^{\operatorname{tt}(h,n_{0})}$ is polynomially equivalent to
$\mathsf{iEF}$ itself, so by Theorem 3.11 the corollary follows. ∎

### Acknowledgments

Independently, Albert Atserias suggested to us to consider the possibility of
using interactive proof systems in order to derive circuit lower bounds from
proof complexity lower bounds.

We would like to thank Pavel Pudlák for useful comments and suggestions. We
are also grateful to different anonymous reviewers for several comments and
references.

This work was done in part while the first author was visiting the University
of Oxford and the Institute of Mathematics of the Czech Academy of Sciences.

Noel Arteche was supported by the Wallenberg AI, Autonomous Systems and
Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.
Erfan Khaniki was supported by the Institute of Mathematics of the Czech
Academy of Sciences (RVO 67985840) and GAČR grant 19- 27871X. Ján Pich
received support from the Royal Society University Research Fellowship
URF$\backslash$R1$\backslash$211106 Proof complexity and circuit complexity: a
unified approach.

For the purpose of Open Access, the authors have applied a CC BY public
copyright license to any Author Accepted Manuscript version arising from this
submission.

## References

  * [AB09] Sanjeev Arora and Boaz Barak  “Computational Complexity: A Modern Approach”  Cambridge University Press, 2009
  * [AB87] Noga Alon and Ravi B Boppana  “The monotone circuit complexity of Boolean functions”  In _Combinatorica_ 7 Springer, 1987, pp. 1–22
  * [ACG24] Noel Arteche, Gaia Carenini and Matthew Gray  “Quantum Automating $\TC^{0}$-Frege Is LWE-Hard”  In _arXiv preprint arXiv:2402.10351_ , 2024
  * [Ajt83] Miklós Ajtai  “$\Sigma_{1}^{1}$-formulae on finite structures”  In _Annals of Pure and Applied Logic_ 24.1 Elsevier, 1983, pp. 1–48
  * [Ajt94] Miklós Ajtai  “The complexity of the pigeonhole principle”  In _Combinatorica_ 14 Springer, 1994, pp. 417–433
  * [And85] Alexander Andreev  “On a method for obtaining lower bounds for the complexity of individual monotone functions”  In _Soviet Math. Dokl._ 31.3, 1985, pp. 530–534
  * [Bab85] László Babai  “Trading group theory for randomness”  In _Proceedings of the seventeenth annual ACM symposium on Theory of computing_ , 1985, pp. 421–429
  * [BB17] Arnold Beckmann and Sam Buss  “The $\NP$ search problems of Frege and Extended Frege proofs”  In _ACM Transactions on Computational Logic (TOCL)_ 18.2 ACM New York, NY, USA, 2017, pp. 1–19
  * [BBCP20] Olaf Beyersdorff, Ilario Bonacina, Leroy Chew and Jan Pich  “Frege systems for quantified Boolean logic”  In _Journal of the ACM (JACM)_ 67.2 ACM New York, NY, USA, 2020, pp. 1–36
  * [BDG+04] Maria Luisa Bonet et al.  “Non-automatizability of bounded-depth Frege proofs”  In _computational complexity_ 13 Springer, 2004, pp. 47–68
  * [BIK+92] Paul Beame et al.  “Exponential lower bounds for the pigeonhole principle”  In _Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing_ , 1992, pp. 200–220
  * [BPR00] Maria Luisa Bonet, Toniann Pitassi and Ran Raz  “On interpolation and automatization for Frege systems”  In _SIAM Journal on Computing_ 29.6 SIAM, 2000, pp. 1939–1967
  * [BPU92] Stephen Bellantoni, Toniann Pitassi and Alasdair Urquhart  “Approximation and small-depth Frege proofs”  In _SIAM Journal on Computing_ 21.6 SIAM, 1992, pp. 1161–1179
  * [Bür00] Peter Bürgisser  “Completeness and Reduction in Algebraic Complexity Theory”  In _Algorithms and Computation in Mathematics_ Springer Berlin Heidelberg, 2000
  * [Bus85] Samuel R Buss  “Bounded arithmetic”  Princeton University, 1985
  * [Bus95] Samuel R Buss  “Relating the bounded arithmetic and polynomial time hierarchies”  In _Annals of Pure and Applied Logic_ 75.1-2, 1995, pp. 67–77
  * [CK07] Stephen Cook and Jan Krajíček  “Consequences of the provability of $\NP\subseteq\Ppoly$”  In _The Journal of Symbolic Logic_ 72.4 Cambridge University Press, 2007, pp. 1353–1371
  * [CN10] Stephen Cook and Phuong Nguyen  “Logical Foundations of Proof Complexity”  Cambridge University Press, 2010
  * [Cob64] A Cobham  “The intrinsic computational difficulty of functions”  In _Proc. 1964 Congress for Logic, Methodology, and the Philosophy of Science_ , 1964, pp. 24–30  North-Holland
  * [Coo75] Stephen A. Cook  “Feasibly constructive proofs and the propositional calculus”  In _Proceedings of the Seventh Annual ACM Symposium on Theory of Computing_ , 1975, pp. 83–97
  * [Coo96] Stephen Cook  “Relating the provable collapse of $\mathbf{P}$ to $\NC^{1}$ and the power of logical theories”  In _Proof Complexity and Feasible Arithmetics_ , 1996, pp. 73–91
  * [CR79] Stephen A. Cook and Robert A. Reckhow  “The Relative Efficiency of Propositional Proof Systems”  In _Logic, Automata, and Computational Complexity_ , 1979
  * [DMN+20] Susanna De Rezende et al.  “Lifting with simple gadgets and applications to circuit and proof complexity”  In _61st Annual Symposium on Foundations of Computer Science (FOCS)_ , 2020, pp. 24–30
  * [DR23] Ben Davis and Robert Robere  “Colourful TFNP and Propositional Proofs”  In _38th Computational Complexity Conference (CCC 2023)_ 264, Leibniz International Proceedings in Informatics (LIPIcs), 2023, pp. 36:1–36:21  DOI: 10.4230/LIPIcs.CCC.2023.36
  * [dRGR22] Susanna F Rezende, Mika Göös and Robert Robere  “Proofs, circuits, and communication”  In _ACM SIGACT News_ 53.1, 2022, pp. 59–82
  * [FSS84] Merrick Furst, James B Saxe and Michael Sipser  “Parity, circuits, and the polynomial-time hierarchy”  In _Mathematical Systems Theory_ 17.1 Springer, 1984, pp. 13–27
  * [Gay22] Azza Gaysin  “Proof complexity of CSP”  In _arXiv preprint arXiv:2201.00913_ , 2022
  * [Gay24] Azza Gaysin  “Proof complexity of universal algebra in a CSP dichotomy proof”  In _arXiv preprint arXiv:2403.06704_ , 2024
  * [GGKS18] Ankit Garg, Mika Göös, Pritish Kamath and Dmitry Sokolov  “Monotone circuit lower bounds from resolution”  In _Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing_ , 2018, pp. 902–911
  * [GP18] Joshua A Grochow and Toniann Pitassi  “Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system”  In _Journal of the ACM (JACM)_ 65.6, 2018, pp. 1–59
  * [Gro23] Joshua A Grochow  “Polynomial Identity Testing and the Ideal Proof System: PIT is in $\NP$ if and only if IPS can be p-simulated by a Cook-Reckhow proof system”  In _arXiv preprint arXiv:2306.02184_ , 2023
  * [Hak20] Tuomas Hakoniemi  “Feasible interpolation for Polynomial Calculus and Sums-of-Squares”  In _47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)_ , 2020
  * [Hås86] John Håstad  “Almost optimal lower bounds for small depth circuits”  In _Proceedings of the Eighteenth Annual ACM Symposium on Theory of Computing_ , 1986, pp. 6–20
  * [IW97] Russell Impagliazzo and Avi Wigderson  “$\mathbf{P}=\mathbf{BPP}$ if $\mathbf{E}$ requires exponential circuits: Derandomizing the XOR lemma”  In _Proceedings of the Twenty-Ninth Annual ACM Symposium on Theory of computing_ , 1997, pp. 220–229
  * [Jeř04] Emil Jeřábek  “Dual weak pigeonhole principle, Boolean complexity, and derandomization”  In _Annals of Pure and Applied Logic_ 129.1-3, 2004, pp. 1–37
  * [Jeř05] Emil Jeřábek  “Weak pigeonhole principle, and randomized computation”, 2005
  * [Jeř07] Emil Jeřábek  “Approximate counting in bounded arithmetic”  In _The Journal of Symbolic Logic_ 72.3 Cambridge University Press, 2007, pp. 959–993
  * [Kha23] Erfan Khaniki  “(Im)possibilty results in Proof Complexity and Arithmetic”, 2023  URL: https://dspace.cuni.cz/handle/20.500.11956/187614
  * [Kha23a] Erfan Khaniki  “Jump Operators, Interactive Proofs, and Proof Complexity Generators” Unpublished preprint, 2023
  * [KI04] Valentine Kabanets and Russell Impagliazzo  “Derandomizing polynomial identity tests means proving circuit lower bounds”  In _Computational Complexity_ 13.1/2 Birkhauser Verlag Basel, Switzerland, Switzerland, 2004, pp. 1–46
  * [KNT11] Leszek Aleksander Kołodziejczyk, Phuong Nguyen and Neil Thapen  “The provably total $\NP$ search problems of weak second order bounded arithmetic”  In _Annals of Pure and Applied Logic_ 162.6 Elsevier, 2011, pp. 419–446
  * [KP90] Jan Krajíček and Pavel Pudlák  “Quantified propositional calculi and fragments of bounded arithmetic”  In _Zeitschrift für mathematische Logik und Grundlagen der Mathematik_ 36.1, 1990, pp. 29–46
  * [KP98] Jan Krajíček and Pavel Pudlák  “Some Consequences of Cryptographical Conjectures for $\mathsf{S^{1}_{2}}$ and $\mathsf{EF}$ ”  In _Information and Computation_ 140.1 Elsevier, 1998, pp. 82–94
  * [KPT91] Jan Krajíček, Pavel Pudlák and Gaisi Takeuti  “Bounded arithmetic and the polynomial hierarchy”  In _Annals of Pure and Applied Logic_ 52.1-2, 1991
  * [KPW95] Jan Krajíček, Pavel Pudlák and Alan Woods  “An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle”  In _Random Structures & Algorithms_ 7.1 Wiley Online Library, 1995, pp. 15–39
  * [Kra04] Jan Krajíček  “Diagonalization in proof complexity”  In _Fundamenta Mathematicae_ 182 Instytut Matematyczny Polskiej Akademii Nauk, 2004, pp. 181–192
  * [Kra04a] Jan Krajíček  “Implicit proofs”  In _The Journal of Symbolic Logic_ 69.2 Cambridge University Press, 2004, pp. 387–397
  * [Kra16] Jan Krajíček  “Consistency of circuit evaluation, Extended Resolution and total $\NP$ search problems”  In _Forum of Mathematics, Sigma_ 4, 2016, pp. e15  Cambridge University Press
  * [Kra19] Jan Krajíček  “Proof Complexity”, Encyclopedia of Mathematics and its Applications  Cambridge University Press, 2019  DOI: 10.1017/9781108242066
  * [Kra90] Jan Krajíček  “Exponentiation and second-order bounded arithmetic”  In _Annals of Pure and Applied Logic_ 48.3 Elsevier, 1990, pp. 261–276
  * [Kra94] Jan Krajíček  “Lower bounds to the size of constant-depth propositional proofs”  In _The Journal of Symbolic Logic_ 59.1 Cambridge University Press, 1994, pp. 73–86
  * [Kra95] Jan Krajíček  “Bounded Arithmetic, Propositional Logic and Complexity Theory”, Encyclopedia of Mathematics and its Applications  Cambridge University Press, 1995  DOI: 10.1017/CBO9780511529948
  * [Kra97] Jan Krajíček  “Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic”  In _The Journal of Symbolic Logic_ 62.2 Cambridge University Press, 1997, pp. 457–486
  * [LFKN92] Carsten Lund, Lance Fortnow, Howard Karloff and Noam Nisan  “Algebraic methods for interactive proof systems”  In _Journal of the ACM (JACM)_ 39.4 ACM New York, NY, USA, 1992, pp. 859–868
  * [LMM+22] Shachar Lovett et al.  “Lifting with Sunflowers”  In _13th Innovations in Theoretical Computer Science Conference (ITCS 2022)_ , 2022
  * [MP20] Moritz Müller and Ján Pich  “Feasibly constructive proofs of succinct weak circuit lower bounds”  In _Annals of Pure and Applied Logic_ 171.2 Elsevier, 2020, pp. 102735
  * [NW94] Noam Nisan and Avi Wigderson  “Hardness vs randomness”  In _Journal of Computer and System Sciences_ 49.2 Elsevier, 1994, pp. 149–167
  * [PBI93] Toniann Pitassi, Paul Beame and Russell Impagliazzo  “Exponential lower bounds for the pigeonhole principle”  In _Computational complexity_ 3 Springer, 1993, pp. 97–140
  * [Pic15] Ján Pich  “Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic”  In _Logical Methods in Computer Science_ 11 Episciences, 2015
  * [Pra75] Vaughan R Pratt  “Every prime has a succinct certificate”  In _SIAM Journal on Computing_ 4.3 SIAM, 1975, pp. 214–220
  * [PS23] Jan Pich and Rahul Santhanam  “Towards $\mathbf{P}\neq\NP$ from Extended Frege lower bounds”  In _arXiv preprint arXiv:2312.08163_ , 2023
  * [Pud20] Pavel Pudlák  “Reflection principles, propositional proof systems, and theories”, 2020  arXiv:2007.14835
  * [Pud97] Pavel Pudlák  “Lower bounds for resolution and cutting planes proofs and monotone computations”  In _The Journal of Symbolic Logic_ 62.3 Cambridge University Press, 1997, pp. 981–998
  * [Raz85] Alexander Razborov  “Lower bounds on the monotone complexity of some Boolean function”  In _Soviet Math. Dokl._ 31, 1985, pp. 354–357
  * [Raz87] Alexander A. Razborov  “Lower bounds on the size of bounded depth circuits over a complete basis with logical addition”  In _Mathematical Notes of the Academy of Sciences of the USSR_ 41.4 Springer, 1987, pp. 333–338
  * [Raz95] Alexander Razborov  “Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic”  In _Izvestiya: mathematics_ 59.1, 1995, pp. 205
  * [Raz95a] Alexander A Razborov  “Bounded arithmetic and lower bounds in Boolean complexity”  In _Feasible Mathematics II_ Springer, 1995, pp. 344–386
  * [RM97] Ran Raz and Pierre McKenzie  “Separation of the monotone $\NC$ hierarchy”  In _Proceedings 38th Annual Symposium on Foundations of Computer Science (FOCS)_ , 1997, pp. 234–243  IEEE
  * [Smo87] Roman Smolensky  “Algebraic methods in the theory of lower bounds for Boolean circuit complexity”  In _Proceedings of the Nineteenth Annual ACM Symposium on the Theory of Computing_ , 1987, pp. 77–82