Provably Total Functions in the Polynomial Hierarchy

Fleming, Noah; Imrek, Deniz; Marciot, Christophe

doi:10.4230/LIPIcs.CCC.2025.28

Provably Total Functions in the Polynomial Hierarchy

Noah Fleming

Memorial University of Newfoundland, St. John’s, Canada Deniz Imrek

University of Texas at Austin, TX, USA Christophe Marciot

Memorial University of Newfoundland, St. John’s, Canada

Abstract

${\mathsf{TFNP}}$ studies the complexity of total, verifiable search problems, and represents the first layer of the total function polynomial hierarchy ( ${\mathsf{TFPH}}$ ). Recently, problems in higher levels of the ${\mathsf{TFPH}}$ have gained significant attention, partly due to their close connection to circuit lower bounds. However, very little is known about the relationships between problems in levels of the hierarchy beyond ${\mathsf{TFNP}}$ .
Connections to proof complexity have had an outsized impact on our understanding of the relationships between subclasses of ${\mathsf{TFNP}}$ in the black-box model. Subclasses are characterized by provability in certain proof systems, which has allowed for tools from proof complexity to be applied in order to separate ${\mathsf{TFNP}}$ problems. In this work we begin a systematic study of the relationship between subclasses of total search problems in the polynomial hierarchy and proof systems. We show that, akin to ${\mathsf{TFNP}}$ , reductions to a problem in ${\mathsf{TF}}\Sigma_{d}$ are equivalent to proofs of the formulas expressing the totality of the problems in some $\Sigma_{d}$ -proof system. Having established this general correspondence, we examine important subclasses of ${\mathsf{TFPH}}$ . We show that reductions to the StrongAvoid problem are equivalent to proofs in a $\Sigma_{2}$ -variant of the (unary) Sherali-Adams proof system. As well, we explore the ${\mathsf{TFPH}}$ classes which result from well-studied proof systems, introducing a number of new ${\mathsf{TF}}\Sigma_{2}$ classes which characterize variants of DNF resolution, as well as ${\mathsf{TF}}\Sigma_{d}$ classes capturing levels of $\Sigma_{d}$ -bounded-depth Frege.

Keywords and phrases:

TFNP, TFPH, Proof Complxity, Characterizations

Funding:

Noah Fleming: Supported by NSERC.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Proof complexity ; Theory of computation

\rightarrow

Complexity classes

Acknowledgements:

The authors thank Robert Robere, Toniann Pitassi, and Oliver Korten for helpful discussions.

DOI:

10.4230/LIPIcs.CCC.2025.28

Event:

40th Computational Complexity Conference (CCC 2025)

Editors:

Srikanth Srinivasan

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

The class ${\mathsf{TFNP}}$ consists of the total search problems whose solutions are verifiable in polynomial time. It has received considerable attention since it captures fundamental problems in a broad range of areas whose lack of efficient algorithms is not readily explained by the theory of ${\mathsf{NP}}$ -completeness. Famous examples include Nash: output a Nash equilibria of a given bimatrix game; and Factoring: output a prime divisor of a given integer. ${\mathsf{TFNP}}$ itself is not believed to admit complete problems [21], and as a consequence much of the work on ${\mathsf{TFNP}}$ has focused on studying subclasses which do. However, we are limited to proving conditional or oracle separations, as a separation between any ${\mathsf{TFNP}}$ subclasses would imply ${\mathsf{P}}\neq{\mathsf{NP}}$ .

A flurry of recent results have established a complete picture of the relationships between the major ${\mathsf{TFNP}}$ subclasses in the black-box setting, where the input is presented as a black-box oracle which can be queried [2, 12, 11, 9, 13]. These results exploited a deep connection between black-box ${\mathsf{TFNP}}$ – denoted ${\mathsf{TFNP}}^{dt}$ – and proof complexity, an area which studies efficient provability in certain propositional logics, known as proof systems. The connection of proof complexity to ${\mathsf{TFNP}}^{dt}$ can be summarized as follows: A reduction between two total search problems is a proof that the first is total, assuming the totality of the second. By employing this lens, it has been shown that many important ${\mathsf{TFNP}}^{dt}$ subclasses are characterized by provability in certain well-studied proof systems in the sense that there is a simple proof of the totality of a search problem if and only if there is an efficient reduction of that search problem to the complete problem for that subclass [13, 12, 5, 19, 8]. This connection has been highly impactful for the study of ${\mathsf{TFNP}}^{dt}$ , allowing for the rich set of tools in proof complexity to be leveraged in order to provide separations between the major ${\mathsf{TFNP}}^{dt}$ subclasses.

${\mathsf{TFNP}}={\mathsf{TF}}\Sigma_{1}$ is the first level of the total function polynomial hierarchy ${\mathsf{TFPH}}=\bigcup_{i}{\mathsf{TF}}\Sigma_{i}$ [14]. Recently, problems in higher levels of the polynomial hierarchy have received considerable attention, in part due to their close connection to circuit lower bounds. Indeed, consider the task of finding (the truth table of) a function which does not have circuits of size $s$ . Using a standard encoding, any circuit of size $s$ can be represented uniquely by $k=\textup{poly}(s)$ -many bits. Consider the map $T:\{0,1\}^{k}\rightarrow\{0,1\}^{n}$ which maps circuits of size $s$ to truth tables of the function that they compute. Finding a truth table of a function with high circuit complexity is equivalent to finding a string which is not in the range of $T$ . This is an instance of the RangeAvoidance problem.

Definition 1.

RangeAvoidance (or simply Avoid) is the following search problem: Given a function $f:\{0,1\}^{n}\rightarrow\{0,1\}^{n+1}$ , find a $y\in\{0,1\}^{n+1}$ such that for all $x$ , $f(x)\neq y$ .

Observe that any solution $y$ to Avoid can be checked by a ${\mathsf{coNP}}$ verifier – check that for every $x\in\{0,1\}^{n}$ , $f(x)\neq y$ . This means that Avoid belongs to the class ${\mathsf{TF}}\Sigma_{2}$ . If there is an algorithm for solving Avoid which belongs to a class $\cal C$ then this implies the existence of a function in $\cal C$ which does not have small circuits – a circuit lower bound against $\cal C$ ! This approach led to the recent breakthrough circuit lower bounds against symmetric exponential time [20, 7, 17]. Hence, understanding the complexity of ${\mathsf{TF}}\Sigma_{2}$ is important for understanding circuit lower bounds. Indeed, the current best upper bound puts Avoid in the class of problems reducible to LOP – the ${\mathsf{TF}}\Sigma_{2}$ problem of finding a minimum element in a total order.

${\mathsf{TF}}\Sigma_{2}$ contains numerous important problems beyond those connected to circuit lower bounds. For example, Avoid is the complete problem for the class ${\mathsf{APEPP}}$ which also captures the complexity of finding pseudo-random number generators, randomness extractors, and rigid matrices [16]. We can restrict Avoid to only have one more element in its range than in its domain to obtain the problem StrongAvoid.

Definition 2.

strongRangeAvoidance (or simply StrongAvoid) is the following search problem: Given a function $f:\{0,1\}^{n}\setminus\{0\}\rightarrow\{0,1\}^{n}$ , find an empty hole $y\in\{0,1\}^{n}$ , i.e., such that for all $x\in\{0,1\}^{n}\setminus\{0\}$ , $f(x)\neq y$ .

StrongAvoid is the complete problem for the class ${\mathsf{PEPP}}$ which captures the complexity of finding objects whose existence is guaranteed by the union bound, including all of ${\mathsf{APEPP}}$ [14]. Important problems have also been identified in higher levels of the polynomial hierarchy, such as those related to finding sets of large VC dimension [14].

Despite the importance of problems in levels of the polynomial hierarchy beyond ${\mathsf{TFNP}}$ , there has been little structural exploration into how they relate. Indeed, [17] provide the first black-box separation, showing that StrongAvoid is not reducible to any problem in ${\mathsf{TF}}\Sigma_{2}$ with a unique solution (in fact, they show that it cannot be solved with non-adaptive oracle calls to any language in $\Sigma_{2}^{P}$ ). Proof complexity has had an outsized impact on proving black-box separations for ${\mathsf{TFNP}}$ . To facilitate further structural exploration of ${\mathsf{TFPH}}$ , we would like to explore to what degree proof complexity tools can be used to provide separations between classes within higher levels of the black-box total function polynomial hierarchy (denoted ${\mathsf{TFPH}}^{dt}$ ).

Our Results

Figure 1: Relationships and characterizations of

{\mathsf{TF}}\Sigma_{2}

classes studied. An arrow indicates containment.

In this paper we begin a systematic study of the connections between the total function polynomial hierarchy in the black-box model and propositional proof complexity. First, we identify the form that proof systems which characterize ${\mathsf{TF}}\Sigma_{d}^{dt}$ subclasses take. In order to characterize ${\mathsf{TF}}\Sigma_{d}$ subclasses, these proof systems must be able to prove the validity of depth- $(d+1)$ propositional formulas. However, they cannot be Cook-Reckhow proof systems ( ${\mathsf{NP}}$ -verifiers) in general unless ${\mathsf{NP}}={\mathsf{coNP}}$ as there are syntactic subclasses of ${\mathsf{TF}}\Sigma_{2}^{dt}$ which contain all of ${\mathsf{TFNP}}^{dt}$ ; a characterization of which would imply a polynomialy-bounded proof system. Recall that a class is syntactic if it admits a complete problem. We show that in order to characterize ${\mathsf{TF}}\Sigma_{d}^{dt}$ subclasses, it suffices to augment Cook-Reckhow proof systems $P$ with a $\Sigma_{d}$ -weakening rule which generalizes the resolution weakening rule to $\Sigma_{d}$ formulas; we call the resulting proof system $\Sigma_{d}$ - $P$ (see Definition 14).

To begin, we explore the limits of these characterizations, verifying that this is indeed the correct definition of a proof system for ${\mathsf{TF}}\Sigma_{d}^{dt}$ . A syntactic class ${\cal C}\subseteq{\mathsf{TF}}\Sigma_{d}^{dt}$ is uniform is there is a polynomial-time algorithm which given $n$ outputs the $n^{th}$ instance of the complete problem for ${\cal C}$ .

Theorem 3 (Informal).

The following hold:

1.

For every uniform ${\cal C}\subseteq{\mathsf{TF}}\Sigma_{d}^{dt}$ there is a $\Sigma_{d}$ -proof system $P$ such that $R\in{\cal C}$ if and only if $P$ efficiently proves that $R$ is total.
2.

For every well-behaved $\Sigma_{d}$ -proof system $P$ there is a uniform ${\mathsf{TF}}\Sigma_{d}^{dt}$ subclass ${\cal C}$ such that $R\in{\cal C}$ if and only if $P$ proves that $R$ is total.

Having established this scaffolding result, we begin to explore characterizations of specific ${\mathsf{TF}}\Sigma_{d}^{dt}$ subclasses; our results for ${\mathsf{TF}}\Sigma_{2}$ can be seen in Figure 1. First, we show that ${\mathsf{PEPP}}^{dt}$ is characterized by the $\Sigma_{2}$ -variant of the Sherali-Adams proof system.

Theorem 4 (Informal).

$R\in{\mathsf{PEPP}}^{dt}$ iff there is an efficient $\Sigma_{2}$ -Sherali-Adams proof that $R$ is total.

This allows one to use an extension to the pseudo-expectation technique in order to exclude total search problems from ${\mathsf{PEPP}}$ , and hence also ${\mathsf{APEPP}}$ . Currently, no such exclusions are known.

We also consider several variants of the DNF-resolution proof system: DNF Resolution ( ${\mathsf{Res}}({\mathsf{polylog}})$ ), Circular DNF resolution ( ${\mathsf{uCircRes}}({\mathsf{polylog}})$ ), and Reversible DNF resolution ( ${\mathsf{RevRes}}({\mathsf{polylog}})$ ). We introduce new ${\mathsf{TF}}\Sigma_{2}^{dt}$ classes which characterize them.

Theorem 5 (Informal).

$\Sigma_{2}$ - ${\mathsf{Res}}({\mathsf{polylog}})$ , $\Sigma_{2}$ - ${\mathsf{uCircRes}}({\mathsf{polylog}})$ , $\Sigma_{2}$ - ${\mathsf{RevRes}}({\mathsf{polylog}})$ are characterized by the ${\mathsf{TF}}\Sigma_{2}^{dt}$ subclasses ${\mathsf{PLS}}_{2}$ , ${\text{SoL}}_{2}$ , ${\text{SoPL}}_{2}$ , respectively.

We explore how these new classes relate to natural ${\mathsf{TF}}\Sigma_{2}$ classes, which can be seen in Figure 1. In doing so, we introduce a natural ${\mathsf{TF}}\Sigma_{2}$ class ${\mathsf{SOD}}$ , of problems reducible to finding a source in a DAG given a sink, which we believe may be of independent interest.

Finally, we show that our characterization of DNF resolution can be extended to characterize bounded-depth Frege in higher levels of ${\mathsf{TFPH}}$ . The depth- $d$ Frege system allows one to cut on depth- $d$ propositional formulas.

Theorem 6 (informal).

$\Sigma_{d}$ -Depth $d$ -Frege is characterized by the ${\mathsf{TF}}\Sigma_{d}^{dt}$ class ${\mathsf{PLS}}_{d}^{dt}$ .

This result is inspired by the work of Beckmann and Buss, who characterize ${\text{PE}}_{d}$ and ${\mathsf{GI}}_{d}$ in bounded arithmetic [23]. It is also the ${\mathsf{TF}}\Sigma_{d}$ analogue of Thapen’s recent ${\mathsf{TFNP}}$ characterization of bounded-depth Frege [25].

Comparison with Bounded Arithmetic.

Characterizations of ${\mathsf{TFPH}}$ classes have been studied in the uniform setting by theories of bounded arithmetic. Beckmann and Buss [3] showed that $\Sigma^{b}_{d}$ -definable functions of $T^{d}_{2}$ correspond to the class ${\mathsf{PLS}}^{\Sigma^{p}_{d-1}}$ , which is defined by replacing the polynomial-time predicates and functions of the complete problem for the ${\mathsf{TFNP}}$ subclass ${\mathsf{PLS}}$ with predicates and functions from ${\mathsf{P}}^{\Sigma^{p}_{d-1}}$ . This results in the generalized polynomial local search problem ${\text{GPLS}}_{d}$ of [23]. However, these correspondences do not stray outside of proof systems which correspond to bounded-depth Frege systems.

Comparison with [25].

Recently and independently, Thapen [25] considered reductions between black-box total search problems in the polynomial hierarchy under the notion of counter example reducibility, in order to define new ${\mathsf{TFNP}}$ subclasses. Taking the set of ${\mathsf{TFNP}}$ problems which are counter-example reducible to a ${\mathsf{TF}}\Sigma_{2}$ problem, characterizing a class $C\subseteq{\mathsf{TF}}\Sigma_{2}$ , essentially acts as a projection of $C$ to ${\mathsf{TFNP}}$ . He uses these in order to obtain ${\mathsf{TFNP}}^{dt}$ characterizations. In comparison, we are interested in reductions between and characterizations of ${\mathsf{TF}}\Sigma_{d}^{dt}$ problems. As well, he shows that versions of the game induction problems $\mathsf{GI}_{d}$ [24] form ${\mathsf{TFNP}}^{dt}$ subclasses which characterize bounded-depth Frege proofs of CNF formulas.

Open Problems.

In this paper we provide the framework for characterizations between total search problems in the polynomial hierarchy, leaving open many natural questions.

1.

We study decision-tree reductions, as these are the query analogue of polynomial-time reductions. However, it is natural also to consider more powerful reductions, such as ${\mathsf{P}}^{{\mathsf{NP}}}$ -reductions. What characterizations does one obtain under such reductions?
2.

There are several studied classes for which we do not yet have characterizations, such as ${\mathsf{APEPP}}$ and LOP. Due to the connection between StrongAvoid and Sherali-Adams, it would appear that ${\mathsf{PEPP}}$ should correspond to a variant of Sherali-Adams which produces a large negative value, rather than $-1$ . However, we cannot maintain this under decision-tree reductions.
3.

${\mathsf{TF}}\Sigma_{2}$ problems with unique solutions play a critical role in the recent circuit lower bounds [20, 7, 17]. What properties do proof systems which characterize such problems possess?

2 Preliminaries on the Total Function Polynomial Hierarchy

Subclasses of ${\mathsf{TFPH}}$ are typically defined by a simple existence principle to which everything in the class reduces. For example, any total order must have a minimal element. These existence principles naturally give rise to total search problems. Continuing the example:

Definition 7.

The Linear Ordering Principle (LOP) asks, given $\prec:\{0,1\}^{n}\times\{0,1\}^{n}\rightarrow\{0,1\}$ , to find:

$\blacksquare$

A minimal element: $x\in\{0,1\}^{n}$ such that $\forall y\neq x$ , $x\prec y$ .
$\blacksquare$

A violation of the total order: either (i) $x\in\{0,1\}^{n}$ such that $x\prec x$ , (ii) $x\neq y$ such that $x\not\prec y$ and $y\not\prec x$ , or (iii) $x\prec y$ and $y\prec z$ and $x\not\prec z$ .

To make these problems non-trivial, the input is presented as a circuit $C$ so that the search space is exponential in the number of input bits $n$ . Formally, for any $x,y\in\{0,1\}^{n}$ , $C(x,y)=\prec(x,y)$ . We call $C$ a white-box encoding of the problem. Unfortunately, a separation between any pair of total search problems in the white-box model is hard to achieve, as it would imply ${\mathsf{P}}\neq{\mathsf{NP}}$ .

Instead, we can gain intuition for the relationships between these classes by exploring their black-box variants. In this setting $C$ is given as an oracle which can be queried, but we no longer have access to the description of $C$ . A major benefit of considering the black-box model is that we can now prove unconditional separations between classes without having to resolve ${\mathsf{P}}$ versus ${\mathsf{NP}}$ . These separations imply oracle separation in the white-box setting.

A query search problem is a sequence of relations $R_{n}\subseteq\{0,1\}^{n}\times{\cal O}_{n}$ , one for each $n\in\mathbb{N}$ . It is total if for every $x\in\{0,1\}^{n}$ there is an $o\in{\cal O}_{n}$ such that $(x,o)\in R_{n}$ . We think of $x\in\{0,1\}^{n}$ as a bit string which can be accessed by querying individual bits, and we will measure the complexity of solving $R_{n}$ as the number of bits that must be queried. Hence, an efficient algorithm for $R_{n}$ will be one which finds a suitable $o$ while making at most ${\mathsf{polylog}}(n)$ -many queries to the input. We will not charge the algorithm for other computational steps, and therefore an efficient algorithm corresponds to a shallow decision tree. Total query search problems which can be computed by decision trees of depth ${\mathsf{polylog}}(n)$ belong to the class ${\mathsf{FP}}^{dt}$ , where $d t$ indicates that it is a black-box class. While search problems are formally defined as sequences $R=(R_{n})$ , we will often want to speak about individual elements in the sequence. For readability, we will abuse notation and refer to elements $R_{n}$ in the sequence as total search problems; furthermore, we will often drop the subscript $n$ , and rely on context to differentiate.

In this paper we will be considering total query search problems in the polynomial hierarchy ${\mathsf{TFPH}}^{dt}$ .

Definition 8.

We say that a total search problem $R=(R_{n})$ , where $R_{n}\subseteq\{0,1\}^{n}\times{\cal O}_{n}$ , belongs to the $d^{th}$ level of the query total function polynomial hierarchy ${\mathsf{TF}}\Sigma_{d}^{dt}$ if for every $o\in{\cal O}_{n}$

(x,o)\in R\iff\forall z_{1}\in\{0,1\}^{\ell_{1}}\leavevmode\nobreak\ \exists z% _{2}\in\{0,1\}^{\ell_{2}}\leavevmode\nobreak\ \ldots Qz_{d-1}\in\{0,1\}^{\ell_% {d-1}}\leavevmode\nobreak\ V_{o,(z_{1},\ldots,z_{d-1})}(x)=1,

where $Q\in\{\exists,\forall\}$ , $V_{o,\vec{z}}=V_{o,(z_{1},\ldots,z_{d-1})}$ is a decision tree of ${\mathsf{polylog}}(n)$ -depth, and each $\ell_{i}\in{\mathsf{polylog}}(n)$ .

Note that ${\mathsf{FP}}^{dt}={\mathsf{TF}}\Sigma_{0}^{dt}$ and ${\mathsf{TFNP}}={\mathsf{TF}}\Sigma_{1}^{dt}$ . At this point one may ask about ${\mathsf{TF}}\Pi_{d}^{dt}$ . Kleinberg et al. [14] showed that ${\mathsf{TF}}\Pi_{d}$ is efficiently reducible to ${\mathsf{TF}}\Sigma_{d-1}$ , and vice versa. Hence, it does not offer a new perspective.

We can compare the complexity of total search problems by taking reductions between them. The following defines decision tree reductions between total search problems, the query analogue of polynomial-time reductions.

Definition 9.

For total search problems $R\subseteq\{0,1\}^{n}\times{\cal O}_{n},S\subseteq\{0,1\}^{m}\times{\cal O}_{m% }^{\prime}$ , there is an $S$ -formulation of $R$ if, for every $i\in[m]$ and $o\in{\cal O^{\prime}}_{m}$ , there are functions $f_{i}:\{0,1\}^{n}\rightarrow\{0,1\}$ and $g_{o}:\{0,1\}^{n}\rightarrow{\cal O}_{n}$ such that

(f(x),o)\in S\implies(x,g_{o}(x))\in R,

where $f(x)=(f_{1}(x)\ldots f_{n}(x))$ . The depth of the reduction is

d\leavevmode\nobreak\ :=\leavevmode\nobreak\ \max\big{(}\{0pt(f_{i}):i\in[m]\}% \cup\{0pt(g_{o}):o\in{\cal O}_{m}^{\prime}\}\big{)},

where $0pt(f)$ denotes the minimum depth of any decision tree which computes $f$ . The size of the reduction is $m$ , the number of input bits to $S$ . The complexity of the reduction is $\log m+d$ , and the complexity of reducing $R$ to $S$ is the minimum $S$ -formulation of $R$ .

We extend this definition to sequences in the natural way. If $S=(S_{n})$ is a sequence and $R_{n}$ is a single search problem, then the complexity of reducing $R_{n}$ to $S$ is the minimum over $m$ of the complexity of reducing $R_{n}$ to $S_{m}$ . For two sequences of search problems $S=(S_{n})$ and $R=(R_{n})$ , the complexity of reducing $R$ to $S$ is the complexity of reducing $R_{n}$ to $S$ for each $n$ . A reduction from $R$ to $S$ is efficient if its complexity is ${\mathsf{polylog}}(n)$ ; we denote this by $R\leq_{dt}S$ .

Syntactic and Uniform Classes.

We say that a class of total search problems ${\cal C}\subseteq{\mathsf{TF}}\Sigma_{d}^{dt}$ has $R\in{\cal C}$ as its complete problem if for every $S\in{\cal C}$ , $S\leq_{dt}R$ . We call subclasses with complete problems syntactic. Further, we say that a syntactic class is uniform if it has a complete problem $R$ which is uniformly generated – - there is a polynomial-time Turing machine which on input $n$ outputs the $n^{th}$ instance of a complete problem for that class.

3 Proof Systems for TFPH

Search problems in the black-box model are intimately tied to the complexity of propositional theorem proving. A proof is a procedure for convincing a verifier that a statement is correct. In the propositional setting, a proof convinces the verifier that a propositional formula is unsatisfiable (equivalently, its negation is a tautology).

3.1 Recap: Proof Systems for TFNP

We begin by recalling how characterizations of proof systems by ${\mathsf{TFNP}}^{dt}$ subclasses occur. We will then generalize this to ${\mathsf{TFPH}}$ . Let $\mathsf{UNSAT}$ be the language of all unsatisfiable propositional formulas.

Definition 10.

A Cook-Reckhow proof system is a polynomial-time function $P:\{0,1\}^{*}\rightarrow\{0,1\}$ such that for every propositional formula $F\in\{0,1\}^{*}$ ,

F\in\mathsf{UNSAT}\iff\exists\Pi\in\{0,1\}^{*},P(\Pi,F)=1.

The size of proving an unsatisfiable formula $F$ in $P$ is $\min\{|\Pi|:P(\Pi,F)=1\}$ .

For many proof systems there is an associated width/degree measure. For example, in resolution it is the maximum number of literals in any clause appearing in a proof, and in algebraic systems such as Sherali-Adams and Sum-of-Squares it is the maximum degree of the polynomials appearing in the proof. Characterizations of ${\mathsf{TFNP}}^{dt}$ subclasses are in terms of a complexity parameter of the proof system, denoted

P(F)\leavevmode\nobreak\ :=\leavevmode\nobreak\ \min\big{\{}\mathsf{width}(\Pi% )+\log\mathsf{size}(\Pi):\Pi\mbox{ is a $P$-proof of $F$}\big{\}},

where $\mathsf{width}$ is some associated width measure particular to that system. For example, for example for resolution the width measure is the number of literals in a clause, while for algebraic proof systems the width measure is typically the proof degree. This complexity measure is studied in order to account for the fact that in the black-box setting our reductions are performed by decision trees and we would like the complexity of a proof to be closely related to the complexity of a formulation; width will correspond to the depth of the decision trees in the formulation.

Typically one studies the complexity of proving the unsatisfiability of CNF formulas. As a CNF formula $F=C_{1}\wedge\ldots\wedge C_{m}$ is falsified only when one of its clauses is falsified, a proof convinces the verifier that for every assignment $x\in\{0,1\}^{n}$ there is some clause $C_{i}$ of $F$ such that $C_{i}(x)=0$ . Hence, the complexity of proving that $F$ is unsatisfiable is intimately related to the complexity of exhibiting a falsified clause, given an assignment. This is known as the false clause search problem ${\text{Search}}_{F}\subseteq\{0,1\}^{n}\times[m]$ , defined as

(x,i)\in{\text{Search}}_{F}\iff C_{i}(x)=0.

As $F$ is unsatisfiable, this search problem is total, and if each clause of $F$ contains at most ${\mathsf{polylog}}(n)$ -many variables, it belongs to ${\mathsf{TFNP}}^{dt}$ .

The above intuition suggests that understanding ${\mathsf{TFNP}}^{dt}$ (or at least the false clause search problem) is important for understanding proof complexity. Remarkably, proof complexity is also crucial for understanding ${\mathsf{TFNP}}^{dt}$ . It turns out that ${\mathsf{TFNP}}^{dt}$ is equivalent to a large sub-area of proof complexity! The intuition is the following: A reduction between two total search problems is a proof that the first is total, assuming the totality of the second. By employing this lens, works have shown that many common proof systems are characterized by certain well-studied tautologies in the sense that they can prove a tautology iff there is a short reduction of that tautology to the characterizing one.

The heart of this connection is the following claim, which shows that ${\mathsf{TFNP}}^{dt}$ is exactly the study of the false clause search problem. The proof proceeds by expressing the totality of any problem $R$ in ${\mathsf{TFNP}}^{dt}$ as a tautology and then taking its negation.

Claim 11.

If $R\in{\mathsf{TFNP}}^{dt}$ then there is an unsatisfiable ${\mathsf{polylog}}(n)$ -width CNF formula $F_{R}$ such that ${\text{Search}}_{F_{R}}\in{\mathsf{TFNP}}^{dt}$ and $R=_{dt}{\text{Search}}_{F_{R}}$ .

From this, characterizations of ${\mathsf{TFNP}}^{dt}$ subclasses by proof systems have been derived. We say that a syntactic subclass ${\cal C}\subseteq{\mathsf{TFNP}}^{dt}$ is characterized by a proof system $P$ if for every ${\text{Search}}_{F}\in{\mathsf{TFNP}}^{dt}$ , ${\text{Search}}_{F}\in{\cal C}$ iff $P(F)={\mathsf{polylog}}(n)$ . Note that as a proof system is a polynomial-time Turing machine, any ${\mathsf{TFNP}}^{dt}$ class must be which characterizes that proof system must be uniform.

3.2 Proof Systems and TFPH

The aim of this paper is to explore characterizations of classes of problems belonging to higher levels of ${\mathsf{TFPH}}^{dt}$ . These will correspond to the provability of quantified formulas.

Definition 12.

A $\Sigma_{d.5}$ formula $F$ is the propositional translation of any quantified formula of the form

\exists z_{1}\in\{0,1\}^{\ell_{1}}\leavevmode\nobreak\ \forall z_{2}\in\{0,1\}% ^{\ell_{2}}\ldots Qz_{d}\in\{0,1\}^{\ell_{d}}\leavevmode\nobreak\ L(x,z_{1},% \ldots,z_{d}),

where $\ell_{i}\in{\mathsf{polylog}}(n)$ , $Q\in\{\exists,\forall\}$ , and $L$ is a formula which depends on at most ${\mathsf{polylog}}(n)$ -many free variables ( $x$ ). That is, a $\Sigma_{d.5}$ formula is of the form

F(x)=\bigvee_{z_{1}\in\{0,1\}^{\ell_{1}}}\bigwedge_{z_{2}\in\{0,1\}^{\ell_{2}}% }\ldots\underset{z_{d}\in\{0,1\}^{\ell_{d}}}{\bigcirc}L_{z_{1},\ldots,z_{d}}(x),

where $\bigcirc\in\{\wedge,\lor\}$ , and $L_{z_{1},\ldots,z_{d}}(x):=L(x,z_{1},\ldots,z_{d})$ . Similarly, $\Pi_{d.5}$ formulas are negations of $\Sigma_{d.5}$ formulas.

Note that because $L_{z}$ depends on ${\mathsf{polylog}}(n)$ -many variables, we may assume without loss of generality (with a quasi-polynomial blow-up in size) that $L_{z}$ is a CNF/DNF formula with clauses/terms of width ${\mathsf{polylog}}(n)$ . Hence, a $\Sigma_{d.5}$ -formula is a layered circuit of depth $d$ where the gates at each layer are the same, and the gates at the first $d$ layers are allowed $2^{{\mathsf{polylog}}(n)}$ fanin, while the final layer is restricted to have ${\mathsf{polylog}}(n)$ fanin. Observe that a $\Pi_{1.5}$ -formula is a low-width CNF formula.

Our aim is to characterize subclasses of the higher levels of the total function polynomial hierarchy. Towards this, we generalize the false clause search problem to $\Sigma_{d.5}$ formulas.

False Formula Search.

For a formula $F:=\bigwedge_{o\in[m]}H_{o}$ where each $H_{o}$ is a $\Sigma_{d.5}$ -formula, the False Formula search problem ${\text{FF}}_{F}\subseteq\{0,1\}^{n}\times[m]$ is defined as

(x,o)\in{\text{FF}}_{F}\iff H_{o}(x)=0.

Observe that if $F$ is unsatisfiable then ${\text{FF}}_{F}$ is total and ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{d+1}^{dt}$ . The following lemma generalizes Claim 11 to say that ${\mathsf{TF}}\Sigma_{d}^{dt}$ is exactly the study of the false formula search problem.

Lemma 13.

For every $d\geq 1$ and $R\in{\mathsf{TF}}\Sigma_{d}$ there is an unsatisfiable $\Pi_{d.5}$ -formula $F_{R}$ such that $(x,o)\in R$ iff $(x,o)\in{\text{FF}}_{F_{R}}$ .

Proof.

Let $R\subseteq\{0,1\}^{n}\times[m]\in{\mathsf{TF}}\Sigma_{d}$ . Then there are ${\mathsf{polylog}}(n)$ -depth decision trees $V_{o,(z_{1},\ldots,z_{d-1})}$ such that

(x,o)\in R\iff\forall z_{1}\in\{0,1\}^{\ell_{1}}\leavevmode\nobreak\ \exists z% _{2}\in\{0,1\}^{\ell_{2}}\leavevmode\nobreak\ \ldots Qz_{d-1}\in\{0,1\}^{\ell_% {d-1}}\leavevmode\nobreak\ V_{o,(z_{1},\ldots,z_{d-1})}(x)=1,

where $Q\in\{\exists,\forall\}$ , $V_{o,\vec{z}}=V_{o,(z_{1},\ldots,z_{i-1})}$ is a decision tree of ${\mathsf{polylog}}(n)$ -depth, and each $\ell_{j}\in{\mathsf{polylog}}(n)$ . Slightly abusing notation, let $V_{o}$ be a propositional translation of the verifier as a $\Pi_{(d-1).5}$ -formula:

V_{o}(x):=\bigwedge_{z_{1}\in\{0,1\}^{\ell_{1}}}\bigvee_{z_{2}\in\{0,1\}^{\ell% _{2}}}\ldots\underset{z_{d-1}\in\{0,1\}^{\ell_{d-1}}}{\bigcirc}V_{o,\vec{z}}(x),

where $\bigcirc\in\{\wedge,\lor\}$ , and $V_{o,\vec{z}}(x)$ is computable by a ${\mathsf{polylog}}(n)$ -depth decision tree, and hence propositionalized as a ${\mathsf{polylog}}(n)$ -width CNF formula if $\bigcirc=\wedge$ or a ${\mathsf{polylog}}(n)$ -width DNF if $\bigcirc=\lor$ , collapsing the top gate into $\bigcirc$ . This is done as follows: Say that a root-to-leaf path in $V_{o,\vec{z}}$ is a $b$ -path if it ends at a leaf labeled $b\in\{0,1\}$ . Then, $V_{o,\vec{z}}$ is propositionalized as

$\blacksquare$

If $d-1$ is even: $\bigvee_{\text{\scriptsize 1\mbox{-path }}p\in V_{o,\vec{z}}}p$ ,
$\blacksquare$

If $d-1$ is odd: $\bigwedge_{0\text{\scriptsize\mbox{-path }}p\in V_{o,\vec{z}}}\neg p$ ,

where $p$ is the conjunction of literals queried along $p$ (if a variable $x$ is queried and we take branch- $0$ , then we consider this as literal $\neg x$ and otherwise as $x$ ). Note that in this case the outer gate of $V_{o,\vec{z}}$ matches $\bigcirc$ , and the depth collapses by $1$ . Consider the following $\Pi_{d.5}$ -formula, which states that $R$ is not total:

F(x):=\bigwedge_{o\in{\cal O}}\neg V_{o}(x).

Observe that if $(x,o)\in R$ , then there is some $z_{1},\ldots,z_{d}$ such that $V_{o,z}(x)=1$ , and hence $(x,o)\in{\text{FF}}_{F}$ . Conversely, if $(x,o)\in{\text{FF}}_{F}$ , then $(x,o)\in R$ . $\hfill\blacktriangleleft$

We will call the formula $F_{R}$ the propositionalization of $R$ . This lemma allows us to relate the complexity of total search problems to the provability of propositional formulas. In the remainder we will develop what provability means in this context. In particular, what are the properties of a proof system which proves the formulas that result from ${\mathsf{TFPH}}^{dt}$ search problems.

A characterization of a ${\mathsf{TFPH}}^{dt}$ class by a proof system proceeds by showing that the proof system can prove the correctness of reductions to the class. To discuss this, we will need to propositionalize reductions.

Reduced Formula.

Let $R\subseteq\{0,1\}^{n}\times{\cal O}$ be a problem in ${\mathsf{TF}}\Sigma_{d}^{dt}$ and let $V_{\vec{z},o}$ , $o\in{\cal O}$ be its verifiers. Let $(f,g)$ be an $R$ -formulation where $f:\{0,1\}^{m}\rightarrow\{0,1\}^{n}$ , $g:\{0,1\}^{m}\rightarrow{\cal O}$ , then the reduced formula $F_{R}(f,g)$ is the $\Pi_{d.5}$ -formula defined as

\displaystyle F_{R}(f,g)\leavevmode\nobreak\ :=\leavevmode\nobreak\ \bigwedge_% {o\in{\cal O}}\bigwedge_{\mbox{path }p\in g_{o}}\neg V_{o,p}(f(x)),

where $V_{o,p}(f(x))=\bigwedge_{z_{1}\in\{0,1\}^{\ell_{1}}}\bigvee_{z_{2}\in\{0,1\}^{% \ell_{2}}}\ldots\bigcirc_{z_{d-1}\in\{0,1\}^{\ell_{d-1}}}(V_{o,\vec{z}}(f(x))% \wedge p)$ and $V_{o,\vec{z}}(f(x))$ can be represented as a ${\mathsf{polylog}}(n)$ -width CNF/DNF as in Lemma 13, using that both $V_{o,\vec{z}}$ and $f$ are computable by ${\mathsf{polylog}}(n)$ -depth decision trees.

Reduced formulas capture formulations in the following sense. Let $H\leavevmode\nobreak\ :=\bigwedge_{o\in{\cal O}_{H}}H_{o}$ and $(f,g)$ be an ${\text{FF}}_{F}$ -formulation of ${\text{FF}}_{H}$ , where $F=\bigwedge_{o\in{\cal O}_{F}}F_{o}$ . Then for any $o\in{\cal O}_{F}$ and any path $p$ in $g_{o}$ labelled with some $o^{*}\in{\cal O}_{H}$ we have that

\displaystyle\neg V_{o,p}(f(x))=0\implies H_{o^{*}}(x)=0.

(1)

That is, $H_{o^{*}}\implies\neg V_{o,p}(f)$ , and we say that $\neg V_{o,p}(f)$ is a weakening of $H_{o^{*}}$ .

A proof system $P$ is characterized by a ${\mathsf{TFPH}}^{dt}$ class $\cal C$ with complete problem ${\text{FF}}_{F}$ if efficient provability of $F$ in that proof system implies low-complexity reductions to the complete problem ${\text{FF}}_{F}$ for that class, and membership in the class $\cal C$ implies that $P$ can prove the correctness of the reduction to $P$ . The latter takes the following form: if $(f,g)$ is a ${\text{FF}}_{F}$ -formulation of a ${\text{FF}}_{H}\in\cal C$ then

i)

From $H$ , $P$ can efficiently derive the reduced formula $F(f,g)$ .
ii)

$P$ has an efficient proof of $F(f,g)$ .

What properties must a proof system possess in order to perform (i) and (ii) for a subclass ${\cal C}\subseteq{\mathsf{TFPH}}^{dt}$ ? If ${\mathsf{TFNP}}^{dt}\subseteq\cal C$ then a Cook-Reckhow proof system (an ${\mathsf{NP}}$ -verifier) does not suffice unless ${\mathsf{NP}}={\mathsf{coNP}}$ ¹¹1Indeed, for any unsatisfiable $3$ -CNF formula $F$ , ${\text{FF}}_{F}\in{\mathsf{TFNP}}^{dt}$ .. Interestingly, what fails is step (i) – Theorem 23 shows that step (ii) can always be carried out by a Cook-Reckhow system. We will need to augment Cook-Reckhow proof systems in order to perform step (i). The issue is that Cook-Reckhow systems cannot always perform the weakening from (1). That is, if $F(f,g)=\bigwedge_{o\in{\cal O}_{F(f,g)}}F_{o}$ and $H=\bigwedge_{o^{\prime}\in{\cal O}_{H}}H_{o^{\prime}}$ then by correctness of the reduction, we know that for every $o\in{{\cal O}_{F(f,g)}}$ , $F_{o}$ is a weakening of some $H_{o^{\prime}}$ . However, Cook-Reckhow proof systems cannot necessarily derive $F_{o}$ efficiently given $H$ . For example, if $F_{o}=\top$ , the trivial tautology, then this is tantamount to proving that $F_{o}$ is a tautology, which is a ${\mathsf{coNP}}$ -complete task. It will suffice to augment our proof systems to be able to do so.

Definition 14.

Let $P$ be a Cook-Reckhow proof system. A proof of a $\Pi_{d+1}$ formula $F=\bigwedge_{i\in[m]}F_{i}$ in the proof system $\Sigma_{d}$ - $P$ is a pair $(H,\Pi)$ such that

1.

$\Pi$ is a $P$ -proof that the $\Pi_{d+1}$ -formula $H=\bigwedge_{j\in[k]}H_{j}$ is unsatisfiable.
2.

Each $H_{j}$ is a $\Sigma_{d}$ -formula such that there is some $i\in[m]$ for which $F_{i}\implies H_{j}$ . That is, $H_{j}$ is a $\Sigma_{d}$ -weakening of $F_{i}$ .

The complexity of the proof $(H,\Pi)$ is $\log|H|+\log s+d$ , where $\log s+d$ is the complexity of the proof $\Pi$ .

Clearly such proofs are verifiable in $\Sigma_{d}$ . As we will see, they suffice to characterize subclasses of ${\mathsf{TF}}\Sigma_{d}^{dt}$ . Note as well that the definition of a $\Sigma_{1}$ -proof system agrees with the standard definition of any proof system which corresponds to a ${\mathsf{TFNP}}^{dt}$ subclass. Indeed, $\Sigma_{1}$ -weakening is simply weakening over clauses, which can be performed in tree resolution, which characterizes ${\mathsf{FP}}^{dt}$ .

Comparison with Proof Systems for QBF.

A line of research has explored proof systems for proving the unsatisfiability of quantified boolean formulas (QBF) (see [4] for a survey). These QBF proof systems appear to be weaker than $\Sigma_{d}$ -proof systems when restricted to $\Sigma_{d}$ -formulas. Indeed, these proof systems are typically Cook-Reckhow systems augmented with a $\forall$ Reduction rule, and hence lower bounds for CNF formulas from the propositional case readily apply to these proof systems. This is not the case for $\Sigma_{d}$ -proof systems, and further $\Sigma_{d}$ weakening is able to simulate $\forall$ Reduction.

4 Sherali-Adams and Strong Range Avoidance

We begin with an example of a characterization by showing that strongRangeAvoidance is characterized by $\Sigma_{2}$ -Sherali-Adams. A full treatment of the Sherali-Adams proof system is given in the monograph [10].

For any boolean formula $F$ , we will assume without loss of generality that all negations occur at the leaves and let $\mathsf{Vars}^{+}(F)$ be the positive literals in $F$ and $\mathsf{Vars}^{-}(F)$ be the negative literals. For any conjunct $t=\bigwedge_{x\in\mathsf{Vars}^{+}(t)}x\wedge\bigwedge_{x\in\mathsf{Vars}^{-}(% t)}\neg x$ , we associate the polynomial $\prod_{x\in\mathsf{Vars}^{+}(t)}x\prod_{x\in\mathsf{Vars}^{-}(t)}(1-x)$ , and refer to them also as conjuncts. A conical junta is a sum of conjuncts ${\cal J}:=\sum t$ .

Let $D=\bigvee_{t}t$ be any DNF. We can express $D$ as a degree $\deg(D):=\max_{t\in D}\deg(t)$ polynomial

\sum_{t\in D}t-1.

Observe that for any $x\in\{0,1\}^{n}$ , $D(x)=1$ iff $\sum_{t\in D}t(x)-1\geq 0$ . Henceforth we will abuse notation and refer to $D$ as both the DNF and the associated polynomial.

Throughout this section we will work with multi-linear arithmetic, associating $x_{i}^{2}=x_{i}$ for every variable $x$ . This has the effect of restricting the underlying linear program to $\{0,1\}$ -points.

Definition 15.

Let $F=\{D_{i}\}_{i\in[m]}$ be an unsatisfiable collection of DNFs. A $\Sigma_{2}$ -Unary Sherali-Adams (which we denote by ${\mathsf{uSA}}$ ) proof $\Pi$ of $F$ is a weakening $F^{\prime}=\{D_{i}^{\prime}\}_{i\in[m^{\prime}]}$ of $F$ together with a list of conical juntas ${\cal J}_{i},{\cal J}$ , such that

\sum_{i\in[m^{\prime}]}D_{i}^{\prime}{\cal J}_{i}+{\cal J}=-1.

The degree $\deg(\Pi)$ is the maximum degree among $D_{i},D_{i}^{\prime}{\cal J}_{i},$ and ${\cal J}$ , and the size $\mathsf{size}(\Pi)$ is the number of monomials (counted with multiplicity)²²2This is a unary proof system as the number of monomials are counted with multiplicity, akin to writing coefficients in unary, rather than allowing for monomials with coefficients written in binary in $D_{i},D_{i}^{\prime}{\cal J}_{i},{\cal J}$ . The complexity of the proof is ${\mathsf{uSA}}(\Pi)\leavevmode\nobreak\ :=\leavevmode\nobreak\ \deg(\Pi)+\log% \mathsf{size}(\Pi)$ , and the complexity of proving $F$ is ${\mathsf{uSA}}(F)\leavevmode\nobreak\ :=\leavevmode\nobreak\ \min_{\Pi}{% \mathsf{uSA}}(\Pi)$ , where the minimum is taken over all ${\mathsf{uSA}}$ proofs of $F$ .

Note also that weakening subsumes the need to explicitly allow the additional conical junta in a ${\mathsf{uSA}}$ proof; we could instead defined ${\mathsf{uSA}}$ as a Nullstellensatz proof $\sum D_{i}^{\prime}{\cal J}_{i}=-1$ . This is because the additional junta $\cal J$ may be introduced using weakening: for each conjunct $t$ of $\cal J$ , weaken some $D_{i}$ in $F$ to true or $t$ . For example, $D_{i}$ can be weakened to $x_{i}\lor\neg x_{i}\lor t$ , the polynomial encoding of which is $x_{i}+(1-x_{i})+t-1=t$ .

Claim 16.

${\mathsf{uSA}}$ is sound and complete.

Proof.

Suppose that ${\mathsf{uSA}}$ is not sound; then there exists a ${\mathsf{uSA}}$ refutation of a satisfiable DNF $F=\{D_{i}\}_{i\in[m]}$ ,

\sum_{i\in[m^{\prime}]}D_{i}^{\prime}{\cal J}_{i}+{\cal J}=-1.

Let $x\in\{0,1\}^{n}$ be a satisfying assignment to $F$ , meaning that for every $i$ , $D_{i}^{\prime}(x)=1$ for any weakening $D_{i}^{\prime}$ of $D_{i}$ , and in particular the polynomial representation of $D_{i}^{\prime}(x)\geq 0$ . As juntas are non-negative over $\{0,1\}^{n}$ , we have that

\sum_{i\in[m^{\prime}]}D_{i}^{\prime}(x){\cal J}_{i}(x)+{\cal J}(x)\geq 0,

which is a contradiction.

For completeness, let $F=\{D_{i}\}_{i\in[m]}$ be an unsatisfiable formula. Each assignment $x\in\{0,1\}^{n}$ must falsify some DNF of $F$ , which we will denote by $D_{x}$ . Let $I_{x}$ be the indicator polynomial $I_{x}:=\prod_{i:x_{i}=1}x_{i}\prod_{i:x_{i}=0}(1-x_{i})$ of the assignment $x$ . We claim that the polynomial

\sum_{x\in\{0,1\}^{n}}I_{x}D_{x}=-1,

and is therefore a ${\mathsf{uSA}}$ proof. To see this, since we are working over the ideal $\langle x_{i}-x_{i}^{2}\rangle$ , it suffices to show that the polynomial evaluates to $-1$ on every $x\in\{0,1\}^{n}$ . Observe that if $y\in\{0,1\}^{n}$ falsifies $D_{x}$ , then $D_{x}(y)=-1$ ; additionally, if $x\neq y$ , then $I_{x}(y)=0$ . Hence, for every $y\in\{0,1\}^{n}$ ,

\sum_{x\in\{0,1\}^{n}}I_{x}(y)D_{x}(y)=I_{y}(y)D_{y}(y)=D_{y}(y)=-1.\

$\hfill\vartriangleleft$

In the rest of this section, we show that ${\mathsf{uSA}}$ is closely related to the search problem strongRangeAvoidance. We restate an equivalent definition next.

Definition 17.

An instance of strongRangeAvoidance $({\text{StrongAvoid}})$ is given by a map $f:[n]\rightarrow[n+1]$ . A solution is any $h\in[n+1]$ such that for every $p\in[n]$ , $f(p)\neq h$ .

StrongAvoid can be encoded as a CNF formula by introducing, for every $p\in[n]$ , $\log(n+1)$ -many binary variables $p_{1},\ldots,p_{\log n+1}$ naming in binary the hole $h\in[n+1]$ to which pigeon $p$ flies. For exposition, it will be convenient to think of $p$ as an $(n+1)$ -ary variable and we will denote by $[\![p=h]\!]$ the indicator conjunct that is satisfied iff $p$ maps to $h\in[n+1]$ under the given assignment

[\![p=h]\!]\leavevmode\nobreak\ :=\leavevmode\nobreak\ p_{1}^{h_{1}}\wedge% \ldots\wedge p_{\log(n+1)}^{h_{\log(n+1)}},

where $p_{i}^{h_{i}}=p_{i}$ if the $i^{th}$ bit of $h$ is $1$ and $\neg p_{i}$ otherwise. Note that $\sum_{h\in[n+1]}[\![p=h]\!]=1$ as polynomials.

We can express StrongAvoid as the unsatisfiable family of DNFs,

\bigvee_{p\in[n]}[\![p=h]\!]\hskip 50.00008pt\forall h\in[n+1].

The main theorem of this section is the following.

Theorem 18.

For any ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{2}^{dt}$ there is a complexity- $c$ StrongAvoid-formulation of ${\text{FF}}_{F}$ iff there is a $\Sigma_{2}$ - ${\mathsf{uSA}}$ proof of $F$ of complexity $\Theta(c)$ .

We break the proof of this theorem into Lemma 19 and Lemma 22, which are proven over the following two subsections. This theorem gives necessary and sufficient conditions for separating other ${\mathsf{TF}}\Sigma_{2}$ classes ${\cal C}$ from StrongAvoid: Exhibit a pseudo-expectation (see e.g., [10]) against any ${\mathsf{polylog}}(n)$ -width $\Sigma_{2}$ -weakening of the propositionalization of StrongAvoid.

4.1 SA Proofs Imply sRA Reductions

Lemma 19.

If there is a size $s$ and degree $d$ $\Sigma_{2}$ - ${\mathsf{uSA}}$ proof of $F$ , then there is a depth- $d$ reduction from ${\text{FF}}_{F}$ to an instance of StrongAvoid of size $O(s)$ .

To prove this lemma, it will be convenient to work with the following problem. We show that it is equivalent to StrongAvoid.

Definition 20.

The Unmetered Source of Dag (USoD) problem is defined as follows. The input is a “successor” function $S:[n]\rightarrow[n]$ which defines a graph in which each vertex has fan-out $\leq 1$ but arbitrary fan-in. There is an edge from $i$ to $j$ if $S(i)=j$ . To make the problem total, we enforce that the vertex $1$ is a sink; it will have fan-out $0$ but fan-in at least $1$ . The goal is to find a source; the solutions are:

$\blacksquare$

$1$ is a solution if either $S(1)\neq 1$ or $\forall v\neq 1\in[n]$ , $S(v)\neq 1$ ( $1$ is not a sink).
$\blacksquare$

$v\in[n]$ is a solution if $S(v)\neq v$ but $\forall u\in[n]$ , $S(u)\neq v$ ( $v$ is a source).

Lemma 21.

${\text{USoD}}=_{dt}{\text{StrongAvoid}}$ . Furthermore, this reduction is by depth- $1$ decision trees.

Proof.

From an instance $S:[n]\rightarrow[n]$ of USoD, we construct an instance $f:[n]\rightarrow[n+1]$ of StrongAvoid as follows. For $v\neq 1\in[n]$ , let $f(v)\leavevmode\nobreak\ :=\leavevmode\nobreak\ S(v)$ and let $f(1)\leavevmode\nobreak\ :=\leavevmode\nobreak\ n+1$ . We claim that any solution $u$ to this StrongAvoid instance is a source in $S$ . First observe that $u\neq n+1$ as $f(1)=n+1$ . Hence, by construction, we have that $\forall v\in[n],S(v)\neq u$ , and in particular $S(u)\neq u$ , so $u$ is a source.
For the converse direction, from an instance $f:[n]\rightarrow[n+1]$ of StrongAvoid we construct an instance $S:[n+1]\rightarrow[n+1]$ of USoD by defining $S(v+1)\leavevmode\nobreak\ :=\leavevmode\nobreak\ f(v)$ for all $v\in[n]$ and letting $S(1)=1$ . Let $v$ be a solution to this instance of USoD, if $v=1$ , then, since $S(1)=1$ , for all $u\in[n]$ , $f(u)\neq 1$ . Otherwise, $v\neq S(u)$ for all $u\in[n+1]$ , and so $v\neq f(u)$ for all $u\in[n]$ . $\hfill\blacktriangleleft$

Proof of Lemma 19.

Let $F=\bigwedge_{o\in{\cal O}}D_{o}$ , and let $\Pi$ be a size $s$ and degree $d$ ${\mathsf{uSA}}$ proof of $F$ over $n$ variables, where

\Pi:=\sum_{i\in[m]}\sum_{j\in I_{i}}D_{i}^{\prime}J_{j}+\sum_{k\in K}J_{k}+1=0,

for sets of indices $I_{i},K$ , each $D_{i}^{\prime}$ is a weakening of some $D_{o}\in F$ and each $J_{j},J_{k}$ is a conjunct. We construct an instance of USoD with one node per occurrence of a (signed) monomial in $\Pi$ . Therefore, for simplicity, we will refer to monomials as nodes and vice versa. The constant $1$ will be our distinguished sink, and we will set $S(1)=1$ . We will define the remaining successor pointers as follows:

Negative Monomials. Since $\Pi=0$ , there is a positive and negative copy of every monomial occurring in the proof; construct a pairing of the monomials in this way. Furthermore, under any assignment $x\in\{0,1\}^{n}$ , the number of monomials which evaluate to $1$ and to $-1$ is equal. For each negative monomial $-m$ in $\Pi$ , the decision tree $S(-m)$ queries the variables of $m$ and outputs as follows:

i)

If $m(x)=0$ , then $S(-m)=-m$ .
ii)

Otherwise, let $m$ be the positive copy of $-m$ that $-m$ is paired with, and set $S(-m)=m$ .

This completes the description of the successor pointer for negative monomials.

Positive Monomials. For any positive monomial $m$ , the decision tree for $S(m)$ first queries the (at most $d$ -many) variables of $m$ to determine the value of $m(x)$ . If $m(x)=0$ , then $S(m)=m$ . Otherwise, we will define $S$ as follows.

We define the successor pointer for the positive monomials which belong to each $D_{i}^{\prime}J_{j}$ first, and handle the monomials from the conjuncts $J_{k}$ later. Fix some $D_{i}^{\prime}J_{j}$ in $\Pi$ , where $D_{i}^{\prime}=\sum_{k\in[\ell]}t_{k}-1$ , and consider the monomials within it. We would like to satisfy the following property: there is a source within the monomials $D_{i}^{\prime}J_{j}$ iff $D_{i}^{\prime}(x)=-1$ (i.e., the DNF $D_{i}^{\prime}(x)=0$ ). To get some intuition, first suppose that $J_{j}=1$ and that all monomials $m$ in $D_{i}^{\prime}$ are positive – that is, $D_{i}^{\prime}J_{j}=\sum_{k\in[\ell]}m_{k}-1$ . Then, the current assignment to $S$ affects $D_{i}^{\prime}J_{j}$ as follows:

$\blacksquare$

Each monomial $m_{k}$ such that $m_{k}(x)=0$ is an isolated vertex for which $S(m_{k})=m_{k}$ .
$\blacksquare$

Each monomial $m_{k}$ for which $m_{k}(x)\neq 0$ has a single incoming edge (from $-m_{k}$ ).
$\blacksquare$

The monomial $-1$ has an outgoing edge.

If at least one of the monomials $m_{k}$ is non-zero, we can send it to $-1$ , and otherwise $-1$ becomes a source (see Figure 2). Therefore, the only sources will come from the “ $-1$ nodes” of falsified DNFs. To handle the general case, we use the fact that in every conjunct, under any assignment, there are at least as many non-zero positive monomials as non-zero negative monomials.

Figure 2: The “gadget” for a

D_{i}^{\prime}J_{j}

where

J_{j}=1

and

D_{i}^{\prime}

contains only positive literals (each conjunct is a monomial).

We now describe the construction in general. Consider a $D_{i}^{\prime}J_{j}$ in $\Pi$ . For each positive monomial $m$ in $D_{i}^{\prime}J_{j}=(\sum_{k\in[\ell]}t_{k}-1)J_{j}$ , belonging to some conjunct $t_{k}J_{j}$ , the pointer $S(m)$ will query the (at most $d$ -many) variables in $t_{k}J_{j}$ . Let $\alpha\in\{0,1\}^{\mathsf{Vars}(J_{j})}$ be the assignment to the variables of $J_{j}$ that was discovered.

If $J_{j}\!\upharpoonright\!\alpha=0$ : Then $D_{i}^{\prime}J_{j}\!\upharpoonright\!\alpha=0$ . Hence, for every positive monomial $m$ in $D_{i}^{\prime}J_{j}$ , either $m\!\upharpoonright\!\alpha=0$ , in which case we have already set $S(m)=m$ , or $m$ must cancel with another monomial $-m^{\prime}$ in $D_{i}^{\prime}J_{j}$ under $\alpha$ . That is, $m\!\upharpoonright\!\alpha=-m^{\prime}\!\upharpoonright\!\alpha$ , and so we define $S(m)=-m^{\prime}$ . Note that in this case there are no sources within $D_{i}^{\prime}J_{j}$ : every monomial $m$ $D_{i}^{\prime}J_{j}$ either evaluates to $0$ and nothing points to it, or has exactly one incoming and one outgoing edge.

If $J_{j}\!\upharpoonright\!\alpha\neq 0$ : We define the successor pointer for the monomials in $D_{i}^{\prime}J_{j}$ so that there is a source iff every for every term $t_{k}$ of $D_{i}^{\prime}$ , $t_{k}(x)=0$ . Let $\mathsf{Mons}(J_{j})^{+},\mathsf{Mons}(J_{j})^{-}$ be the (non-zero) positive and negative monomials in $J_{j}$ respectively. Let

\delta\leavevmode\nobreak\ :=\leavevmode\nobreak\ |\mathsf{Mons}^{+}(J_{j}\!% \upharpoonright\!\alpha)|-|\mathsf{Mons}^{-}(J_{j}\!\upharpoonright\!\alpha)|

be the difference between the number of positive and negative monomials, and note that $\delta>0$ as $J_{j}$ is a conjunct and $J_{j}\!\upharpoonright\!\alpha\neq 0$ . Recall that $D_{i}^{\prime}J_{j}=\sum_{k\in[\ell]}t_{k}J_{j}-J_{j}$ . For each term, we will define a matching so that $-J_{j}$ has only $\delta$ -many negative monomials without incoming edges, and every negative monomial in $t_{k}J_{j}$ has an incoming edge.

$\blacksquare$

For $-J_{j}$ : Define an arbitrary pairing $P\leavevmode\nobreak\ :=\leavevmode\nobreak\ \{(m,-m^{\prime})\}\subseteq% \mathsf{Mons}^{+}(J_{j}\!\upharpoonright\!\alpha)\times\mathsf{Mons}^{-}(J_{j}% \!\upharpoonright\!\alpha)$ such that each positive monomial occurs in exactly one pair and each negative monomial occurs in at most one pair. Hence we have $\delta$ -many negative monomials that are not paired. For each pair $(m,-m^{\prime})\in P$ , define $S(m)=-m^{\prime}$ .

Note that we have now defined the successor of every positive monomial in $J_{j}$ .
$\blacksquare$

For each $t_{k}J_{j}$ : Observe that as $t_{k}$ is a conjunct, under any assignment it contains at least as many positive monomials as negative monomials. Define an arbitrary pairing $P:=\{(m,-m^{\prime})\}\subseteq\mathsf{Mons}^{+}(t_{k}J_{j}\!\upharpoonright\!% \alpha)\times\mathsf{Mons}^{-}(t_{k}J_{j}\!\upharpoonright\!\alpha)$ such that each negative monomial occurs in exactly one pair and each positive monomial occurs in at most one pair. For each pair $(m,-m^{\prime})\in P$ , define $S(m)=-m^{\prime}$ . Let $\beta\in\{0,1\}^{\mathsf{Vars}(t_{k}J_{j})}$ be the assignment to the variables of $t_{k}J_{j}$ that was discovered by the trees made by the decision tree of any of the monomials $m$ in $t_{k}J_{j}$ . Let

$c\leavevmode\nobreak\ :=\leavevmode\nobreak\ |\mathsf{Mons}^{+}(t_{k}\!% \upharpoonright\!\beta)|-|\mathsf{Mons}^{-}(t_{k}\!\upharpoonright\!\beta)|$

be the difference between the number of non-zero positive and negative monomials in $t_{k}$ under $\beta$ .

If $c=0$ , then $t_{k}J_{j}\!\upharpoonright\!\beta=0$ , and so the number of non-zero positive and negative monomials is equal. In this case, each negative monomial has an incoming edge, which is provided by this pairing.

Otherwise, if $t_{k}J_{j}\!\upharpoonright\!\beta\neq 0$ , then there are $c\delta$ -many non-zero positive monomials whose successor is still undefined, and partition them into $c$ -many groups of $C_{1},\ldots C_{\delta}$ of $\delta$ -many monomials each. Recall that $-J_{j}$ has exactly $\delta$ -many negative monomials with no incoming edge, $-m_{1},\ldots,-m_{\delta}$ . For each $m\in C_{i}$ , define $S(m)=-m_{i}$ . In this case, each monomial in $t_{k}J_{j}$ and $-J_{j}$ has an incoming edge.

Finally, we define the successor for each positive monomial in the conical junta $\sum_{k\in K}J_{k}$ in $\Pi$ . We will do this individually for each $J_{k}$ . To do so, we use the fact that $J_{k}$ contains at least as many positive monomials as negative monomials in order to ensure that there is never any source among the monomials of $J_{k}$ . The successor for each positive monomial $m$ of $J_{k}$ queries the (at most $d$ -many) variables in $J_{k}$ for an assignment $\alpha\in\{0,1\}^{\mathsf{Vars}(J_{k})}$ . Define an arbitrary pairing $P\leavevmode\nobreak\ :=\leavevmode\nobreak\ \{(m,-m^{\prime})\}\subseteq% \mathsf{Mons}^{+}(J_{k}\!\upharpoonright\!\alpha)\times\mathsf{Mons}^{-}(J_{k}% \!\upharpoonright\!\alpha)$ such that each negative monomial occurs in exactly one pair and each positive monomial occurs in at most one pair. For each pair $(m,-m^{\prime})\in P$ , define $S(m)=-m^{\prime}$ . For the remaining positive monomials $m$ in $J_{k}$ whose successor is not defined, set $S(m)=1$ (this choice is somewhat arbitrary).

This completes the description of the successor function $S$ (the $f$ -part of the formulation). It remains to define the output function $g$ of the formulation. For each potential solution $m$ ,

$\blacksquare$

If $m$ is a monomial from some $D_{i}^{\prime}J_{j}$ , then $D_{i}^{\prime}$ is the weakening of some $D_{o}$ of $F$ , and we output $o$ .
$\blacksquare$

Otherwise, we output an arbitrary index $o\in[m]$ .

Finally, we prove that this formulation is correct. To do so, we show that the only monomials which do not have incoming edges belong to some $D_{i}^{\prime}J_{j}$ for which $D_{i}^{\prime}(x)$ is falsified. This suffices, as if $m$ belongs to $D_{i}^{\prime}J_{j}$ where $D_{i}^{\prime}(x)=0$ , then $g_{m}(x)=o$ for some $D_{o}$ of $F$ of which $D_{i}^{\prime}$ is a weakening of. Hence, $D_{o}(x)$ is falsified, and we have found a solution to ${\text{FF}}_{F}$ . By the negative monomial case in the formulation, every positive monomial has an incoming edge. By the pairings constructed in the formulation, every negative monomial in each $J_{k}$ in the conical junta also has an incoming edge. As well, for each $D_{i}^{\prime}J_{j}=\sum_{k}t_{k}J_{j}-J_{j}$ , each negative monomial in each $t_{k}J_{j}$ has an incoming edge. Hence, the only potential sources belong to the $-J_{j}$ terms of each $D_{i}^{\prime}J_{j}$ . As we argued before, if $J_{j}(x)=0$ , then there is no source in the monomials of $D_{i}^{\prime}J_{j}$ , so suppose that this is not the case. As we have paired off positive and negative monomials in $-J_{j}$ , the only incoming edge to each of the $\delta$ -many remaining negative monomials of $J_{j}$ must come from some $t_{k}J_{j}$ . If there is a $t_{k}$ such that $t_{k}(x)\neq 0$ (and hence $D_{i}^{\prime}(x)$ is satisfied), then $t_{k}J_{j}$ has $c\delta$ -many monomials which map to to the $\delta$ -many remaining negative monomials of $J_{j}$ , meaning that there is no source in $D_{i}^{\prime}J_{j}$ . Thus, $D_{i}^{\prime}J_{j}$ becomes a source only if $J_{j}(x)\neq 0$ and $D_{i}^{\prime}(x)$ is falsified. $\hfill\blacktriangleleft$

4.2 sRA Reductions Imply SA Proofs

We begin by observing that there is a trivial unary Sherali-Adams refutation of Range Avoidance:

\sum_{h\in[n+1]}\Big{(}\sum_{p\in[n]}[\![p=h]\!]-1\Big{)}=\sum_{p\in[n]}\sum_{% h\in[n+1]}[\![p=h]\!]-(n+1)=n-(n+1)=-1,

where the third equality follows as we $\sum_{h\in[n+1]}[\![p=h]\!]=1$ .

In the remainder of this section, we will show that unary Sherali-Adams can prove reductions to StrongAvoid.

Lemma 22.

If $f, g$ is a StrongAvoid-formulation of ${\text{FF}}_{F}$ of depth $d$ and size $s$ , then there is a degree- $O(d\log n)$ and size $\textup{poly}(s\cdot n^{d})$ $\Sigma_{2}$ - ${\mathsf{uSA}}$ proof of $F$ .

If $(f,g)$ is a StrongAvoid-formulation of ${\text{FF}}_{F}$ for some formula $F=\bigwedge_{i\in[m]}D_{i}$ , let $P(g_{h}),P(f_{p})$ be the set of all root-to-leaf paths in the decision trees $g_{h}$ and $f_{p}$ , respectively. As well, for any hole $h\in[n+1]$ , let $P_{h}(f_{p})$ be the set of paths in $f_{p}$ whose leaf is labeled by hole $h$ .

We can express the reduction from ${\text{FF}}_{F}$ to StrongAvoid as the unsatisfiable formula ${\text{StrongAvoid}}(f,g)$ defined as

	$\displaystyle\forall h\in[n+1],\leavevmode\nobreak\ \forall\sigma^{}\in P(g_{% h}),\bigvee_{p\in[n]}[\![p=h]\!]\vee\overline{\sigma^{}}$
	$\displaystyle\leavevmode\nobreak\ \equiv\forall h\in[n+1],\leavevmode\nobreak% \ \forall\sigma^{}\in P(g_{h}),\bigvee_{p\in[n]}[\![p=h]\!]\vee\bigvee_{% \sigma^{}\neq\sigma\in P(g_{h})}\sigma$
	$\displaystyle\leavevmode\nobreak\ \equiv\forall h\in[n+1],\leavevmode\nobreak% \ \forall\sigma^{}\in P(g_{h}),\bigvee_{p\in[n]}\bigvee_{\rho\in P_{h}(f_{p})% }\rho\vee\bigvee_{\sigma^{}\neq\sigma\in P(g_{h})}\sigma$

Letting $D_{h,\sigma^{*}}:=\bigvee_{p\in[n]}\bigvee_{\rho\in P_{h}(f_{p})}\rho\vee% \bigvee_{\sigma^{*}\neq\sigma\in P(g_{h})}\sigma$ , this becomes the unsatisfiable family of DNFs

{\text{StrongAvoid}}(f,g):=\{D_{h,\sigma^{*}}\}_{h\in[n+1],\sigma^{*}\in P(g_{% h})}.

Each of the formulas $D_{h,\sigma^{*}}$ is indeed a weakening of an axiom of $F$ . For a given $h\in[n+1]$ and $\sigma^{*}\in P(g_{h})$ , the DNF $D_{h,\sigma^{*}}$ is falsified if and only if $h$ is an output of the instance of StrongAvoid and $\sigma^{*}$ is satisfied by the assignment. When $\sigma^{*}$ is labeled with $F_{i}$ , an axiom of $F$ , the correctness of the reduction ensures that $F_{i}$ is also falsified by the assignment. Hence $D_{h,\sigma^{*}}$ is a semantic weakening of the axiom $F_{i}$ . The following lemma shows that ${\mathsf{uSA}}$ can deduce ${\text{StrongAvoid}}(f,g)$ from $F$ .

Proof of Lemma 22.

We will abuse notation and let $[\![p=h]\!]:=\sum_{\rho\in P_{h}(f_{p})}\rho$ denote the decision-tree substitution of the indicator $[\![p=h]\!]$ . To begin, we will weaken $F$ to ${\text{StrongAvoid}}(f,g)$ , the polynomials of which are

D_{h,\sigma^{*}}-1\leavevmode\nobreak\ :=\leavevmode\nobreak\ \sum_{p\in[n]}[% \![p=h]\!]+\sum_{\sigma^{*}\neq\sigma\in P(g_{h})}\sigma-1

for $h\in[n+1]$ and $\sigma^{*}\in P(g_{h})$ . As each $[\![p=h]\!]$ contains $O(\log n)$ -many Boolean variables, and we are replacing each one by a depth- $d$ decision tree, the degree of ${\text{StrongAvoid}}(f,g)$ is $O(d\log n)$ . Similarly, the size blows up by a factor of $n^{d}$ .

For any $h\in[n+1]$ ,

$\displaystyle\sum_{h\in[n+1]}\sum_{\sigma^{}\in P(g_{h})}\sigma^{}\big{(}D_{% h,\sigma^{*}}-1\big{)}$	$\displaystyle=\sum_{h\in[n+1]}\sum_{\sigma^{}\in P(g_{h})}\sigma^{}\Big{(}% \sum_{p\in[n]}[\![p=h]\!]+\sum_{\sigma^{*}\neq\sigma\in P(g_{h})}\sigma-1\Big{)}$
	$\displaystyle=\sum_{h\in[n+1]}\sum_{\sigma^{}\in P(g_{h})}\sigma^{}\Big{(}% \sum_{p\in[n]}[\![p=h]\!]-1\Big{)}$	(Multiplying two distinct paths of $g_{h}$ )
	$\displaystyle=\sum_{h\in[n+1]}\Big{(}\sum_{p\in[n]}[\![p=h]\!]-1\Big{)}$	(Summing all paths in the DT $g_{h}$ )
	$\displaystyle=\sum_{p\in[n]}\sum_{h\in[n+1]}[\![p=h]\!]-(n+1)$
	$\displaystyle=\sum_{p\in[n]}1-(n+1)=-1$	(Summing all paths in the DT $f_{p}$ )

$\hfill\blacktriangleleft$

5 A Generic Correspondence

In this section we establish a general correspondence between uniform subclasses of total search problems in the polynomial hierarchy and proof systems. Our characterizations will rely on the following two properties of a $\Sigma_{d}$ -proof system:

$\blacksquare$

Reduction-Closed. For unsatisfiable $\Pi_{d.5}$ formulas $F, H$ , if $P$ has a complexity- $s$ proof of $F$ and there is a complexity- $c$ ${\text{FF}}_{F}$ -formulation of ${\text{FF}}_{H}$ , then $P(H)=\textup{poly}(cs)$ .
$\blacksquare$

Reflective. $P$ has ${\mathsf{polylog}}(n)$ -complexity proofs of a reflection principle about itself – a formula encoding the soundness of this proof system; we expand on the meaning of this below.

We show the following, generalizing [5].

Theorem 23.

The following hold:

i)

Every uniform subclass of ${\mathsf{TF}}\Sigma_{d}$ is characterized by a $\Sigma_{d}$ -proof system.
ii)

Every $\Sigma_{d}$ -proof system which is reduction-closed and reflective is characterized by a subclass of ${\mathsf{TF}}\Sigma_{d}$ .

We prove (i) in Subsection 5.1 and (ii) in Subsection 5.2.

5.1 A Proof System for any ${\mathsf{TF}}\Sigma_{d}$ Problem

In this section we show how to construct a proof system from any total search problem $R\subseteq\{0,1\}^{n}\times\cal O$ , which we think of as the complete problem for some uniform subclass. The key insight is that one can view a decision tree reduction from a total search problem $Q\subseteq\{0,1\}^{m}\times{\cal O}_{Q}$ to $R$ as a proof that $Q$ is total, if we take the totality of $R$ as an axiom. In what follows, we formalize this intuition. We define proofs in the canonical proof system for a ${\mathsf{TF}}\Sigma_{d}^{dt}$ subclass as reductions to one of its complete problems.

Definition 24.

Let ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{d}^{dt}$ where $F_{n}=\bigwedge_{o\in[m]}F_{o}$ . The canonical proof system for ${\text{FF}}_{F}$ , denoted $P_{F}$ , is defined as follows: A proof $\Pi$ in $P_{F}$ consists of a triple $(n,f,g,F_{n}(f,g))$ , where

$\blacksquare$

$(f,g)$ is a ${\text{FF}}_{F}$ -formulation (i.e., a set of decision trees) to an instance of ${\text{FF}}_{F}$ on $n$ variables, and
$\blacksquare$

$F_{n}(f,g)=\bigwedge_{o\in[m^{*}]}L_{o}$ is the reduced formula associated with this formulation.

$\Pi$ is a $P_{F}$ proof of an unsatisfiable formula $H=\bigwedge_{t\in[m^{\prime}]}H_{t}$ , where each $H_{t}$ is a $\Sigma_{d}$ -formula, if for every $L_{o}$ in $F_{n}(f,g)$ there exists some $t\in[m^{\prime}]$ such that $L_{o}$ is a $\Sigma_{d}$ -weakening of $L_{o}$ ; that is,

H_{t}\implies L_{o}.

The size of the proof $\Pi$ is the number of bits needed to write down $\Pi$ , and the width of $\Pi$ is the maximum depth among the decision trees in the formulation,

0pt(\Pi)\leavevmode\nobreak\ :=\leavevmode\nobreak\ \max_{i\in[n],o\in[m]}\big% {\{}0pt(f_{i}),0pt(g_{o})\big{\}}.

The complexity of proving $H$ in $P_{F}$ is the minimum over all $P_{F}$ -proofs of $H$ ,

P_{F}(H)\leavevmode\nobreak\ :=\leavevmode\nobreak\ \min\big{\{}0pt(\Pi)+\log% \mathsf{size}(\Pi):\Pi\mbox{ is a $P_{F}$-proof of $H$}\big{\}}.

This proof system is sound, since any substitution of an unsatisfiable formula remains unsatisfiable. As well, it is complete for unsatisfiable $\Pi_{d+1}$ formulas, as depth- $n$ decision trees suffice to solve any total search problem. It is also verifiable by a polynomial-time $\Pi^{P}_{d-1}$ machine which generates $F_{n}$ , checks that $(f,g)$ is a valid ${\text{FF}}_{F}$ -formulation which agrees with the reduced formula $F_{n}(f,g)$ , and checks that $H_{t}\implies L_{o}$ Note that this proof system agrees with the definition of [5] when $d=1$ .

We will show that $P_{F}$ characterizes the subclass with complete problem ${\text{FF}}_{F}$ , proving the first direction of Theorem 23.

Lemma 25.

If ${\text{FF}}_{F},{\text{FF}}_{H}\in{\mathsf{TF}}\Sigma_{d}^{dt}$ , then there is a complexity- $c$ ${\text{FF}}_{F}$ -formulation of ${\text{FF}}_{H}$ iff $P_{F}(H)\leq c\cdot{\mathsf{polylog}}(n)$ .

Proof.

Let $(f,g)$ be a complexity- $c$ ${\text{FF}}_{F}$ -formulation of ${\text{FF}}_{H}$ . We claim that the tuple $(n,f,g,{\text{FF}}_{F}(f,g))$ is a $P_{F}$ proof of $H$ . As ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{d}^{dt}$ , $F$ is a $\Pi_{d.5}$ formula, and so the reduced formula ${\text{FF}}_{F}(f,g)$ is a $\Pi_{d+1}$ -formula ( $\Pi_{d.5}$ if $c={\mathsf{polylog}}(n)$ ). As well, the size of ${\text{FF}}_{F}(f,g)$ is at most $\mathsf{size}({\text{FF}}_{F})\cdot\exp(O(c))$ , as each clause/term on the bottom layer of $F$ has width at most ${\mathsf{polylog}}(n)$ and we replace it by the CNF/DNF representation of a depth- $O(c)$ decision tree, which has width $O(c)$ and size at most $\exp(O(c))$ . Finally, for $F(f,g):=\bigwedge_{o\in[m^{*}]}L_{o}$ and $H:=\bigwedge_{t\in[m]}H_{t}$ , by the correctness of the formulation, we can conclude that for every $o\in[m^{*}]$ there exists some $t\in[m^{\prime}]$ such that $H_{t}\implies L_{o}$ , and so $L_{o}$ is a $\Sigma_{d}$ -weakening of $H_{t}$ .

For the converse direction, suppose that $(n,f,g,F(f,g))$ is a $P_{F}$ proof of an unsatisfiable formula $H\leavevmode\nobreak\ :=\leavevmode\nobreak\ \bigwedge_{i\in[m]}H_{i}$ , where each $H_{i}$ is a $\Sigma_{d}$ -formula. By definition, $(f,g)$ constitutes a complexity- $c$ ${\text{FF}}_{F}$ -formulation of ${\text{FF}}_{H}$ . Indeed, each decision tree of $(f,g)$ has depth at most $c$ and there are at most $2^{c}$ -many of them, and so this is a complexity- $c$ formulation. $\hfill\blacktriangleleft$

5.2 A ${\mathsf{TF}}\Sigma_{d}$ Problem for any Proof System which Reflects

In this section we show that a $\Sigma_{d}$ -proof system $P$ corresponds to a ${\mathsf{TF}}\Sigma_{d}$ -problem if that proof system is reduction closed and reflective.

A reflection principle states that $P$ -proofs are sound; we will restrict ourselves to proofs of $\Sigma_{d.5}$ formulas. Typically, the provability of a proof system’s reflection principle is sufficient in order to simulate that system. In our setting, a reflection principle will falsely assert that there is a complexity- $c$ $P$ -proof $\Pi$ of a $\Sigma_{d.5}$ -formula $H$ and that $H$ is satisfied by a truth assignment $\alpha$ :

{\text{Ref}}_{P}\leavevmode\nobreak\ :=\leavevmode\nobreak\ {\text{Proof}}(H,% \Pi)\wedge{\text{Sat}}(H,\alpha).

This formula will be parameterized by $n_{H}$ , the number of variables of $H$ , as well as $c$ the complexity of the proof $\Pi$ .

SAT. The formula ${\text{Sat}}(H,\alpha)$ states that $\alpha\in\{0,1\}^{n_{H}}$ is a satisfying assignment to $H$ , where $\alpha\in\{0,1\}^{n}$ and $H$ are given as input. A generic $\Pi_{d.5}$ -formula has the following structure:

H=\bigwedge_{o\in{\cal O}}\bigvee_{z_{1}\in\{0,1\}^{\ell_{1}}}\bigwedge_{z_{2}% \in\{0,1\}^{\ell_{2}}}\ldots\underset{z_{d-1}\in\{0,1\}^{\ell_{d-1}}}{\bigcirc% }H_{o,z_{1},\ldots,z_{d-1}}

where $\bigcirc\in\{\wedge,\lor\}$ and $H_{o,z_{1},\ldots,z_{d-1}}$ , is a width $w\in{\mathsf{polylog}}(n)$ clause if $\bigcirc=\wedge$ or conjunct if $\bigcirc=\lor$ . Each $H_{o,\vec{z}}\leavevmode\nobreak\ :=\leavevmode\nobreak\ H_{o,z_{1},\ldots,z_{% d-1}}$ is specified by $w$ -many $(2n+1)$ -ary variables $v_{o,z,1},\ldots,v_{o,z,w}\in[2(n+1)]$ , where $v_{o,z,i}=j$ denotes the variable

$\blacksquare$

$x_{j}$ if $i\in[n]$ ,
$\blacksquare$

$\neg x_{j-n}$ if $j\in\{n+1,\ldots,2n\}$ ,
$\blacksquare$

constant $1$ if $j=2n+1$ ,
$\blacksquare$

constant $0$ if $j=2n+2$ .

We could allow the formula ${\text{Ref}}_{P}$ to be parameterized by $|{\cal O}|,\ell_{1},\ldots,\ell_{d-1}$ . However, for simplicity, since we are considering complexity- $c$ proofs, it suffices to simply set all of these parameters to $2^{c}$ and $w=c$ . In this case, the number of $H_{o,\vec{z}}$ is $2^{cd}$ , and hence the number of Boolean variables of $H$ is $c\log(2n_{H}+2)\cdot 2^{cd}$ . Then the $\Pi_{d.5}$ formula Sat can be written as

{\text{Sat}}(H,\alpha)\leavevmode\nobreak\ :=\leavevmode\nobreak\ \bigwedge_{o% \in{\cal O}}H_{o}(\alpha):=\bigwedge_{o\in{\cal O}}\bigvee_{z_{1}\in\{0,1\}^{% \ell_{1}}}\bigwedge_{z_{2}\in\{0,1\}^{\ell_{2}}}\ldots\underset{z_{d-1}\in\{0,% 1\}^{\ell_{d-1}}}{\bigcirc}[\![H_{o,\vec{z}}(\alpha)=1]\!],

where $[\![H_{o,\vec{z}}(\alpha)=1]\!]$ is the width- $O(w\log n_{H})$ DNF (if $\bigcirc=\vee$ ) or CNF (if $\bigcirc=\wedge$ ) defined by the following decision tree $T_{o,\vec{z}}$ : First query the $w\log(2n_{H}+2)$ -many Boolean variables $H_{o,\vec{z},1},\ldots,H_{o,\vec{z},w}$ to determine the literals $\ell_{1},\ldots,\ell_{w}$ of $H_{o,\vec{z}}$ . Then, query the corresponding bits of $\alpha$ to determine if $H_{o,\vec{z}}$ is satisfied. If it is, then $T_{o,\vec{z}}$ outputs $1$ , and otherwise it outputs $0$ . This can be converted into a DNF or CNF in the usual way.

Proof.

The formula ${\text{Proof}}(H,\Pi)$ states that $\Pi$ is a $P$ -proof of $H$ . A complication is that there are many different ways by which one could encode a $P$ -proof as a formula, some of which may change the difficulty of proving the reflection principle drastically. Following [5], we define one reflection principle for each encoding of a $P$ -proof; we call such an encoding a verification procedure. $\hfill\blacktriangleleft$

Definition 26.

A verification procedure $V$ for a $\Sigma_{d}$ -proof system $P$ , parameterized by $n_{H}$ , $c$ , is a $\Pi_{d.5}$ -formula which generically encodes a complexity- $c$ $P$ -proof $\Pi$ of an $n_{H}$ -variate formula $H$ . Specifically, the formula $V_{n_{H},c}(\Pi,H)$ has two sets of variables $H$ , $\Pi$ , where:

$\blacksquare$

An assignment to the variables $H=\{H_{o,\vec{z},i}|i\in[n_{H}]\}$ specifies a $\Pi_{d.5}$ formula as before.
$\blacksquare$

An assignment to the variables $\Pi$ specifies a purported $P$ -proof of $H$ of complexity $c$ , such that any error in $\Pi$ can be verified by an efficient $\Sigma_{d-1}$ -algorithm (placing ${\text{Ref}}\in{\mathsf{TF}}\Sigma_{d}$ ).
$\blacksquare$

$V$ has $2^{\Theta(c)}$ -many variables.

As $c$ bounds the logarithm of the size of the proof, and the number of variables is exponential in $\Theta(c)$ , the second condition ensures that a violated sub-formula of $V$ can be verified by a $\Sigma_{d-1}$ -algorithm making ${\mathsf{polylog}}(c)$ -many queries.

A reflection principle for a proof system $P$ and verification procedure $V$ is

{\text{Ref}}_{P,V}\leavevmode\nobreak\ :=\leavevmode\nobreak\ {\text{Proof}}_{% n_{H},c}(H,\Pi)\wedge{\text{Sat}}_{n_{H},c}(H,\alpha),

where ${\text{Proof}}_{n_{H},c}(H,\Pi)\leavevmode\nobreak\ :=\leavevmode\nobreak\ V_{% n_{H},c}(H,\Pi)$ . Often, we will suppress the subscripts $P, V$ .

We now prove point (ii) of Theorem 23.

Lemma 27.

Let $P$ be a $\Sigma_{d}$ -proof system that is reduction closed and reflective for some ${\text{Ref}}\leavevmode\nobreak\ :=\leavevmode\nobreak\ {\text{Ref}}_{P,V}$ . Then for any ${\text{FF}}_{H}\in{\mathsf{TF}}\Sigma_{d}$ ,

i)

If there is a complexity- $c$ ${\text{FF}}_{{\text{Ref}}}$ -formulation of ${\text{FF}}_{H}$ , then $P(H)=\textup{poly}(c\cdot P({\text{Ref}}))$ .
ii)

There is a complexity $O(P(H))$ ${\text{FF}}_{{\text{Ref}}}$ -formulation of ${\text{FF}}_{H}$ .

Proof.

To prove (i), suppose that there is a complexity- $c$ ${\text{FF}}_{\text{Ref}}$ -formulation of $H$ . By the definition of being reduction closed, there is a $P$ proof of $H$ of complexity $\textup{poly}(c\cdot P({\text{Ref}}))$ .

For (ii), let $\Pi$ be a complexity- $c$ proof of $H$ in $P$ . We construct a ${\text{FF}}_{{\text{Ref}}}$ -formulation $(f,g)$ of ${\text{FF}}_{H}$ as follows. $f$ will hard-wire $(\Pi,H)$ as the input to Ref, and map the input variables of ${\text{FF}}_{H}$ to the variables $\alpha_{1},\ldots,\alpha_{n_{H}}$ of Ref. Since $\Pi$ is a valid proof of $H$ , ${\text{Proof}}(\Pi,H)$ is always satisfied, and we can set $g_{o}$ arbitrarily for any solution $o$ corresponding to a subformula of ${\text{Proof}}(\Pi,H)$ . As ${\text{Proof}}(\Pi,H)$ is always satisfied under this reduction, the only solutions which may occur belong to ${\text{Sat}}(H,\alpha)$ . In particular, as we have mapped the input variables of $H$ to the bits $\alpha_{1},\ldots,\alpha_{n_{H}}$ , for any assignment $x\in\{0,1\}^{n}$ , $H_{o}(x)=0\iff H_{o}(\alpha)=0$ . Hence, we define $g_{o}=o$ . $\hfill\blacktriangleleft$

6 Characterizations in ${\mathsf{TF}}\Sigma_{2}$

In this section we uncover ${\mathsf{TF}}\Sigma_{2}$ characterizations of several well-studied proof systems – DNF Resolution, DNF Circular Resolution [1, 8], and DNF Reversible Resolution [12, 8]. Along the way we introduce several new ${\mathsf{TF}}\Sigma_{2}$ classes, which are inspired by ${\mathsf{TFNP}}$ classes. These are analogs to the coloured ${\mathsf{TFNP}}$ classes introduced in [18, 8]. In Subsection 6.3 we explore the relationships between these and prominent ${\mathsf{TF}}\Sigma_{2}$ subclasses.

The DNF resolution proof systems are extensions of the resolution proof system (and restrictions of) to allow them to operate with DNF formulas, rather than only clauses. Davis and Robere [8] gave characterizations of these systems by coloured ${\mathsf{TFNP}}$ classes. We introduce several classes which characterize the $\Sigma_{2}$ -variants of these proof systems; we believe these ${\mathsf{TF}}\Sigma_{2}$ classes herbrandize to the coloured classes.

Definition 28.

A ${\mathsf{Res}}({\mathsf{polylog}})$ refutation of a $\Pi_{2}$ -unsatisfiable formula $F=\bigwedge_{i=1}^{m}A_{i}$ is a sequence of ${\mathsf{polylog}}(n)$ -width DNF formulas $\Pi=(D_{1},\ldots,D_{s}=\bot)$ where each $D_{i}$ is deduced from previous DNFs by one of the following rules:

$\blacksquare$

Axiom Introduction. Introduce $A_{i}$ for some $i\in[m]$ .
$\blacksquare$

Symmetric Cut. From $D\lor t$ and $D\lor\overline{t}$ derive $D$ , where $t$ is any term.
$\blacksquare$

Reverse Cut. From $D$ derive $D_{i}=D\lor t$ and $D_{i+1}=D\lor\overline{t}$ , for some term $t$ .

The size $s$ of $\Pi$ is the sum of the sizes of DNFs involved in $\Pi$ , and the width $w$ is the maximum width of any DNF in $\Pi$ . The complexity of $\Pi$ is $\log s+w$ .

A ${\mathsf{RevRes}}({\mathsf{polylog}})$ proof is a ${\mathsf{Res}}({\mathsf{polylog}})$ proof in which every DNF in the sequence is used as the premise to a derivation rule at most once.

A ${\mathsf{uCircRes}}({\mathsf{polylog}})$ proof has access to the additional rule

$\blacksquare$

DNF Creation. $S_{i}=S_{i-1}\cup\{D\}$ , where $D$ is any DNF formula.

provided that each copy of $D$ that is created in this way is derived at least as many times as it is used as the premise to a derivation rule.

The following technical lemma will be key to our characterizations.

Lemma 29 (Theorem 3.6 in [8]).

${\mathsf{Res}}({\mathsf{polylog}}),{\mathsf{RevRes}}({\mathsf{polylog}}),$ and ${\mathsf{uCircRes}}({\mathsf{polylog}})$ are reduction closed.

Davis and Robere proved Lemma 29 for DNF resolution proofs of $\Pi_{1.5}$ -formulas (that is, when the axioms are clauses). It is straightforward to see that it holds by exactly the same argument (Claim 1) when the axioms are DNF formulas. In Section 7 we prove this theorem for depth- $d.5$ Frege, for every $d$ , of which ${\mathsf{Res}}(k)$ is $d=1$ .

In the following subsections we will prove Theorem 5, characterizing each of these proof systems by new ${\mathsf{TF}}\Sigma_{2}^{dt}$ subclasses. To define each of these classes, it will be convenient to use the following notion of a meta-pointer.

Definition 30.

Given a function $S:[m]\times[t]\rightarrow[m]$ , the meta-pointer $\tilde{S}:[m]\rightarrow[m]\cup\{undefined\}$ is defined as

\tilde{S}(u)=\begin{cases}v&\mbox{ if for every $i\in[t]$, $S(u,i)=v$,}\\ u&\mbox{ if there is $i\in[t]$ such that $S(u,i)=u$}\\ undefined&\mbox{ otherwise if there is $i,j\in[t]$ such that $u\neq S(u,i)\neq S% (u,j)$.}\end{cases}

Note that, if $u\neq v$ , $\tilde{S}(u)=v$ is $\Pi_{1}$ -verifiable: For all $i\in[t]$ , we need to verify that $S(u,i)=v$ , which takes $\log(m)$ queries. Moreover, $\tilde{S}(u)=u$ and $\tilde{S}(u)=undefined$ are $\Sigma_{1}$ verifiable: We can non-deterministically guess $i\in[t]$ such that $S(u,i)=u$ , or $i\neq j\in[t]$ such that $u\neq S(u,i)\neq S(u,j)$ ; in other words, they are efficiently computable if we are given $i$ (and $j$ ) as witnesses. The inclusion in ${\mathsf{TF}}\Sigma_{2}$ of the problems presented in this chapter follows directly from this fact.

6.1 DNF Resolution

${\mathsf{polylog}}(n)$ -width resolution was characterized by the ${\mathsf{TFNP}}^{dt}$ subclass ${\mathsf{PLS}}$ [6]. In this section we introduce a ${\mathsf{TF}}\Sigma_{2}$ -variant of the ${\mathsf{PLS}}$ -complete problem iteration and show that it characterizes $\Sigma_{2}$ - ${\mathsf{Res}}({\mathsf{polylog}})$ . The iteration problem encodes the principle that every DAG has a sink. The input is given by a pointer function $S:[n]\rightarrow[n]$ giving the successor of a node $u\in[n]$ , thought of as the next node on a root-to-leaf walk in the DAG. A solution is (i) an invalid source $S(1)=1$ , (ii) a $u$ which points backwards $S(u)<u$ , (iii) a sink: $u\in[n]$ such that $S(u)\neq u$ but $S(S(u))=S(u)$ , or (iv) a node $u$ with an undefined pointer $S(u)=undefined$ . Our ${\mathsf{TF}}\Sigma_{2}$ variant obfuscates the successor function. Similar ideas were used to define the ${\text{rWPHP}}_{2}$ problem in [15].

Definition 31.

An instance of ${\text{Iter}}_{2}$ is given by a function $S:[m]\times[t]\rightarrow[m]$ . A solution is a witness of a solution to the iteration instance defined by the meta-pointer $\tilde{S}$ :

$\blacksquare$

$(u,i,i^{\prime})$ such that $S(u,i),S(u,i^{\prime})\neq u$ and $S(u,i)\neq S(u,i^{\prime})$ , ( $\tilde{S}(u)$ is undefined.)
$\blacksquare$

$(u,i)$ such that $S(u,i)<u$ . (A pointer which points backwards)
$\blacksquare$

$(1,i)$ if $S(1,i)=1$ . ( $1$ is not a source)
$\blacksquare$

$(u,v,i)$ such that $\tilde{S}(u)=v$ and $S(v,i)=v$ . ( $v$ is a proper sink)

The class ${\mathsf{PLS}}^{dt}_{2}$ is the set of $R\in{\mathsf{TF}}\Sigma_{2}^{dt}$ such that $R\leq_{dt}{\text{Iter}}_{2}$ .

Theorem 32.

For any ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{2}^{dt}$ , there is a complexity- $c$ ${\text{Iter}}_{2}$ -formulation of ${\text{FF}}_{F}$ iff there is a complexity $O(c)$ $\Sigma_{2}$ - ${\mathsf{Res}}({\mathsf{polylog}})$ proof of $F$ .

We prove this theorem in the following two lemmas, each giving one direction.

Lemma 33.

For ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{2}$ , if $\Sigma_{2}$ - ${\mathsf{Res}}({\mathsf{polylog}})(F)=c$ , then there is a complexity- $O(c)$ ${\text{Iter}}_{2}$ -formulation of ${\text{FF}}_{F}$ .

Proof.

Let $(\Pi,H)$ be a $\Sigma_{2}$ - ${\mathsf{Res}}({\mathsf{polylog}})(F)$ proof of $F=\bigwedge_{i\in[\ell]}F_{i}$ , where $H=\bigwedge_{i\in[k]}A_{i}$ and each $A_{i}$ is a $\Sigma_{2}$ -weakening of a DNF of $F$ . Up to padding, we may assume that each DNF in the proof has the same number of terms $t$ . Consider the proof $\Pi=D_{1},\ldots,D_{m}$ in reverse order so that $D_{1}=\bot$ ; this will be our designated source.

Let $t_{u,i}$ be the $i^{th}$ term of $D_{u}$ . Given an assignment $\alpha\in\{0,1\}^{n}$ to the variables of $F$ , we construct a function $S_{\alpha}:[m]\times[t]\rightarrow[m]$ by setting $S_{\alpha}(u,i)$ to be:

$\blacksquare$

$u$ if $D_{u}$ is an axiom, or if $t_{u,i}(\alpha)=1$ ;
$\blacksquare$

$v$ if $t_{u,i}(\alpha)=0$ and $D_{u}$ was derived from $D_{v}$ by the reverse cut rule or semantic weakening of an axiom;
$\blacksquare$

$v$ if $t_{u,i}(\alpha)=0$ and $D_{u}$ was derived from $D_{v}=D_{u}\vee t$ and $D_{w}=D_{u}\vee\bar{t}$ via symmetric cut and $t(\alpha)=0$ and $w$ if $\bar{t}(\alpha)=0$ ;

Finally, for each solution $o$ to the instance $S_{\alpha}$ , we define the output of the reduction $g_{o}(\alpha)$ to be arbitrary if $o$ does not correspond to an axiom $A_{i}$ of $H$ , and otherwise this axiom $A_{i}$ is a weakening of a DNF $F_{j}$ of $F$ , and we set $g_{o}(\alpha)=j$ . Note that in this case $A_{i}(\alpha)=0\implies F_{j}(\alpha)=0$ . Observe that computing $S_{\alpha}(u,i)$ involves evaluating at most two terms, and hence the depth of the reduction is at most twice the width of the proof. It remains to argue that the reduction is correct.

Claim 34.

The function $\tilde{S}_{\alpha}$ satisfies the following properties:

i)

$\tilde{S}_{\alpha}$ is defined everywhere.
ii)

If $D_{u}$ is not an axiom of $H$ , then $D_{u}(\alpha)=0$ iff $\tilde{S}_{\alpha}(u)\neq u$ .
iii)

If $\tilde{S}_{\alpha}(u)=v\neq u$ , then $D_{v}(\alpha)=0$ .

Assuming the claim, we see that the only type of solution to this ${\text{Iter}}_{2}$ instance $S_{\alpha}$ are proper sinks corresponding to falsified axioms of $H$ , which are weakenings of (falsified) axioms of $F$ . Hence, $g$ returns a correct solution to ${\text{FF}}_{F}(\alpha)$ .

Proof of Claim.

We prove each item, beginning with (i). Clearly $\tilde{S}_{\alpha}$ is well defined for any $u$ that was not derived using the cut rule since $S_{\alpha}(u,i)$ only has one choice of value other than $u$ . So now consider $u$ such that $D_{u}$ was derived from $D_{v}=D_{u}\vee t$ and $D_{w}=D_{u}\vee\bar{t}$ . For $i\in[t]$ , we see that $S_{\alpha}(u,i)$ depends on two values: $t_{u,i}(\alpha)$ , and $t(\alpha)$ in the case where $t_{u,i}(\alpha)=0$ . Thus, $t(\alpha)$ being independent of $i$ , $S_{\alpha}(u,i)$ is always identical when not equal to $u$ .

(ii) follows from the fact that $D_{u}(\alpha)=0$ iff $t_{u,i}(\alpha)=0$ for all $i$ , and $\tilde{S}_{\alpha}(u)=u$ iff $t_{u,i}(\alpha)=1$ for at least one $i$ . Finally, (iii) follows by definition. $\hfill\vartriangleleft$ $\hfill\blacktriangleleft$

We will now prove the converse. First, we describe the encoding of ${\text{Iter}}_{2}$ as an unsatisfiable formula. For each $(u,i)\in[m]\times[t]$ , the $m$ -ary value of $S_{u,i}$ will be described by $\log m$ -many boolean variables $S_{u,i,b}$ , where the indicator function

[\![S_{u,i}=v]\!]\leavevmode\nobreak\ :=\leavevmode\nobreak\ \bigwedge_{b\in[% \log m]}S_{u,i,b}^{v_{b}},

where we think of $v$ as being written in its binary encoding, $v_{b}$ is its $b^{th}$ bit, and $S_{u,i,b}^{1}=S_{u,i,b}$ and $S_{u,i,b}^{0}=\neg S_{u,i,b}$ . As well, $[\![S_{u,i}\neq v]\!]=\neg[\![S_{u,i}=v]\!]$ , and

[\![\tilde{S}_{u}\neq v]\!]\leavevmode\nobreak\ :=\leavevmode\nobreak\ \bigvee% _{i\in[t]}[\![S_{u,i}\neq v]\!].

Then ${\text{Iter}}_{2}$ is the conjunction of the following subformulas:

$\blacksquare$

$[\![S_{1,i}\neq 1]\!]$ for each $i\in[n]$ . (1 is not a source)
$\blacksquare$

$[\![S_{u,i}\neq v]\!]\vee[\![S_{u,i^{\prime}}\neq v^{\prime}]\!]$ for all $v\neq v^{\prime}$ and $i\neq i^{\prime}$ such that $u\neq v,v^{\prime}$ ( $\tilde{S}$ is defined everywhere)
$\blacksquare$

$[\![S_{u,i}\neq v]\!]$ for all $v<u$ and $i\in[n]$ . (Nothing points backwards)
$\blacksquare$

$[\![\tilde{S}_{u}\neq v]\!]\vee[\![S_{v,j}\neq v]\!]$ for all $u<v$ and $j\in[n]$ . ( $v$ is not a proper sink)

Note that the subformulas of the ${\text{Iter}}_{2}$ formula are clauses making the formula a CNF. We may then question what makes ${\text{Iter}}_{2}$ a ${\mathsf{TF}}\Sigma_{2}^{dt}$ problem and not a ${\mathsf{TFNP}}^{dt}$ one. The key to understanding this resides in the size of said clauses. Indeed, for a false formula problem corresponding to a CNF to be in ${\mathsf{TFNP}}^{dt}$ , we need to be able to verify if a given clause is falsified by an assignment by only querying a ${\mathsf{polylog}}(n)$ amount of bits. This in turn directly implies that we would need each clause to be of ${\mathsf{polylog}}(n)$ -width. This is not the case here because of the fourth type of axioms, which are of $\textup{poly}(n)$ -width. On the other hand, considering clauses as $1$ -width DNFs, we see that this false formula problem corresponding to this formula lands indeed in ${\mathsf{TF}}\Sigma_{2}^{dt}$ . We now state the converse.

Lemma 35.

For ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{2}$ , if there is a complexity- $c$ ${\text{Iter}}_{2}$ -formulation of ${\text{FF}}_{F}$ , then there is a complexity- $O(c)$ ${\mathsf{Res}}({\mathsf{polylog}})$ proof of $F$ .

Observe that the set of formulas $\{[\![S_{u,i}\neq v]\!]\}_{v\in[m]}$ contains all clauses containing all of the variables $S_{u,i,b}$ . Hence they can be cut in $O(m\log m)$ -many steps to obtain $\bot$ . Throughout the proof we will write the

\frac{D_{v}\vee[\![S_{u,i}\neq v]\!],\ \forall v}{D}

as a shorthand for this derivation with $D=\bigvee_{v\in[m]}D_{v}$ .

Proof of Lemma 35.

By Lemma 29 it suffices to show that ${\mathsf{Res}}({\mathsf{polylog}})$ can prove ${\text{Iter}}_{2}$ . By induction from $u=m$ to $u=1$ , we will derive a set of formulas that state that does not point forward in $\tilde{S}$ . Combining this with the fact that the image of $u$ by $\tilde{S}$ cannot be undefined and $u$ may not point backwards, this is semantically equivalent to stating that $u$ points to itself. We then reach a contradiction when reaching $u=1$ , since $1$ must be a proper source of our graph. This will be achieved by deducing

L_{u}\leavevmode\nobreak\ :=\leavevmode\nobreak\ \big{\{}[\![\tilde{S}_{u}\neq v% ]\!]:u<v\big{\}},

which can be combined with axioms stating that no node points backwards for the desired statement.

The base case is trivial, as $L_{m}=\emptyset$ . Consider some $u\in[m]$ and suppose that we have derived $L_{v}$ for all $v>u$ . We derive the formula $[\![\tilde{S}_{u}\neq v]\!]\in L_{u}$ as follows: Consider some $w>v>u$ and apply the reverse cut rule to $[\![\tilde{S}_{v}\neq w]\!]$ in order to obtain $[\![\tilde{S}_{v}\neq w]\!]\lor[\![\tilde{S}_{u}\neq v]\!]$ . Now consider the cuts from $a=t$ to $a=2$ ,

\frac{[\![\tilde{S}_{u}\neq w]\!]\vee\bigvee_{i<a+1}[\![S_{v,i}\neq v]\!]% \qquad[\![\tilde{S}_{u}\neq v]\!]\vee[\![S_{v,a}\neq v]\!]\qquad[\![S_{v,1}% \neq w]\!]\vee[\![S_{v,a}\neq w^{\prime}]\!],\forall w^{\prime}\neq v,w}{[\![% \tilde{S}_{u}\neq v]\!]\vee\bigvee_{i<a}[\![S_{v,i}\neq v]\!]}

to the set of formulas $[\![\tilde{S}_{u}\neq v]\!]\vee[\![S_{v,1}\neq w]\!]$ . Finally, we do one last cut:

\frac{[\![\tilde{S}_{u}\neq v]\!]\vee[\![S_{v,1}\neq w]\!],\ \forall w>v\qquad% [\![\tilde{S}_{u}\neq v]\!]\vee[\![S_{v,1}\neq v]\!]\qquad[\![S_{v,1}\neq w]\!% ],\ \forall w<v}{[\![\tilde{S}_{u}\neq v]\!]},

which derives the formula $[\![\tilde{S}_{u}\neq v]\!]\in L_{u}$ .

Finally, once we have derived $L_{1}$ , we can derive $\bot$ as follows. For a fixed $v>1$ , starting from $a=t$ down to $a=2$ , we operate the cuts:

\frac{\bigvee_{i<a+1}[\![S_{1,i}\neq v]\!]\qquad[\![S_{1,a}\neq 1]\!]\qquad[\!% [S_{1,1}\neq v]\!]\vee[\![S_{1,n}\neq v^{\prime}]\!],\ \forall v^{\prime}\neq v% ,1}{\bigvee_{i<a}[\![S_{1,i}\neq v]\!]}.

Once we have derived $[\![S_{1,1}\neq v]\!]$ , we do one final cut:

\frac{[\![S_{1,1}\neq v]\!],\ \forall v\neq 1\qquad[\![S_{1,1}\neq 1]\!]}{\bot}\

$\hfill\blacktriangleleft$

6.2 Circular and Reversible DNF Resolution

In this section we characterize the $\Sigma_{2}$ - ${\mathsf{uCircRes}}({\mathsf{polylog}})$ proof system by a ${\mathsf{TF}}\Sigma_{2}$ -variant of the Sink-of-Line problem. An instance of Sink-of-Line is given by functions $S,P:[m]\times[t]\rightarrow[m]\cup\{undefined\}$ which define a graph $G$ as follows: there is a directed edge $(u,v)$ if $\tilde{S}(u)=v$ and $\tilde{P}(v)=u$ . A solution to this instance is either i) $1$ if $1$ is not a source in $G$ , ii) a sink $u$ in $G$ , iii) a vertex $u$ for which $\tilde{P}(u)$ or $\tilde{S}(u)$ is undefined. We now describe the ${\mathsf{TF}}\Sigma_{2}$ variant.

Definition 36.

An instance of ${\text{SoL}}_{2}$ is given by functions $S,P:[m]\times[t]\rightarrow[m]$ . A solution is a witness to a solution to the SoL instance defined by the meta-pointers $(\tilde{S},\tilde{P})$ :

$\blacksquare$

$(u,i,i^{\prime})$ if $S(u,i),S(u,i^{\prime})\neq u$ and $S(u,i)\neq S(u,i^{\prime})$ ;
or $P(u,i),P(u,i^{\prime})\neq u$ and $P(u,i)\neq P(u,i^{\prime})$ . (Predecessor or Successor of $u$ is undefined)
$\blacksquare$

$(1,i)$ if $S(1,i)=1$ or $\tilde{S}(1)=v\neq 1$ and $P(v,i)\neq 1$ . ( $1$ is not a source)
$\blacksquare$

$(u,i)$ if $u\neq 1$ and $S(u,i)=1$ . ( $u$ has a pointer to $1$ )
$\blacksquare$

$(u,v,i)$ for $u\neq v$ if $\tilde{S}(u)=v$ , $\tilde{P}(v)=u$ and $S(v,i)=v$ ;
or $\tilde{S}(u)=v,\tilde{P}(v)=u,\tilde{S}(v)=w$ and $P(w,i)\neq v$ . ( $v$ is a proper sink)

Theorem 37.

For any ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{2}$ , there is a complexity- $c$ ${\text{SoL}}_{2}$ -formulation of ${\text{FF}}_{F}$ iff there is a complexity $O(c)$ $\Sigma_{2}$ - ${\mathsf{uCircRes}}({\mathsf{polylog}})$ proof of $F$ .

This theorem follows by combining Lemma 38 and Lemma 42. We begin with the backwards direction, showing that ${\mathsf{uCircRes}}({\mathsf{polylog}})$ can prove ${\text{SoL}}_{2}$ formulations. ${\text{SoL}}_{2}$ is encoded as an unsatisfiable formula which is the conjunction of the following

$\blacksquare$

$[\![S_{u,i}\neq 1]\!]$ for $u\in[m],i\in[t]$ , and $[\![\tilde{S}_{1}\neq v]\!]\lor[\![P_{u,i}\neq v]\!]$ for all $u,v\neq 1,i\in[t]$ . ( $1$ is a source)
$\blacksquare$

$[\![S_{u,i}\neq v]\!]\lor[\![S_{u,i^{\prime}}\neq v^{\prime}]\!]$ for all $i\neq i^{\prime}$ , $v\neq v^{\prime}$ . ( $\tilde{S}$ is not undefined)
$\blacksquare$

$[\![P_{u,i}\neq v]\!]\lor[\![P_{u,i^{\prime}}\neq v^{\prime}]\!]$ for all $i\neq i^{\prime}$ , $v\neq v^{\prime}$ . ( $\tilde{P}$ is not undefined)
$\blacksquare$

$[\![S_{u,i}\neq 1]\!]$ for all $i\in[t]$ and $u\neq 1$ . (Nothing points to $1$ )
$\blacksquare$
Let $\bar{E}_{u,v}:=[\![\tilde{S}_{u}\neq v]\!]\lor[\![\tilde{P}_{v}\neq u]\!]$ , we include (No proper sinks)
- –
  
  $\bar{E}_{u,v}\lor[\![S_{v,i}\neq v]\!]$ for each $u\neq v$ and $i\in[m]$ , and
- –
  
  $\bar{E}_{u,v}\lor[\![\tilde{S}_{v}\neq w]\!]\lor[\![P_{w,k}\neq w^{\prime}]\!]$ for $u\neq v\neq w\neq w^{\prime}$ and $k\in[t]$ .

Lemma 38.

For ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{2}$ , if there is a ${\text{SoL}}_{2}$ -formulation of ${\text{FF}}_{F}$ of complexity $c$ then there is a complexity $O(c)$ $\Sigma_{2}$ - ${\mathsf{uCircRes}}({\mathsf{polylog}})(F)$ proof of $F$ .

Proof.

By Lemma 29, it suffices to show that ${\mathsf{uCircRes}}({\mathsf{polylog}})$ can prove ${\text{SoPL}}_{2}$ . For each $u\in[m]$ , we would like to derive the set of formulas

L_{u}=\{\bar{E}_{u,v}:v\neq u,1\},

stating that $u$ has no outgoing edges. Our proof will proceed by the following three steps:

1.

Assume $L_{u}$ for each $u\neq 1$ ;
2.

From $L_{v}$ for $v\neq u$ , deduce $L_{u}$ . Since $L_{v}$ is semantically equivalent to saying that node $v$ points to itself, if $u$ were to point to any other node, then said node would be a proper sink. Hence $L_{u}$ follows.
3.

$L_{1}$ is in direct contradiction with axioms stating that $1$ is a source.

For step 1, we use the DNF creation rule,

\frac{}{\bar{E}_{u,v}}

For step 2 and $u\in[m]$ , we perform the following. For $w\neq v\neq u$ with $w,v\neq 1$ , consider $\bar{E}_{v,w}\in L_{v}$ and weaken it successively to get

\frac{}{\bar{E}_{u,v}\vee\bar{E}_{v,w}},

then we cut as follows: starting with $c=n$ down to $c=1$ ,

\frac{\bar{E}_{u,v}\vee[\![\tilde{S}_{v}\neq w]\!]\vee\bigvee_{k<c+1}[\![P_{w,% k}\neq v]\!]\qquad\bar{E}_{u,v}\vee[\![\tilde{S}_{v}\neq w]\!]\vee[\![P_{w,c}% \neq w^{\prime}]\!],\ \forall w^{\prime}\neq w}{\bar{E}_{u,v}\vee[\![\tilde{S}% _{v}\neq w]\!]\vee\bigvee_{k<c}[\![P_{w,k}\neq v]\!]}

to get $\bar{E}_{u,v}\vee[\![\tilde{S}_{v}\neq w]\!]$ . Next, starting from $b=n$ down to $b=2$ ,

\frac{\bar{E}_{u,v}\vee\bigvee_{j<b+1}[\![S_{v,j}\neq w]\!]\qquad\bar{E}_{u,v}% \vee[\![S_{v,b}\neq v]\!]\qquad[\![S_{v,1}\neq w]\!]\vee[\![S_{v,b}\neq w^{% \prime}]\!],\ \forall w^{\prime}\neq v,w}{\bar{E}_{u,v}\vee\bigvee_{j<b}[\![S_% {v,j}\neq w]\!]}

and end up with the formulas $\bar{E}_{u,v}\vee[\![S_{v,1}\neq w]\!]$ . Finally,

\frac{\bar{E}_{u,v}\vee[\![S_{v,1}\neq w]\!],\ \forall w\neq v,1\qquad\bar{E}_% {u,v}\vee[\![S_{v,1}\neq v]\!]\qquad[\![S_{v,1}\neq 1]\!]}{\bar{E}_{u,v}}

derives $\tilde{E}_{u,v}\in L_{u}$ . Having derived $L_{1}$ allows us to take $\bar{E}_{1,v}\in L_{1}$ and, starting with $b=n$ down to $b=1$ , we may cut:

\frac{[\![\tilde{S}_{1}\neq v]\!]\vee\bigvee_{j<b+1}[\![P_{v,j}\neq 1]\!]% \qquad[\![\tilde{S}_{1}\neq v]\!]\vee[\![P_{v,b}\neq w]\!],\ \forall w\neq 1}{% [\![\tilde{S}_{1}\neq v]\!]\vee\bigvee_{j<b}[\![P_{v,j}\neq 1]\!]}

to get $[\![\tilde{S}_{1}\neq v]\!]$ for each $v\neq 1$ . Next, starting from $a=n$ down to $a=2$ , we cut:

\frac{\bigvee_{i<a+1}[\![S_{1,i}\neq v]\!]\qquad[\![S_{1,a}\neq 1]\!]\qquad[\!% [S_{1,1}\neq v]\!]\vee[\![S_{1,a}\neq v^{\prime}]\!],\ \forall v^{\prime}\neq v% }{\bigvee_{i<a}[\![S_{1,a}\neq v]\!]}

to get $[\![S_{1,1}\neq v]\!]$ for $v\neq 1$ . We may then cut one final time,

\frac{[\![S_{1,1}\neq v]\!],\ \forall v\neq 1\qquad[\![S_{1,1}\neq 1]\!]}{\bot% }.\

$\hfill\blacktriangleleft$

We delay the proof of the other direction until the end of this section and complete it together with the proof of the same direction ${\mathsf{RevRes}}({\mathsf{polylog}})$ as they are similar.

We characterize the ${\mathsf{RevRes}}({\mathsf{polylog}})$ by a ${\mathsf{TF}}\Sigma_{2}$ variant of the Sink-of-Potential-Line (SoPL) problem. This is a metered variant of SoL, meaning that edges must always point towards larger numbers. An instance of SoPL is given by functions $S,P:[m]\rightarrow[m]\cup\{undefined\}$ that define a graph $G$ with edges $(u,v)$ iff $S(u)=v$ and $P(v)=u$ . A solution is either i) $1$ if $1$ is not a source in $G$ , ii) a sink $u$ in $G$ , iii) a vertex which points backwards $S(u)<u$ , or iv) a vertex $u$ if $S(u)$ or $P(u)$ is undefined.

Definition 39.

An instance of ${\text{SoPL}}_{2}$ is given by functions $S,P:[m]\times[t]\rightarrow[m]$ . A solution is a witness to a solution to the SoPL instance defined by the meta-pointers $(\tilde{S},\tilde{P})$ :

$\blacksquare$

$(u,i,i^{\prime})$ if $S(u,i),S(u,i^{\prime})\neq u$ and $S(u,i)\neq S(u,i^{\prime})$ ;
or $P(u,i),P(u,i^{\prime})\neq u$ and $P(u,i)\neq P(u,i^{\prime})$ .
a (Predecessor or Successor of $u$ is undefined)
$\blacksquare$

$(1,i)$ if $S(1,i)=1$ or $\tilde{S}(1)=v\neq 1$ and $P(v,i)\neq 1$ . ( $1$ is not a source)
$\blacksquare$

$(u,i)$ if $S(u,i)<u$ . ( $u$ points backwards)
$\blacksquare$

$(u,v,i)$ for $u<v$ if $\tilde{S}(u)=v$ , $\tilde{P}(v)=u$ and $S(v,i)=v$ ; or $\tilde{S}(u)=v,\tilde{P}(v)=u,\tilde{S}(v)=w$ and $P(w,i)\neq v$ . a ( $v$ is a proper sink)

Theorem 40.

For any ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{2}$ , there is a complexity- $c$ ${\text{SoPL}}_{2}$ -formulation of ${\text{FF}}_{F}$ iff there is a complexity $O(c)$ $\Sigma_{2}$ - ${\mathsf{RevRes}}({\mathsf{polylog}})$ proof of $F$ .

This theorem follows by combining Lemma 41 and Lemma 42. We begin with the backwards direction, showing that ${\mathsf{RevRes}}({\mathsf{polylog}})$ can prove ${\text{SoPL}}_{2}$ formulations. ${\text{SoPL}}_{2}$ is encoded as an unsatisfiable formula, which is the conjunction of the following:

$\blacksquare$

$[\![S_{u,i}\neq 1]\!]$ for $u\in[m],i\in[t]$ , and $[\![\tilde{S}_{1}\neq v]\!]\lor[\![P_{u,i}\neq v]\!]$ for all $u,v\neq 1,i\in[t]$ . ( $1$ is a source)
$\blacksquare$

$[\![S_{u,i}\neq v]\!]\lor[\![S_{u,i^{\prime}}\neq v^{\prime}]\!]$ for all $i\neq i^{\prime}$ , $v\neq v^{\prime}$ . ( $\tilde{S}$ is not undefined)
$\blacksquare$

$[\![P_{u,i}\neq v]\!]\lor[\![P_{u,i^{\prime}}\neq v^{\prime}]\!]$ for all $i\neq i^{\prime}$ , $v\neq v^{\prime}$ . ( $\tilde{P}$ is not undefined)
$\blacksquare$

$[\![S_{u,i}\neq v]\!]$ for all $i\in[t]$ and $v<u$ . (No backwards edges)
$\blacksquare$
Let $\bar{E}_{u,v}:=[\![\tilde{S}_{u}\neq v]\!]\lor[\![\tilde{P}_{v}\neq u]\!]$ , we include (No proper sinks)
1. i)
  
  $\bar{E}_{u,v}\lor[\![S_{v,i}\neq v]\!]$ for each $u<v$ and $j\in[m]$ , and
2. ii)
  
  $\bar{E}_{u,v}\lor[\![\tilde{S}_{v}\neq w]\!]\lor[\![P_{w,k}\neq w^{\prime}]\!]$ for $u<v<w$ and $w\neq w^{\prime}$ and $k\in[t]$ .

Lemma 41.

For ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{2}$ , if there is a ${\text{SoPL}}_{2}$ -formulation of ${\text{FF}}_{F}$ of complexity $c$ , then there is a complexity $O(c)$ $\Sigma_{2}$ - ${\mathsf{RevRes}}({\mathsf{polylog}})(F)$ proof of $F$ .

Proof.

By Lemma 29, it suffices to show that ${\mathsf{RevRes}}({\mathsf{polylog}})$ can prove ${\text{SoPL}}_{2}$ . We will prove by induction on $u=m\ldots 1$ that $u$ does not have any outgoing edges. That is, we will derive the set of formulas:

L_{u}\leavevmode\nobreak\ :=\leavevmode\nobreak\ \big{\{}\bar{E}_{u,v}:u>v\big% {\}}.

First observe that the base case is given by the no backwards edges axioms. Assuming that we can derive $L_{1}$ , we show how to complete the proof. For $v>1$ , starting with $b=n$ down to $b=1$ , we cut

\frac{[\![\tilde{S}_{1}\neq v]\!]\vee\bigvee_{j<b+1}[\![P_{v,j}\neq 1]\!]% \qquad[\![\tilde{S}_{1}\neq v]\!]\vee[\![P_{v,b}\neq w]\!],\ \forall w\neq 1}{% [\![\tilde{S}_{1}\neq v]\!]\vee\bigvee_{j<b}[\![P_{v,j}\neq 1]\!]}.

Next, starting from $a=n$ down to $a=2$ , we successively cut

\frac{\bigvee_{i<a+1}[\![S_{1,i}\neq v]\!]\qquad[\![S_{1,a}\neq 1]\!]\qquad[\!% [S_{1,1}\neq v]\!]\vee[\![S_{1,a}\neq w]\!],\ \forall w\neq 1,v}{\bigvee_{i<a}% [\![S_{1,i}\neq v]\!]}.

Once all those formulas are derived, we cut one final time to finish the proof

\frac{[\![S_{1,1}\neq 1]\!]\qquad[\![S_{1,1}\neq v]\!],\ \forall v>1}{\bot}.

We now describe how to derive $L_{u}$ from all $L_{v}$ with $v>u$ . For a given $v$ and $\bar{E}_{v,w}\in L_{v}$ , we start by weakening it to get $[\![\tilde{P}_{v}\neq u]\!]\vee\bar{E}_{v,w}$ and again to get $\bar{E}_{u,v}\vee\bar{E}_{v,w}$ . Once this is done, starting at $c=n$ down to $k=1$ , we cut

\frac{\bar{E}_{u,v}\vee[\![\tilde{S}_{v}\neq w]\!]\vee\bigvee_{k<c+1}[\![P_{w,% k}\neq v]\!]\qquad\bar{E}_{u,v}\vee[\![\tilde{S}_{v}\neq w]\!]\vee[\![P_{v,c}% \neq w^{\prime}]\!],\ \forall w^{\prime}\neq w}{\bar{E}_{u,v}\vee[\![\tilde{S}% _{v}\neq w]\!]\vee\bigvee_{k<c}[\![P_{w,k}\neq v]\!]}

to get $\bar{E}_{u,v}\vee[\![\tilde{S}_{v}\neq w]\!]$ . Finally, from $b=n$ down to $b=2$ , we cut

\frac{\bar{E}_{u,v}\vee\bigvee_{j<b+1}[\![S_{v,j}\neq w]\!]\qquad\bar{E}_{u,v}% \vee[\![S_{v,b}\neq v]\!]\qquad[\![S_{v,1}\neq w]\!]\vee[\![S_{v,c}\neq w]\!],% \ \forall w^{\prime}\neq v,w}{\bar{E}_{u,v}\vee\bigvee_{j<b}[\![S_{v,j}\neq w]% \!]}.

Once we derived $\bar{E}_{u,v}\vee[\![S_{v,1}\neq w]\!]$ for each $w>v$ , we have one final cut

\frac{\bar{E}_{u,v}\vee[\![S_{v,1}\neq w]\!],\ \forall w>v\qquad\bar{E}_{u,v}% \vee[\![S_{v,1}\neq v]\!]\qquad[\![S_{v,1}\neq w]\!],\ \forall w<v}{\bar{E}_{u% ,v}}

to get $\bar{E}_{u,v}\in L_{u}$ . $\hfill\blacktriangleleft$

Finally, we prove the other direction of Theorem 40 and Theorem 37.

Lemma 42.

Let ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{2}$ . Suppose that $F$ admits a complexity- $c$ $\Sigma_{2}$ - ${\mathsf{uCircRes}}({\mathsf{polylog}})$ ( $\Sigma_{2}$ - ${\mathsf{RevRes}}({\mathsf{polylog}})$ ) proof. Then there is a complexity- $O(c)$ ${\text{SoL}}_{2}$ -( ${\text{SoPL}}_{2}$ -)formulation of ${\text{FF}}_{F}$ .

Proof.

We first handle Circular DNF Resolution and discuss what needs to be changed in order to handle Reversible DNF Resolution at the end of the proof. The idea for the transformation of a ${\mathsf{uCircRes}}({\mathsf{polylog}})$ proof into an ${\text{SoL}}_{2}$ formulation is the same as the transformation of a ${\mathsf{Res}}({\mathsf{polylog}})$ into an ${\text{Iter}}_{2}$ formulation (Lemma 33) with the addition of defining a predecessor function. Let $\Pi=(D_{1},\ldots,D_{m})$ be such a proof. By padding, we may assume that each DNF in the proof has the same number of terms. Let us consider the proof in reverse order such that $D_{1}=\bigvee_{i\in[t]}\bot$ .

Let $t_{u,i}$ be the $i^{th}$ term of $D_{u}$ . Given an assignment $\alpha\in\{0,1\}^{n}$ to the variables of $F$ , we construct a function $S_{\alpha}:[m]\times[t]\rightarrow[m]$ by setting $S_{\alpha}(u,i)$ to be:

$\blacksquare$

$u$ if $D_{u}$ is an axiom, or if $t_{u,i}(\alpha)=1$ ;
$\blacksquare$

$v$ if $t_{u,i}(\alpha)=0$ and $D_{u}$ was derived from $D_{v}$ by the reverse cut rule or semantic weakening of an axiom;
$\blacksquare$

$v$ if $t_{u,i}(\alpha)=0$ and $D_{u}$ was derived from $D_{v}=D_{u}\vee t$ and $D_{w}=D_{u}\vee\bar{t}$ via symmetric cut and $t(\alpha)=0$ and $w$ if $\bar{t}(\alpha)=0$ ;

As well, define the predecessor function $P_{\alpha}:[m]\times[t]\rightarrow[m]$ , as $P_{\alpha}(u,i)$ :

$\blacksquare$

$u$ if either $u=1$ , or the formula $D_{u}$ was deduced but never used as the premise of a rule, or if $t_{u,i}(\alpha)=1$ ;
$\blacksquare$

$v$ if $t_{u,i}(\alpha)=0$ and $u$ is used as a premise to derive $D_{v}$ via any of the rules but the reverse cut;
$\blacksquare$

$v$ or $w$ if $t_{u,i}(\alpha)=0$ and $D_{u}$ was used as the premise of the reverse cut rule to derive $D_{v}=D_{u}\vee t$ and $D_{w}=D_{u}\vee\bar{t}$ . If $t(\alpha)=0$ , then $P_{\alpha}(u,i)=v$ and $P_{\alpha}(u,i)=w$ otherwise.

Finally, for each solution $o$ to the instance $S_{\alpha}$ , we define the output of the reduction $g_{o}(\alpha)$ to be arbitrary if $o$ does not correspond to an axiom $A_{i}$ of $H$ , and otherwise this axiom $A_{i}$ is a weakening of a DNF $F_{j}$ of $F$ , and we set $g_{o}(\alpha)=j$ . Note that in this case $A_{i}(\alpha)=0\implies F_{j}(\alpha)=0$ . Observe that computing $S_{\alpha}(u,i)$ and $P_{\alpha}(u,i)$ involves evaluating at most two terms, and hence the reduction is efficient.

It remains to argue that the reduction is correct.

Claim 43.

The following hold:

i)

$\tilde{P}_{\alpha}$ and $\tilde{S}_{\alpha}$ are defined everywhere;
ii)

If $D_{u}$ was used as the premise of a rule, $D_{u}(\alpha)=0$ if and only if $\tilde{P}_{\alpha}(u)\neq u$ and $\tilde{S}_{\alpha}(u)\neq u$ ;
iii)

If $\tilde{P}_{\alpha}(u)=v\neq u$ , then $D_{v}(\alpha)=0$ ;
iv)

For a pair $u\neq v$ , $\tilde{S}_{\alpha}(u)=v$ if and only if $\tilde{P}_{\alpha}(v)=u$ .

Assuming the claim, the only solutions are proper sinks corresponding to falsified axioms of $H$ , which are weakenings of (falsified) axioms of $F$ . Hence, $g$ returns a correct solution to ${\text{FF}}_{F}(\alpha)$ .

Proof of Claim..

The proof of this claim is, at heart, the same as the proof of the claim in Lemma 33. The behavior of both functions implies that the only solutions one might get in the instance are proper sinks and that these proper sinks can only be falsified axioms. Finally, when $\Pi$ is a ${\mathsf{RevRes}}({\mathsf{polylog}})$ proof, $S_{\alpha}(u,i)\geq u$ and $P_{\alpha}(v,j)\leq v$ for any $u$ and $v$ since the graph representation of $\Pi$ does not include cycles, and thus we would not have fake solutions corresponding to edges pointing backwards, making our formulation a valid ${\text{SoPL}}_{2}$ -formulation. $\hfill\vartriangleleft$ $\hfill\blacktriangleleft$

6.3 Relationships in ${\mathsf{TF}}\Sigma_{2}$

In this subsection, we use the characterizations that we have constructed in order to prove all of the new inclusions in Figure 1. We begin by giving a ${\mathsf{uCircRes}}$ proof of the unmetered source-of-DAG problem, which is equivalent to StrongAvoid. USoD is encoded propositionally by the conjunction of the following formulas:

$\blacksquare$

$[\![S_{1}=1]\!]$ and $\bigvee_{t\in[n]}[\![S_{t}=1]\!]$ . (1 is a sink);
$\blacksquare$

$\bigvee_{t\in[n]}[\![S_{t}=u]\!]$ for all $u\neq 1$ . ( $u$ is not a source).

Proposition 44.

USoD has a ${\mathsf{polylog}}(n)$ -complexity ${\mathsf{uCircRes}}({\mathsf{polylog}}(n))$ -proof and so ${\text{StrongAvoid}}\in{\mathsf{SOL}}_{2}$ .

Proof.

The strategy for the proof is:

i)

Assume that $S(u)=u$ for any $u\neq 1$ ;
ii)

From the fact that $S(v)=v$ for all $v\neq u$ , deduce that $S(u)=u$ . Indeed if all other nodes point to themselves, $u$ can not point to anything but itself since otherwise it would qualify as a source. We also derive $S(u)\neq 1$ during this process;
iii)

Once this is done, we will be left with the fact that $S(u)\neq 1$ for each $u\neq 1$ which is in direct contradiction with the second axiom.

For step (i), we introduce $[\![S_{u}=u]\!]$ for each $u\neq 1$ via the DNF creation rule. Now, fixing some such $u$ , for $t\neq u$ , we weaken $[\![S_{t}=t]\!]$ to $[\![S_{t}=t]\!]\vee[\![S_{u}\neq w]\!]$ for each $w\in[n]$ and consider the case $w=t$ . Since $u\neq t$ , the formula $[\![S_{t}\neq t]\!]\vee[\![S_{u}\neq t]\!]$ is a tautology, and therefore we can introduce it. For each $t\neq u$ we cut

\frac{[\![S_{t}=t]\!]\vee[\![S_{t}\neq u]\!]\qquad[\![S_{t}\neq t]\!]\vee[\![S% _{t}\neq u]\!]}{[\![S_{t}\neq u]\!]}.

Then, cutting

\frac{\bigvee_{t}[\![S_{t}=u]\!]\qquad[\![S_{t}\neq u]\!],\ \forall t\neq u}{[% \![S_{u}=u]\!]}

From $[\![S_{u}=u]\!]$ we can deduce $[\![S_{u}\neq 1]\!]$ , completing step (ii).

Finally, we can perform step (iii) by cutting

\frac{\bigvee_{u\neq 1}[\![S_{u}=1]\!]\qquad[\![S_{u}\neq 1]\!],\ \forall u% \neq 1}{\bot}

The size of the proof and the characterization theorem shows that ${\text{USoD}}\in{\mathsf{SOL}}_{2}$ . Also, the equivalence ${\text{USoD}}=_{dt}{\text{StrongAvoid}}$ gives us ${\text{StrongAvoid}}\in{\mathsf{SOL}}_{2}$ $\hfill\blacktriangleleft$

The sink-of-DAG problem is the canonical ${\mathsf{PLS}}$ -complete problem in which one is given a source of a DAG and one wants to find a sink. Our characterization of unary Sherali-Adams by StrongAvoid proceeded via the equivalent unmetered source-of-DAG problem. Hence, it is natural to also consider a metered version of these problem, where one is given a sink of a DAG and one wants to find a source.

Definition 45.

The Source of DAG (SoD) problem is defined as follows. The input is a “successor” function $S:[n]\rightarrow[n]$ which defines a graph in which each vertex has fan-out $\leq 1$ but arbitrary fan-in. There is an edge from $i$ to $j$ if $S(i)=j$ . A solution to the instance $S$ is:

i)

$i$ if $S(i)<i$ ; ( $i$ has a backward edge)
ii)

$n$ if for all $i<n$ , $S(i)\neq n$ ; ( $n$ is not a sink)
iii)

$i$ if for all $j\in[n]$ , $S(j)\neq i$ . (A source)

We can encode SoD propositionally as the conjunction of the following formulas:

i)

$\bigvee_{t\neq n}[\![S_{t}=n]\!]$ ; ( $n$ is a proper sink)
ii)

$\bigvee_{t}[\![S_{t}=u]\!]$ for each $u\neq 1$ ; (no sources)
iii)

$[\![S_{u}\neq v]\!]$ for any pair of nodes $v<u$ . (no edges pointing backwards)

Proposition 46.

There is a ${\mathsf{polylog}}(n)$ -complexity ${\mathsf{RevRes}}({\mathsf{polylog}}(n))$ proof of ${\mathsf{SOD}}$ , and hence ${\text{SoD}}\in{\mathsf{SOPL}}_{2}$ .

Proof.

The strategy of the proof is as follows:

i)

Given that $S(t)=t$ for each $t<u$ , deduce that $S(u)=u$ . This must be true since otherwise $u$ is a source.
ii)

Use the fact that the derived formulas directly contradicts the first axiom.

For step (i), by induction assume that we have derived $[\![S_{t}=t]\!]$ for each $t<u$ . Weaken these formulas to get $[\![S_{t}=t]\!]\vee[\![S_{t}\neq v]\!]$ and consider the case when $v=u$ . Since $t\neq u$ , the formula $[\![S_{t}\neq t]\!]\vee[\![S_{t}\neq u]\!]$ is a tautology that we introduce, and we cut

\frac{[\![S_{t}\neq t]\!]\vee[\![S_{t}\neq u]\!]\qquad[\![S_{t}=t]\!]\vee[\![S% _{t}\neq u]\!]}{[\![S_{t}\neq u]\!]}

to obtain $[\![S_{t}\neq u]$ . Next, we cut

\frac{\bigvee_{t}[\![S_{t}=u]\!]\qquad[\![S_{t}\neq u]\!],\ \forall t<u\qquad[% \![S_{t}\neq u]\!],\forall t>u}{[\![S_{u}=u]\!]}

to derive $[\![S_{u}=u]\!]$ . Fianlly, cut

\frac{\bigvee_{t\neq n}[\![S_{t}=n]\!]\qquad[\![S_{t}\neq n]\!],\ \forall t% \neq n}{\bot}

hence ${\text{SoD}}\in{\mathsf{SOPL}}_{2}$ . $\hfill\blacktriangleleft$

Observe that these proofs indicate that up to complexifying a function, it is possible to build an inverse that is also hard to compute with an efficient reduction. Also, since we know how to transform ${\mathsf{uCircRes}}({\mathsf{polylog}})$ refutations (resp. ${\mathsf{RevRes}}({\mathsf{polylog}})$ refutations) into ${\text{SoL}}_{2}$ -instances (resp. ${\text{SoPL}}_{2}$ -instances), following the instructions lets us concretely build those inverses.

We end this section by proving several inclusions which do not rely on our characterizations.

Proposition 47.

${\text{LOP}}\leq_{dt}{\text{Iter}}_{2}$ .

Proof.

Let $\prec$ be an LOP instance on $[n]$ . By encoding it with $\binom{n}{2}$ variables such that, for $i<j\in[n]$ , $x_{i,j}=1$ means $i\prec j$ , and $x_{i,j}=0$ means $j\prec i$ , we can force the purported order to always be total. An output to the LOP instance would thus either be a $\prec$ -minimal element or a proof that $\prec$ is not an order, i.e., that the transitivity does not hold.
Consider the ${\text{Iter}}_{2}$ instance on $\binom{n}{2}+n$ meta-nodes with a meta-node for each $(i,j)\in[n]^{2}$ with $i\geq j$ . Let $(1,1)$ be the source. It helps to think of the meta-nodes as arranged in $n$ levels, with the first element in the label being the level a meta-node is at.

The idea is that $(i,j)$ is valid (i.e., has an outgoing edge) iff $\prec$ is transitive and $j$ is the $\prec$ -minimal value in $[i]$ . If $i<n$ , it will point to $(i+1,j^{\prime})$ , where $j^{\prime}=j$ if $j$ is still $\prec$ -minimal in $[i+1]$ , and $j^{\prime}=i+1$ otherwise. We now formally define the nodes with index $(i,j)$ . If $i=n$ , then it contains a single node that points to itself. Otherwise, there are two kinds of nodes:

Transitivity nodes.

$\binom{n}{3}$ -many nodes verifying the transitivity of $\prec$ . Each of those nodes is associated with 3 distinct elements $(a,b,c)\in[n]^{3}$ . We define $S((i,j),(a,b,c))$ as follows:

$\blacksquare$

Query $a\prec b$ , $b\prec c$ and $a\prec c$ . If the answers show that $\prec$ is not transitive on $(a,b,c)$ , point to $(i,j)$ .
$\blacksquare$

Query $j\prec i+1$ . If it holds, point to $(i+1,j)$ . Otherwise, point to $(i+1,i+1)$ .

Validity nodes.

$(i-1)$ -many nodes verifying the validity of $(i,j)$ . Each of those nodes is associated with a value $k\in[i]\setminus\{j\}$ . We define $S((i,j),k)$ as follows:

$\blacksquare$

Query $j\prec k$ . If it does not hold, point to $(i,j)$ .
$\blacksquare$

Query $j\prec i+1$ . If it holds, point to $(i+1,j)$ ; otherwise, point to $(i+1,i+1)$ .

Since every node that points out of its index does the same query to decide where to point, the meta successor is well-defined. If $\prec$ is not transitive, every meta-node will point to itself. The solution can thus only be of type $((1,1),i)$ , with this node being of the transitive type. This immediately gives us a triple in $[n]$ , proving $\prec$ is not transitive. If $\prec$ is indeed a total order, then it is clear that every level has a single active node; the only proper sink on level $n$ indicates the $\prec$ -minimal value in $[n]$ . $\hfill\blacktriangleleft$

Proposition 48.

${\text{SoD}}\leq_{dt}{\text{LOP}}$ .

Proof.

Let $S$ be an SoD instance on $n$ vertices. Consider an LOP instance $\prec$ on $2n$ values split into two groups $C=[n]$ and $L=[n]$ . We denote elements of $C$ by $i_{C}$ and elements of $L$ by $i_{L}$ , for $i\in[n]$ . The group $C$ ’s goal is to “check for backward pointers”; if the $\prec$ -minimal element is $i_{C}$ , then $i$ points backwards. The group $L$ checks for loops: if the $\prec$ -minimal element is $i_{L}$ , then there are no backward edges. Moreover, if $i=n$ , then $n$ is not a proper sink. Otherwise, $i$ is the first node (in regular order) to not point to itself in $S$ , i.e., $i$ is a source.
Formally, for $i,j\in[n]$ , we define $\prec$ as follows:

$\blacksquare$

$i_{C}\prec j_{C}$ iff $i<j$ ;
$\blacksquare$

$i_{C}\prec j_{L}$ iff $S(i)<i$ ;
$\blacksquare$
$i_{L}\prec j_{L}$ iff either one of the following holds:
1. i)
  
  $S(i_{L})=i$ , $S(j_{L})=j$ and $i>j$ ;
2. ii)
  
  $S(i_{L})\neq i$ and $S(j_{L})=j$ ;
3. iii)
  
  $S(i_{L})\neq i$ , $S(j_{L})\neq j$ and $i<j$ .

Observe that $\prec$ is total. If it is transitive, then the minimal element is either the first source in $S$ , or $n$ if it is not a proper sink. If it is not transitive, the minimal element allows us to find a backward pointer. $\hfill\blacktriangleleft$ Theorem 1 in [14] proves that ${\mathsf{FNP}}\subseteq{\mathsf{PEPP}}$ ; we prove that actually ${\mathsf{FNP}}\subseteq{\mathsf{SOD}}$ . As it is straightforward that SourceofDag reduces to UnmeteredSourceofDag, which is equivalent to empty, this implies that every ${\mathsf{TF}}\Sigma_{2}$ class studied in this paper, apart from ${\mathsf{APEPP}}$ , contains ${\mathsf{FNP}}$ .

Proposition 49.

${\mathsf{FNP}}\subseteq{\mathsf{SOD}}$ .

Proof.

Let $x$ be an instance of $R_{n}$ , an ${\mathsf{FNP}}$ problem, and let $\mathcal{O}$ be its set of solutions. By definition of ${\mathsf{FNP}}$ , this set is of size at most quasipolynomial in $n$ . Consider the SoD instance with $|\mathcal{O}|+1$ nodes. Consider the extra node as $n$ . To define $S(o)$ , run the verifier $T_{o}(x)$ . If it accepts, point to $n$ ; otherwise, point $S(o)$ to itself.

Any solution $o$ for the input $x$ will then point to $n$ , making it a source. The case where $n$ is not a proper sink may occur only if $x$ does not admit an output. $\hfill\blacktriangleleft$

7 Characterizing Bounded-Depth Frege

In this section we prove Theorem 6, introducing a hierarchy of classes in the polynomial hierarchy which characterize bounded-depth Frege systems. Depth- $d$ Frege generalizes resolution to allow one to cut (resolve) over depth $d$ formulas of unbounded fanin. Recall that the depth of a formula is the length of the longest root-to-leaf path, and the size is the number of wires in the formula. The width of a $\Sigma_{d}$ -formula is defined as the maximum fanin among the gates at depth $d$ . From now on and for the remainder of this section, we assume $d\geq 3$ .

Definition 50.

A Frege proof of an unsatisfiable formula $F=\bigwedge_{i=1}^{m}A_{i}$ is a sequence $\Pi=(\pi_{1},\ldots,\pi_{\ell}=\bot)$ of formulas, where each $\pi_{i}$ is deduced from the previously derived formulas by one of the following rules:

$\blacksquare$

Axiom Introduction. Introduce $\pi_{i}=A_{i}$ for some $i\in[m]$ .
$\blacksquare$

Cut. From $C\lor D$ and $\overline{D}\lor H$ derive $C\lor H$ for any formula $D$ .
$\blacksquare$

Weakening. From $C$ derive $C\lor D$ for any formula $D$ .

The depth (resp. width) of a Frege proof is the maximum depth (resp width) among any of the formulas $\pi_{i}\in\Pi$ . In particular, we say that $\Pi$ is a depth- $d$ Frege (which we denote Frege_d) proof if each $\pi_{i}$ is a $\Sigma_{d}$ -formula. The size $|\Pi|$ of the proof is $\sum_{i=1}^{\ell}|\pi|$ . The complexity of a Frege_d proof $\Pi$ is $\mathsf{width}(\Pi)+\log|\Pi|$ , and the complexity of proving an unsatisfiable formula in Frege_d is the minimum complexity of any Frege_d proof of $F$ .

Our characterization will generalize our characterization of $\Sigma_{2}$ - ${\mathsf{Res}}({\mathsf{polylog}})$ by ${\text{Iter}}_{2}$ (Theorem 5). The high-level idea is to obfuscate the successor function of the ${\mathsf{TFNP}}$ problem Iter so that it is efficiently computable with access to a $\Pi_{d-1}$ oracle, but not obviously efficiently computable with any weaker oracle. For ${\text{Iter}}_{2}$ , this was accomplished by replacing each node $v\in[m]$ of Iter with a group of nodes $v_{1},\ldots,v_{t}$ , each with their own successor function, pointing to a “meta-node” in $[m]$ . We then treated $v$ as pointing to a meta-node $u\in[m]$ iff all of $v_{1},\ldots,v_{t}$ pointed to $u$ . To generalize this to a problem in the $d^{th}$ layer of the polynomial hierarchy, which we call ${\text{Iter}}_{d}$ , we will take a slightly different approach. We will still replace the “meta-nodes” of Iter with groups of nodes – in fact, this is recursively repeated $d-1$ times in order to simulate $d$ alternating quantifiers – however, we will no longer insist that they all point to the same node. Instead, the successor will be defined by alternatively taking the minimum (corresponding to universal quantifiers) or maximum (corresponding to existential quantifiers) of the pointed-to nodes. The intuition is that the evaluation of an existentially quantified relation $\exists xF(x)$ is true if some value of $x$ makes $F$ true, hence we should take the maximum value of $F$ over all $x$ . Similarly, the evaluation of universally quantified relation $\forall xF(x)$ should be false unless every assignment makes $x$ output true, and so this corresponds to a minimum value of $F$ over all $x$ . This is inspired by the problems ${\text{GPLS}}_{d}$ and ${\text{PE}}_{d}$ from [23], which characterize the $\forall\Sigma_{1}^{b}$ consequences of $T_{2}^{d}$ in bounded arithmetic.

For an integer $d\geq 1$ , a product set $\mathbf{r}=[r_{1}]\times\cdots\times[r_{d}]$ , and a function $S:[r_{1}]\times\ldots\times[r_{d}]$ we will denote by

	$\displaystyle\mathsf{MAX}(S,\mathbf{r})$	$\displaystyle:=\max_{i_{1}\in[r_{1}]}\min_{i_{2}\in[r_{2}]}\cdots\max_{i_{d}% \in[r_{d}]}S(i_{1},\ldots,i_{d}),$
	$\displaystyle\mathsf{MIN}(S,\mathbf{r})$	$\displaystyle:=\min_{i_{1}\in[r_{1}]}\max_{i_{2}\in[r_{2}]}\cdots\min_{i_{d}% \in[r_{d}]}S(i_{1},\ldots,i_{d}),$

if $d$ is odd, and if $d$ is even, we change the final $\min$ or $\max$ to its opposite. We now formalize the aforementioned intuition about the connection between $\exists/\forall$ quantifiers (that is, $\lor/\land$ gates) and $\max/\min$ which will allow us to connect our Frege proofs to

Observation 51.

Let $F=\bigvee_{i_{1}\in[r_{1}]}\bigwedge_{i_{2}\in[r_{2}]}\cdots\bigcirc_{i_{d}\in% [r_{d}]}F_{\mathbf{i}}$ , where $\mathbf{i}=(i_{1},\ldots,i_{d})$ and each $F_{\mathbf{i}}$ is a formula. Then, for any assignment $x\in\{0,1\}^{n}$ , $F(x)=\mathsf{MAX}(F_{x},\mathbf{r})$ , where $F_{x}(\mathbf{i}):=F_{\mathbf{i}}(x)$ . Similarly, if instead $F$ begins with $\wedge$ , then $F(x)=\mathsf{MIN}(F_{x},\mathbf{r})$ .

Figure 3: An example of how a formula is converted into a sequence of minimums/maximums in Observation 51.

Proof.

The main idea is depicted Figure 3. The proof is by induction on the depth $d$ , observing that a disjunction returns the maximum value of its subformulas, while a conjunction returns the minimum value. $\hfill\blacktriangleleft$

Definition 52.

An instance of ${\text{Iter}}_{d}$ is given by a successor function $S:[m]\times[r_{1}]\times\cdots\times[r_{d-1}]\rightarrow[m]$ that describes a directed graph on $m$ vertices as follows. For $u\in[m]$ , let $S_{u}$ denote the function $S$ where the first input is fixed to $u$ , let $\mathbf{r}=[r_{1}]\times\ldots\times[r_{d-1}]$ , and define the meta-pointer $\tilde{S}:[m]\rightarrow[m]$ as

\tilde{S}(u):=\mathsf{MIN}(S_{u},\mathbf{r}).

There is an edge from $u$ to $v$ in this graph if $\tilde{S}(u)=v$ . A solution to ${\text{Iter}}_{d}$ is then a solution to the Iter instance defined by $\tilde{S}$ . In particular, a solution is a quadruple $(u,i_{1}^{*},v,j_{1}^{*})$ such that $\tilde{S}(u)=v$ and either

i)

$u=v=1$ ( $1$ is not a source);
ii)

$v<u$ ( $u$ admits a backward pointer);
iii)

$u<v$ and $\tilde{S}(u)=\tilde{S}(v)=v$ ( $v$ is a proper sink);

and $i_{1}^{*}$ and $j_{1}^{*}$ witness the outermost minimums for $u$ and $v$ : if $d$ is even

	$\displaystyle i_{1}^{*}$	$\displaystyle=\operatorname*{arg\,min}_{i_{1}\in[r_{1}]}\Big{\{}\max_{i_{2}\in% [r_{2}]}\cdots\min_{i_{d-1}\in[r_{d-1}]}S(u,\mathbf{i})\Big{\}};$
	$\displaystyle j_{1}^{*}$	$\displaystyle=\operatorname*{arg\,min}_{j_{1}\in[r_{1}]}\Big{\{}\max_{j_{2}\in% [r_{2}]}\cdots\min_{j_{d-1}\in[r_{d-1}]}S(v,\mathbf{j})\Big{\}};$

and if $d$ is odd the last $\min$ is replaced by a $\max$ .

The class ${\mathsf{PLS}}_{d}\subseteq{\mathsf{TF}}\Sigma_{d}$ is the class of problems that admit an efficient reduction to ${\text{Iter}}_{d}$ .

One should think of the indices $i_{1}^{*}$ and $j_{1}^{*}$ in a solution to ${\text{Iter}}_{d}$ as the outer-most existential in $\Sigma_{d}$ -certificates of the computation of the successor functions for $u$ and $v$ . One reason that this problem is hard is that for the solutions where $u<v$ , the verifier must be able check that $\tilde{S}(u)=v$ and $\tilde{S}(v)=v$ or, in other words, it must be able to verify that the certificates $i^{*}$ and $j^{*}$ indeed witness a correct computation for their respective input nodes.

Proposition 53.

${\text{Iter}}_{d}\in{\mathsf{TF}}\Sigma_{d}$ for all $d\geq 1$ .

Proof.

Let us assume $d$ is even; the case when $d$ is odd is identical up to changing the final $\min$ into a $\max$ . Let $S$ be an instance of ${\text{Iter}}_{d}$ and $o=(u,i_{1}^{*},v,j_{1}^{*})$ be a solution. Writing $\mathbf{i}=(i_{1},\ldots,i_{d-1})$ , checking that $\tilde{S}(u)=v$ is equivalent to checking that

	$\displaystyle\tilde{S}(u)\geq v$	$\displaystyle\equiv\forall i_{1}\exists i_{2}\cdots\forall i_{d-1}S(u,\mathbf{% i})\ \geq v;$
	$\displaystyle\tilde{S}(u)\leq v$	$\displaystyle\equiv\exists i_{1}\forall i_{2}\cdots\exists i_{d-1}S(u,\mathbf{% i})\leq v.$

Our polynomial-time verifier $V_{o}$ , given witnesses $\mathbf{i}=(i_{2},\ldots,i_{d-1})$ , $\mathbf{j}=(j_{2},\ldots,j_{d-1})$ , $\mathbf{i^{\prime}}=(i^{\prime}_{1},\ldots,i^{\prime}_{d-1})$ , $\mathbf{j^{\prime}}=(j_{1}^{\prime},\ldots,j^{\prime}_{d-1})$ , $V_{o}$ , behaves as follows:

i)

It checks that $S(u,\mathbf{i^{\prime}})\geq v$ and $S(u,i_{1}^{*}\mathbf{i})\leq v$ ; if not, it outputs $0$ ³³3Here, $i_{1}^{*}\mathbf{i}$ denotes the concatonation of $i_{1}^{*}$ with $\mathbf{i}$ .;
ii)

It outputs $1$ if $u<v$ or $u=v=1$ ;
iii)

Otherwise, it checks whether $S(v,\mathbf{j^{\prime}})\geq v$ and $S(v,j_{1}^{*}\mathbf{j})\leq v$ ; if this is the case then it outputs $1$ , and otherwise it outputs $0$ .

Observe that the expression

\forall(i^{\prime}_{1},i_{2},j^{\prime}_{1},j_{2})\exists(i^{\prime}_{2},i_{3}% ,j_{2}^{\prime},j_{3})\cdots\exists(i^{\prime}_{k-2},i_{d-1},j^{\prime}_{k-2},% j_{d-1})\forall(i_{d-1}^{\prime},j_{d-1}^{\prime})\ V_{o}(S,\mathbf{i},\mathbf% {i^{\prime}},\mathbf{j},\mathbf{j^{\prime}})=1

is true iff $o$ is a solution to $S$ . $\hfill\blacktriangleleft$

7.1 Proofs as Games

To establish the correspondence between bounded-depth Frege and ${\text{Iter}}_{d}$ it will be useful to view proofs as games. The depth- $d$ Prover-Delayer game (essentially also known as the Buss-Pudlák game [22]) for an unsatisfiable formula $F$ consists of two players, Prover and Delayer. Intuitively, the Prover is attempting to convince itself that $F$ is unsatisfiable, while the Delayer is trying to postpone this. The game proceeds in rounds, where in each round the Prover asks for the value of an arbitrary formula $C$ and the delayer responds with an answer – either $C=1$ (in which case the Prover remembers $C$ ) or $\neg C=1$ (and the Prover remembers $\neg C$ ). Finally, at the end of each round the Prover may forget any number of formulas from its memory. The game ends when the set of $\{0,1\}$ -assignments consistent with the Prover’s memory all falsify some axiom $A_{i}$ . That is, when the conjunction of the formulas in the Prover’s memory logically imply $\overline{A}_{i}$ .

Definition 54.

Let $F=\bigwedge_{i=1}^{m}A_{i}$ be an unsatisfiable formula. A Prover strategy is a rooted fan-out $\leq 2$ DAG $G$ in which every node $v$ is labeled with a set of boolean formulas $M_{v}$ , which we call the memory at node $v$ . Let $\mathsf{False}(M_{n})\leavevmode\nobreak\ :=\leavevmode\nobreak\ \{x\in\{0,1\}% ^{n}:C(x)=0,\forall C\in M_{v}\}$ be the set of assignments which falsify all of the formulas. The labels $M_{v}$ satisfy the following:

$\blacksquare$

root. If $v$ is the root then $M_{v}=\emptyset$ ;
$\blacksquare$

single child. If $v$ has one child $c$ then $M_{c}=M_{v}\setminus\{C\}$ for some formula $C$ ;
$\blacksquare$

two children. If $v$ has two children $c,c^{\prime}$ , then $M_{c}=M_{v}\cup\{\neg C\}$ and $M_{c^{\prime}}=M_{v}\cup\{C\}$ for some formula $C$ ;
$\blacksquare$

leaf. If $v$ has no children, then there is some $A_{i}$ for $i\in[m]$ such that $A_{i}(x)=0$ for all $x\in\mathsf{False}(M_{v})$ .

The width of the strategy is given by $\max_{v\in V}\max_{C\in M_{v}}\{0pt(C)\}$ and its depth is given by $\max_{v\in V}\max_{C\in M_{v}}\{0pt(C)\}+1$ – the off-by-one is to account for the fact that, as we will see, the conjunction of the formulas in memory will correspond to a line in Frege proof. The size of the strategy is $\sum_{v\in V(G)}\sum_{C\in M_{v}}|C|$ .

As for the original Prover-Delayer game for the resolution proof system and the Buss-Pudlák game for bounded-depth Frege proofs, finding a strategy for a formula closely relates to finding a refutation.

Lemma 55.

Let $F=\bigwedge_{i\in[m]}A_{i}$ be an unsatisfiable $\Pi_{d+1}$ -formula. There exists a width- $w$ and size- $s$ Frege_d refutation of $F$ iff there is a width- $w$ , depth- $d$ , and size- $s$ Prover strategy for $F$ .

Proof.

Let $\Pi$ be a Frege_d proof of $F$ . The graph of the Prover strategy will be the same as that of the proof. Beginning at the root $r$ , where $M_{r}=\emptyset$ , the Prover’s memory is constructed as follows: let $v$ be a node with memory $M_{v}$ ; we have several cases based on the rule used to derive the corresponding line $\pi_{v}$ .

$\blacksquare$

If $\pi_{v}$ was obtained by weakening $\pi_{u}$ with a formula $D$ , then $M_{u}:=M_{v}\setminus\{\neg D\}$ . That is, the Prover forgets $\neg D$ .
$\blacksquare$

If $\pi_{v}$ was obtained by cutting $\pi_{u}$ and $\pi_{w}$ on a formula $D$ , then $M_{u}:=M_{v}\cup\{D\}$ and $M_{w}:=M_{v}\cup\{\neg D\}$ . That is, the Prover queries the Delayer for the value of $D$ .
$\blacksquare$

If $\pi_{v}$ was obtained by axiom introduction, then $v$ is a leaf.

By induction, observe that the conjunction of the formulas in $M_{v}$ logically implies $\overline{\pi}_{v}$ , and hence the leaf case is satisfied. The width and size of the strategy are the same as the proof. The fact that $\Pi$ is a Frege_d refutation (meaning that $D$ is always a $\Pi_{d-1}\cup\Sigma_{d-1}$ -formula), gives us the depth of the strategy to be $d$ .

For the converse direction, a Prover strategy can be converted into a Frege proof by replacing each memory $M_{v}=\{C_{1},\ldots,C_{k}\}$ with the line $\neg C_{1}\lor\ldots\lor\neg C_{k}$ . As each formula in memory is a $\Pi_{d-1}$ or a $\Sigma_{d-1}$ -formula, the lines of this proof are $\Sigma_{d}$ -formulas and the proof is a Frege_d proof of with the same width and size as the strategy. $\hfill\blacktriangleleft$

As seen in Section 5, for a proof system to correspond to a ${\mathsf{TFPH}}$ class it must be reduction closed. We verify that Frege_d satisfies this property.

Lemma 56.

Let $F=\bigwedge_{i\in[m]}F_{i}$ and $G=\bigwedge_{j\in\ell}G_{j}$ be unsatisfiable $\Pi_{d+1}$ -formulas on $n$ variables, and suppose that there is a width- $w$ and size- $s$ Frege_d proof of $F$ . If $(f,g)$ is an ${\text{FF}}_{F}$ -formulation of ${\text{FF}}_{G}$ of depth ${\mathsf{polylog}}(n)$ , then $G$ has a $\Sigma_{d}$ -Frege_d refutation of size $s\cdot 2^{{\mathsf{polylog}}(n)}$ and width $w$ .

Proof.

Let $\Pi$ be a size- $s$ , Frege_d proof of $F$ . First, we modify $\Pi$ to be a proof of $F(f)=\bigwedge_{i\in[m]}F_{i}(f)$ , where $F_{i}(f)$ is the $\Sigma_{d}$ obtained by replacing each variable $x_{j}$ with the propositionalization of decision tree $f_{j}$ as defined in the reduced formula. To do so, we will view $\Pi$ as a Prover strategy and replace each memory $M_{v}=\{C_{1},\ldots,C_{k}\}$ by $\{C_{1}(f),\ldots,C_{k}(f)\}$ . That is, instead of querying $C$ , the prover will now query the formula $C(f)$ .

We now transform this into a Prover strategy, and hence proof, of $F(f,g)$ , which is a $\Sigma_{d}$ -weakening of $G$ . To do so, consider any leaf of the Prover strategy labeled by some $F_{i}(f)$ (corresponding to the Prover learning that $F_{i}(f)$ is falsified). At this leaf the Prover queries the decision tree $g_{i}$ , one variable at a time. Each leaf is labeled with $F_{i}(f)\lor\overline{p}$ for some path $p\in g_{i}$ ; an axiom of the formula of $F(f,g)$ . $\hfill\blacktriangleleft$

7.2 Chracterizing PLS_d

Now we are ready to prove our characterization Theorem 6, which we state formally next.

Theorem 57.

For any ${\text{FF}}_{F}\in{\mathsf{TF}}\Sigma_{d}$ , there is a complexity- $c$ ${\text{Iter}}_{d}$ -formulation of ${\text{FF}}_{F}$ iff there is a complexity- $\Theta(c)$ $\Sigma_{d}$ -Frege_d refutation of $F$ .

We will break the theorem into two lemmas, Lemma 58 transforming Frege proofs into ${\text{Iter}}_{d}$ -formulations, and Lemma 60 together with Lemma 56 providing the converse.

Lemma 58.

Let $F$ be an unsatisfiable $\Pi_{d+1}$ formula on $n$ variables. Suppose that there is a width- $w$ and size- $s$ $\Sigma_{d}$ -Frege_d proof of $F$ . Then ${\text{FF}}_{F}$ admits an ${\text{Iter}}_{d}$ -formulation of size $s$ and depth $w$ .

Proof.

Let $\Pi^{\prime}=(\pi_{1}^{\prime},\ldots,\pi_{m}^{\prime})$ be a Frege_d refutation of size $s$ and width $w$ , and suppose that it is ordered in reverse topological order so that $\pi_{1}=\bot$ . At a high level the meta-pointer $\tilde{S}:[m]\rightarrow[m]$ of the ${\text{Iter}}_{d}$ formula will trace a path from the root to a falsified axiom of the proof by always pointing a node $u$ , for which $\pi_{u}^{\prime}(x)$ is false under the given assignment $x$ , to a falsified child which is guaranteed to exist by the soundness of the proof. If $\pi_{u}^{\prime}(x)$ is false and was derived by cutting on $\pi_{v}^{\prime}=A\lor C$ and $\pi_{w}^{\prime}=B\lor\neg C$ then $\tilde{S}$ should point $u$ to the child $v$ or $w$ that is falsified. To determine which of $\pi_{v}^{\prime},\pi_{w}^{\prime}$ is falsified, we need to evaluate $A, B$ , and $C$ . Hence, we need to ensure that the size of the domain of the successor $S$ is large enough. A simple way to do so is to pre-process our proof $\Pi^{\prime}$ into a proof $\Pi=(\pi_{1},\ldots,p_{m})$ as follows: if $\pi_{u}^{\prime}=A\lor B$ was derived by cutting $A\lor\neg C$ and $B\lor C$ , then replace $\pi_{u}=A\lor B\lor C$ . Now, let $r_{i}$ be the maximum fanin at layer $i$ of any line $\pi_{i}$ in the proof $\Pi$ . By padding (with, for example, $\top=x\lor\neg x$ or $\bot=x\land\neg x$ ) we may assume that every line $\pi_{u}$ in $\Pi$ has the same fanin $r_{i}$ at each layer. That is,

\pi_{u}=\bigvee_{i_{1}\in[r_{1}]}\bigwedge_{i_{2}\in[r_{2}]}\cdots\underset{i_% {d-1}\in[r_{d-1}]}{\bigcirc}G_{u,\mathbf{i}},

where $G_{u,\mathbf{i}}$ is a fanin- $w$ clause if $\bigcirc=\land$ and a fanin- $w$ term if $\bigcirc=\lor$ . Let $\mathbf{r}=[r_{1}]\times\cdots\times[r_{d-1}]$ .

For any assignment $x\in\{0,1\}^{n}$ the successor function $S_{x}$ of our ${\text{Iter}}_{d}$ instance is defined as:

$\blacksquare$

Axiom Introduction. If $\pi_{u}$ is an axiom then $S_{x}(u,\mathbf{i})=u$ ;
$\blacksquare$

Weakening. If $\pi_{u}$ is a weakening of $\pi_{v}$ then $S_{x}(u,\mathbf{i})=u$ if $G_{u,\mathbf{i}}(x)=1$ and $v$ otherwise.
$\blacksquare$
Cut. If $\pi_{u}=A\lor B\lor C$ was derived by cutting $\pi_{v}=A\lor\neg C$ and $\pi_{w}=B\lor C$ then
1. i)
  
  If $G_{u,\mathbf{i}}$ is a subformula belonging to $A$ or $B$ then $S_{x}(u,\mathbf{i})=u$ if $G_{u,\mathbf{i}}(x)=1$ and $v$ otherwise.
2. ii)
  
  $G_{u,\mathbf{i}}$ is a subformula belonging to $C$ then $S_{x}(u,\mathbf{i})=v$ if $G_{u,\mathbf{i}}(x)=1$ and $w$ otherwise.

Observe that $G_{u,\mathbf{i}}(x)$ have width $w$ and so $S_{x}(u,\mathbf{i})$ can be evaluated by a depth- $w$ decision tree $f_{u,\mathbf{i}}$ querying the variables $x$ . Finally, for each solution $o=(u,i^{*}_{1},v,j^{*}_{1})$ , the output decision tree $g_{o}$ is the constant function which returns $v$ .

The following claim asserts the correctness of the formula, completing the proof.

Claim 59.

The meta-pointer $\tilde{S}_{x}$ , defined from $S_{x}$ , satisfies the following properties:

i)

$\tilde{S}_{x}(u)\geq u$ for any $u\in[m]$ ;
ii)

If $u\in[m]$ is such that $\pi_{u}$ is not an axiom, then $\tilde{S}_{x}(u)=u$ iff $\pi_{u}^{\prime}(x)=1$ (recall that $\pi_{u}^{\prime}$ belongs to the proof $\Pi^{\prime}$ before pre-processing);
iii)

For any $u\in[m]$ , if $\tilde{S}_{x}(u)=v\neq u$ then $\pi_{v}(x)=0$ .

Proof of Claim..

We will consider cases based on how $\pi_{u}$ was derived. If $\pi_{u}$ was deduced by axiom introduction then the claim holds by definition. If $\pi_{u}$ was derived by weakening $\pi_{v}$ , then re-parameterize the formula $G_{u,x}(\mathbf{i}):=G_{u,\mathbf{i}}(x)$ and let $S_{x,u}$ be $S_{x}$ with the first input fixed to $u$ . Then, noting that the definition of the successor in the case of weakening is equivalent to $S_{x,\mathbf{i}}(u)=G_{u,\mathbf{i}}\cdot u+(1-G_{u,\mathbf{i}})\cdot v$ , we have

$\displaystyle\tilde{S}_{x}(u)$	$\displaystyle=\mathsf{MIN}\big{(}S_{x,u},\leavevmode\nobreak\ \mathbf{r}\big{)% }=\mathsf{MIN}\big{(}G_{u,x}\cdot u+(1-G_{u,x})\cdot v,\leavevmode\nobreak\ % \mathbf{r}\big{)}$
	$\displaystyle=\mathsf{MAX}(G_{u,x},\mathbf{r})(u-v)+v$
	$\displaystyle=\pi_{u}(x)(u-v)+v$	(Observation 51)
	$\displaystyle=\pi_{u}(x)\cdot u+(1-\pi_{u}(x))\cdot v,$

where the $\mathsf{MIN}$ switched to a $\mathsf{MAX}$ because $u-v<0$ . The final equality is equivalent to

\tilde{S}_{x}(u)=\begin{cases}u&\mbox{ if }\pi_{u}(x)=1;\\ v&\mbox{ if }\pi_{u}(x)=0.\end{cases}

Thus, the claim holds when $\pi_{u}$ was derived by weakening. $\hfill\vartriangleleft$ Finally, consider the case when $\pi_{u}=A\lor B\lor C$ was derived by cutting $\pi_{v}=A\lor\neg C$ and $\pi_{w}=B\lor C$ . Denote by $\mathbf{r}_{A\vee B}=[r_{1}-1]\times[r_{2}]\times\cdots\times[r_{d-1}]$ and $\mathbf{r}_{C}=\{r_{1}\}\times[r_{2}]\times\cdots\times[r_{d-1}]$ . By partitioning the indices in this way, we will enforce that the subformulas with indices in $\mathbf{r}_{A\lor B}$ belong to $C$ , and the remaining belong to $A\lor B$ ; that is, we take the convention that all subformulas of $C$ have index $r_{1}$ . Then,

$\displaystyle\tilde{S}_{x}(u)$	$\displaystyle=\mathsf{MIN}\big{(}S_{x,u},\leavevmode\nobreak\ \mathbf{r}\big{)}$
	$\displaystyle=\min\Big{\{}\mathsf{MIN}\Big{(}G_{u,x}\cdot u+(1-G_{u,x})v,% \leavevmode\nobreak\ \mathbf{r}_{A\lor B}\Big{)},\mathsf{MAX}\Big{(}G_{u,x}% \cdot v+(1-G_{u,x})w,\leavevmode\nobreak\ \mathbf{r}_{C}\Big{)}\Big{\}}$
	$\displaystyle=\min\Big{\{}\mathsf{MAX}\big{(}G_{u,x},\leavevmode\nobreak\ % \leavevmode\nobreak\ \mathbf{r}_{A\lor B}\big{)}(u-v)+v,\mathsf{MIN}\big{(}G_{% u,x},\leavevmode\nobreak\ \leavevmode\nobreak\ \mathbf{r}_{C}\big{)}(v-w)\Big{\}}$
	$\displaystyle=\min\Big{\{}(A(x)\lor B(x))(u-v)+v,\leavevmode\nobreak\ % \leavevmode\nobreak\ C(x)(v-w)+w\Big{\}}$	(Observation 51)
	$\displaystyle=\big{(}A(x)\lor B(x)\big{)}\cdot u+\big{(}1-(A(x)\lor B(x)\big{)% }\cdot\big{(}C(x)\cdot v+(1-C(x))\cdot w\big{)},$

where we have swapped $\mathsf{MIN}$ s and $\mathsf{MAX}$ s using that $u<v,w$ . That is,

\tilde{S}_{x}(u)=\begin{cases}u&\mathrm{if}\ (A\vee B)(x)=1;\\ v&\mathrm{if}\ (A\vee B)(x)=0\ \mathrm{and}\ C(x)=0;\\ w&\mathrm{if}\ (A\vee B)(x)=0\ \mathrm{and}\ C(x)=1.\end{cases}

It follows that the claim holds in the case of the cut rule. $\hfill\blacktriangleleft$

We now turn to establishing the forward direction of Theorem 57, converting ${\text{Iter}}_{d}$ -formulations into $\Sigma_{d}$ -Frege_d proofs. As observed in Lemma 56, $\Sigma_{d}$ -Frege_d is reduction closed. Hence, in order to establish the forward direction of Theorem 57, it suffices to show that Frege_d has efficient proofs of the propositional encoding of ${\text{Iter}}_{d}$ , which we describe next.

The Iter_d Formula.

For simplicity (by padding) we may assume without loss of generality that in the definition of ${\text{Iter}}_{d}$ , $m=r_{1}=\ldots=r_{d-1}$ . Our formula will be over $m$ -ary variables $S_{u,\bf i}\in[m]$ for $u\in[m]$ and $\mathbf{i}\in[m]^{d-1}$ ; this may be encoded by $\log n$ -many binary variables $S_{u,\mathbf{i},k}$ which spell out the binary encoding of the value of $S_{u,\bf i}$ . In particular, if $v\in[m]$ has binary expansion $v=\sum_{k\in[\log m]}b_{k}2^{k-1}$ , then the formula $[\![S_{u,\mathbf{i}}=v]\!]:=\bigwedge_{k\in[\log m]}S_{u,\mathbf{i},k}^{b_{k}}$ with the notation that $x^{1}=x$ and $x^{0}=\neg{x}$ for any variable $x$ . Similarly, we write $[\![S_{u,\mathbf{i}}\neq v]\!]=\neg[\![S_{u,\mathbf{i}}=v]\!]$ , where the negation is propagated to the literals. As well, for $u,v,i^{*}\in[m]$ denote by $[\![\text{bad}(i^{*})\lor\tilde{S}(u)\neq v]\!]$ the formula

[\![\text{bad}(i^{*}_{1})\vee\tilde{S}(u)\neq v]\!]:=\bigg{(}\bigvee_{i_{1}}% \bigwedge_{i_{2}}\cdots\bigwedge_{i_{d-1}}\bigwedge_{v\leq v^{\prime}}[\![S_{u% ,\mathbf{i}}\neq v^{\prime}]\!]\bigg{)}\vee\bigg{(}\bigvee_{i_{2}^{\prime}}% \bigwedge_{i_{3}^{\prime}}\cdots\bigvee_{i_{d-1}^{\prime}}\bigvee_{v<v^{\prime% }}[\![S_{u,i_{1}^{*}\mathbf{i^{\prime}}}=v^{\prime}]\!]\bigg{)}

If $d$ is odd, and

[\![\text{bad}(i^{*}_{1})\vee\tilde{S}(u)\neq v]\!]:=\bigg{(}\bigvee_{i_{1}}% \bigwedge_{i_{2}}\cdots\bigvee_{i_{d-1}}\bigvee_{v^{\prime}<v}[\![S_{u,\mathbf% {i}}=v^{\prime}]\!]\bigg{)}\vee\bigg{(}\bigvee_{i_{2}^{\prime}}\bigwedge_{i_{3% }^{\prime}}\cdots\bigwedge_{i_{d-1}^{\prime}}\bigwedge_{v^{\prime}\geq v}[\![S% _{u,i_{1}^{*}\mathbf{i^{\prime}}}\neq v^{\prime}]\!]\bigg{)}

If $d$ is even.

It states that $\tilde{S}(u)\neq v$ by asserting that either $i_{1}^{*}$ is not a certificate of computation for $u$ (left-hand side of the disjunction) or that the minimum is greater than $v$ (right-hand side of the disjunction). These are $\Sigma_{(d-1).5}$ -formulas.

The ${\text{Iter}}_{d}$ formula is the conjunction of the following:

i)

$[\![\text{bad}(i^{*}_{1})\vee\tilde{S}(1)\neq 1]\!]$ for each $i_{1}^{*}$ , ( $1$ is a source)
ii)

$[\![\text{bad}(i^{*}_{1})\vee\tilde{S}(u)\neq v]\!]$ for each pair of nodes $v<u$ and index $i_{1}^{*}$ , (No backwards pointer)
iii)

$[\![\text{bad}(i^{*}_{1})\vee\tilde{S}(u)\neq v]\!]\vee[\![\text{bad}(i^{*}_{1% })\vee\tilde{S}(v)\neq v]\!].$ for each $u,v,i_{1}^{*},j_{1}^{*}\in[m]$ with $u<v$ . (No proper sinks)

Lemma 60.

There is a size- $O(n^{2})$ and width- $O(\log n)$ Frege_d proof of ${\text{Iter}}_{d}$ .

For nodes $u, v$ and an index $i_{1}$ , it will be convenient to denote by $[\![S_{i_{1}}(u)\leq v]\!]$ the formula

	$\displaystyle[\![S_{i_{1}}(u)\leq v]\!]:=\bigwedge_{i_{2}}\bigvee_{i_{3}}% \cdots\bigwedge_{i_{d-1}}\bigwedge_{v<v^{\prime}}[\![S_{u,i_{1}\mathbf{i}}\neq v% ^{\prime}]\!]$	$\displaystyle\quad\mathrm{if}\ d\ \mathrm{is\ odd},$
	$\displaystyle[\![S_{i_{1}}(u)\leq v]\!]:=\bigwedge_{i_{2}}\bigvee_{i_{3}}% \cdots\bigvee_{i_{d-1}}\bigvee_{v^{\prime}\leq v}[\![S_{u,i_{1}\mathbf{i}}=v^{% \prime}]\!]$	$\displaystyle\quad\mathrm{if}\ d\ \mathrm{is\ even},$

which encodes that $\max_{i_{2}}\min_{i_{3}}\cdots\bigcirc_{i_{d}}S(u,i_{1}\mathbf{i})$ is less than or equal to $v$ . These are $\Pi_{(d-2).5}$ -formulas that will be used as cuts in the proof (or queries in the Prover’s strategy).

Proof.

We give a Prover strategy for ${\text{Iter}}_{d}$ . The idea of the strategy is as follows: the Prover will begin at the root node $1$ and will traverse the successor $\tilde{S}$ until they reach a solution (either $1$ points to itself, $u$ points to $v$ with $v<u$ , or $u$ is a proper sink). To achieve this, at each node $u$ , the Prover tries to determine the value of $\tilde{S}(u)$ . They are unable to do so directly, as this would require the Prover to query a formula of depth $d$ . Instead, they determine the value of $\tilde{S}(u)$ via an auction procedure, which we describe below. Once the Prover has determined $v$ such that $\tilde{S}(u)=v$ , then either the Prover has found a solution, or otherwise the Prover forgets everything except the information necessary to infer $\tilde{S}(u)=v$ , and queries the Delayer via the auction procedure to learn the value of $\tilde{S}(v)$ . At each step, the Prover has in memory the value of $\tilde{S}(w)$ for at most two nodes $w\in[m]$ .

The Auction Procedure. The procedure determines a value $v\in[m]$ so that $\tilde{S}(u)=v$ is the only value compatible with the answers given by the Delayer. The procedure is in rounds $v=m-1,\ldots,1$ . At each round the Prover queries the formula $[\![S_{i_{1}}(u)\leq v]\!]$ for $i_{1}=1,\ldots,m$ and reacts in the following way to the answers of the Delayer:

Round $v=m-1$ :: As soon as the Delayer answers $1$ for some $i^{*}_{1}\in[m]$ , the Prover forgets all of the previously-learned formulas of the form $\neg[\![S_{j}(u)\leq m-1]\!]$ for $j<i^{*}_{1}$ , retains in memory the formula $[\![S_{i^{*}_{1}}(u)\leq m-1]\!]$ , and moves to the round $v=m-2$ . If the Delayer answers $0$ to all $i_{1}^{*}\in[m]$ , then the Prover knows that $\tilde{S}(u)=m$ .
Round $v<m-1$ :: By induction the Prover’s memory consists only of $[\![S_{j_{1}^{*}}(u)\leq v+1]\!]$ for some $j_{1}^{*}\in[m]$ . Hence, the Prover knows that $\tilde{S}(u)\leq v+1$ , and it would like to determine whether $\tilde{S}(u)=v+1$ or $\tilde{S}(u)\leq v$ . As soon as the Delayer answers $1$ to the queries made during this round, for some $i^{*}_{1}\in[m]$ , the Prover retains in memory only the formula $[\![S_{i^{*}_{1}}(u)\leq v]\!]$ , forgetting the formulas $\neg[\![S_{k}(u)\leq v]\!]$ for all $k<i^{*}_{1}$ and $[\![S_{j_{1}^{*}}(u)\leq v+1]\!]$ . They then move to round $v-1$ if $v>1$ or halt if $v=1$ , as this implies that $\tilde{S}(u)=1$ .

If the Delayer answers $0$ to all $i_{1}^{*}\in[m]$ , then the Prover’s memory contains $[\![S_{j_{1}^{*}}(u)\leq v+1]\!]$ and $\neg[\![S_{k}(u)\leq v]\!]=0$ for all $j\in[m]$ , which implies that $\tilde{S}(u)=v$ . The Prover then halts the auction procedure, keeping its memory as is.

Observe that there are at most $O(m^{4})$ -many possible states in any auction procedure. The memory of each state contains at most $O(m)$ -many formulas, and each formula has size $O(m^{d})$ and width $O(\log m)$ . Hence the size of each auction phase is at most $O(m^{d+5})$ .
With the auction procedure in place, we are ready to describe the Prover strategy in detail. Beginning with the node $u=1$ , the Prover determines a node $v$ such that $\tilde{S}(u)=v$ via the auction procedure.

$\blacksquare$

If $u=v=1$ : the Prover halts;
$\blacksquare$

If $v<u$ : the Prover forgets everything in memory except for the formulas determining that $\tilde{S}(u)=v$ and halts.
$\blacksquare$

If $v=u\neq 1$ , then prior to computing $\tilde{S}(u)$ , the Prover’s memory already contains formulas which enforce that $\tilde{S}(w)=u$ for some $u<w$ , hence they have found a solution and they halt.
$\blacksquare$

If $u<v$ then the Prover had in its memory the formulas determining that $\tilde{S}(w)=u$ for some $w<u$ . They forget these equalities which are not relevant to enforcing that $\tilde{S}(u)=v$ , and the Prover moves to node $v$ .

This process terminates as the current node $u$ increases by at least $1$ at each step. We now calculate the number of possible states (and hence the number of lines in the corresponding Frege_d proof). As the auction procedure is performed once per round, and there are at most $m^{2}$ -many choices for the memory at each round (corresponding to the value of $i^{*}_{1}$ and the node pointing to $v$ ), the total size of the strategy is at most $O(m^{d+8})$ , which is $O(n^{4})$ where $n$ is the number of variables of the formula.

It remains to argue that this is a valid strategy for the Prover; that is, when the Prover halts, at least one axiom of the formula is violated by all assignments which satisfy their memory. There are several cases based on the reason for halting:

$\blacksquare$

If $u=v=1$ : then the memory contains $[\![S_{i_{1}^{*}}(1)\leq 1]\!]$ for some $i_{1}^{*}\in[m]$ . This is incompatible with the axiom $[\![\text{bad}(i_{1}^{*})\lor\tilde{S}(1)\neq 1]\!]$ .
$\blacksquare$

If $v<u$ : there are two possibilities based on the value of $v$ . If $v=1$ , then the memory contains $[\![S_{i_{1}^{*}}(u)\leq 1]\!]$ for some $i_{1}^{*}\in[m]$ , contradicting the axiom $[\![\text{bad}(i_{1}^{*})\lor\tilde{S}(u)\neq 1]\!]$ . Otherwise, if $v\neq 1$ then the memory contains $\neg[\![S_{i}(u)\leq v-1]\!]$ for all $i\in[m]$ and $[\![S_{i_{1}^{*}}(u)\leq v]\!]$ for some $i_{1}^{*}$ , contradicting the axiom $[\![\text{bad}(i_{1}^{*})\lor\tilde{S}(u)\neq v]\!]$ .
$\blacksquare$

If $\tilde{S}(u)=\tilde{S}(v)=v$ : then there are two cases based on whether $v=m$ . If $v\neq m$ then the memory contains $[\![S_{i_{1}^{*}}(u)\leq v]\!]$ and $[\![S_{j_{1}^{*}}(v)\leq v]\!]$ for some $i_{1}^{*},j_{1}^{*}\in[m]$ along with the formulas $\neg[\![S_{i}(u)\leq v-1]\!]$ and $\neg[\![S_{j}(v)\leq v-1]\!]$ for all $i,j\in[m]$ . This contradicts the axiom $[\![\text{bad}(i_{1}^{*})\lor\tilde{S}(u)\neq v]\!]\lor[\![\text{bad}(j_{1}^{*% })\lor\tilde{S}(v)\neq v]\!]$ .

Otherwise, the memory contains $\neg[\![S_{i}(u)\leq m-1]\!]$ and $\neg[\![S_{i}(v)\leq m-1]\!]$ for all $i,j\in[m]$ which contradicts the axiom $[\![\text{bad}(i_{1}^{*})\lor\tilde{S}(u)\neq m]\!]\lor[\![\text{bad}(j_{1}^{*% })\lor\tilde{S}(m)\neq m]\!]$ for all values of $i_{1}^{*}$ and $j_{1}^{*}$ . Indeed, for any node $u$ , if $\tilde{S}(u)=m$ then $i_{1}^{*}$ will always be an argument of the minimum, regardless of its value.

Hence, the Prover strategy is correct. $\hfill\blacktriangleleft$

References

[1] Albert Atserias and Massimo Lauria. Circular (yet sound) proofs in propositional logic. ACM Trans. Comput. Log., 24(3):20:1–20:26, 2023. doi:10.1145/3579997.
[2] Paul Beame, Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The relative complexity of NP search problems. J. Comput. Syst. Sci., 57(1):3–19, 1998. doi:10.1006/jcss.1998.1575.
[3] Arnold Beckmann and Samuel R. Buss. Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic. Journal of Mathematical Logic, 09(01):103–138, 2009. doi:10.1142/S0219061309000847.
[4] Olaf Beyersdorff. Proof complexity of quantified boolean logic–a survey. Mathematics for Computation (M4C), pages 353–391, 2022.
[5] Sam Buss, Noah Fleming, and Russell Impagliazzo. TFNP characterizations of proof systems and monotone circuits. In Yael Tauman Kalai, editor, 14th Innovations in Theoretical Computer Science Conference, ITCS 2023, January 10-13, 2023, MIT, Cambridge, Massachusetts, USA, volume 251 of LIPIcs, pages 30:1–30:40. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.ITCS.2023.30.
[6] Samuel R. Buss, Leszek Aleksander Kolodziejczyk, and Neil Thapen. Fragments of approximate counting. J. Symb. Log., 79(2):496–525, 2014. doi:10.1017/jsl.2013.37.
[7] Lijie Chen, Shuichi Hirahara, and Hanlin Ren. Symmetric exponential time requires near-maximum circuit size. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 1990–1999. ACM, 2024. doi:10.1145/3618260.3649624.
[8] Ben Davis and Robert Robere. Colourful TFNP and propositional proofs. In Amnon Ta-Shma, editor, 38th Computational Complexity Conference, CCC 2023, July 17-20, 2023, Warwick, UK, volume 264 of LIPIcs, pages 36:1–36:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.CCC.2023.36.
[9] Noah Fleming, Stefan Grosser, Toniann Pitassi, and Robert Robere. Black-box PPP is not turing-closed. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 1405–1414. ACM, 2024. doi:10.1145/3618260.3649769.
[10] Noah Fleming, Pravesh Kothari, and Toniann Pitassi. Semialgebraic proofs and efficient algorithm design. Found. Trends Theor. Comput. Sci., 14(1-2):1–221, 2019. doi:10.1561/0400000086.
[11] Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Further collapses in TFNP. Electron. Colloquium Comput. Complex., TR22-018, 2022. URL: https://eccc.weizmann.ac.il/report/2022/018.
[12] Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP. CoRR, abs/2205.02168, 2022. doi:10.48550/arXiv.2205.02168.
[13] Mika Göös, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adventures in monotone complexity and TFNP. In Avrim Blum, editor, 10th Innovations in Theoretical Computer Science Conference, ITCS 2019, January 10-12, 2019, San Diego, California, USA, volume 124 of LIPIcs, pages 38:1–38:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.ITCS.2019.38.
[14] Robert Kleinberg, Oliver Korten, Daniel Mitropolsky, and Christos H. Papadimitriou. Total functions in the polynomial hierarchy. In James R. Lee, editor, 12th Innovations in Theoretical Computer Science Conference, ITCS 2021, January 6-8, 2021, Virtual Conference, volume 185 of LIPIcs, pages 44:1–44:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.ITCS.2021.44.
[15] Leszek Aleksander Kolodziejczyk and Neil Thapen. Approximate counting and NP search problems, 2021.
[16] Oliver Korten. The hardest explicit construction. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 433–444. IEEE, 2021. doi:10.1109/FOCS52979.2021.00051.
[17] Oliver Korten and Toniann Pitassi. Strong vs. weak range avoidance and the linear ordering principle. In 65th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2024, Chicago, IL, USA, October 27-30, 2024, pages 1388–1407. IEEE, 2024. doi:10.1109/FOCS61266.2024.00089.
[18] Jan Krajícek, Alan Skelley, and Neil Thapen. NP search problems in low fragments of bounded arithmetic. J. Symb. Log., 72(2):649–672, 2007. doi:10.2178/JSL/1185803628.
[19] Yuhao Li, William Pires, and Robert Robere. Intersection classes in TFNP and proof complexity. In Venkatesan Guruswami, editor, 15th Innovations in Theoretical Computer Science Conference, ITCS 2024, January 30 to February 2, 2024, Berkeley, CA, USA, volume 287 of LIPIcs, pages 74:1–74:22. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.ITCS.2024.74.
[20] Zeyong Li. Symmetric exponential time requires near-maximum circuit size: Simplified, truly uniform. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 2000–2007. ACM, 2024. doi:10.1145/3618260.3649615.
[21] Pavel Pudlák. On the complexity of finding falsifying assignments for herbrand disjunctions. Arch. Math. Log., 54(7-8):769–783, 2015. doi:10.1007/S00153-015-0439-6.
[22] Pavel Pudlák and Samuel R. Buss. How to lie without being (easily) convicted and the length of proofs in propositional calculus. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 151–162. Springer, 1994. doi:10.1007/BFB0022253.
[23] Pavel Pudlák and Neil Thapen. Alternating minima and maxima, nash equilibira and bounded arithmetic. Annals of Pure and Applied Logic, 72:604–614, 2012. doi:10.1016/J.APAL.2011.06.014.
[24] Alan Skelley and Neil Thapen. The provably total search problems of bounded arithmetic. Proceedings of the London Mathematical Society, 103(1):106–138, 2011.
[25] Neil Thapen. How to fit large complexity classes into TFNP. CoRR, 2024. doi:10.48550/arXiv.2412.09984.

[bib.bib1] [1] Albert Atserias and Massimo Lauria. Circular (yet sound) proofs in propositional logic. ACM Trans. Comput. Log., 24(3):20:1–20:26, 2023. doi:10.1145/3579997.

[bib.bib2] [2] Paul Beame, Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The relative complexity of NP search problems. J. Comput. Syst. Sci., 57(1):3–19, 1998. doi:10.1006/jcss.1998.1575.

[bib.bib3] [3] Arnold Beckmann and Samuel R. Buss. Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic. Journal of Mathematical Logic, 09(01):103–138, 2009. doi:10.1142/S0219061309000847.

[bib.bib4] [4] Olaf Beyersdorff. Proof complexity of quantified boolean logic–a survey. Mathematics for Computation (M4C), pages 353–391, 2022.

[bib.bib5] [5] Sam Buss, Noah Fleming, and Russell Impagliazzo. TFNP characterizations of proof systems and monotone circuits. In Yael Tauman Kalai, editor, 14th Innovations in Theoretical Computer Science Conference, ITCS 2023, January 10-13, 2023, MIT, Cambridge, Massachusetts, USA, volume 251 of LIPIcs, pages 30:1–30:40. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.ITCS.2023.30.

[bib.bib6] [6] Samuel R. Buss, Leszek Aleksander Kolodziejczyk, and Neil Thapen. Fragments of approximate counting. J. Symb. Log., 79(2):496–525, 2014. doi:10.1017/jsl.2013.37.

[bib.bib7] [7] Lijie Chen, Shuichi Hirahara, and Hanlin Ren. Symmetric exponential time requires near-maximum circuit size. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 1990–1999. ACM, 2024. doi:10.1145/3618260.3649624.

[bib.bib8] [8] Ben Davis and Robert Robere. Colourful TFNP and propositional proofs. In Amnon Ta-Shma, editor, 38th Computational Complexity Conference, CCC 2023, July 17-20, 2023, Warwick, UK, volume 264 of LIPIcs, pages 36:1–36:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.CCC.2023.36.

[bib.bib9] [9] Noah Fleming, Stefan Grosser, Toniann Pitassi, and Robert Robere. Black-box PPP is not turing-closed. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 1405–1414. ACM, 2024. doi:10.1145/3618260.3649769.

[bib.bib10] [10] Noah Fleming, Pravesh Kothari, and Toniann Pitassi. Semialgebraic proofs and efficient algorithm design. Found. Trends Theor. Comput. Sci., 14(1-2):1–221, 2019. doi:10.1561/0400000086.

[bib.bib11] [11] Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Further collapses in TFNP. Electron. Colloquium Comput. Complex., TR22-018, 2022. URL: https://eccc.weizmann.ac.il/report/2022/018.

[bib.bib12] [12] Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP. CoRR, abs/2205.02168, 2022. doi:10.48550/arXiv.2205.02168.

[bib.bib13] [13] Mika Göös, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adventures in monotone complexity and TFNP. In Avrim Blum, editor, 10th Innovations in Theoretical Computer Science Conference, ITCS 2019, January 10-12, 2019, San Diego, California, USA, volume 124 of LIPIcs, pages 38:1–38:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.ITCS.2019.38.

[bib.bib14] [14] Robert Kleinberg, Oliver Korten, Daniel Mitropolsky, and Christos H. Papadimitriou. Total functions in the polynomial hierarchy. In James R. Lee, editor, 12th Innovations in Theoretical Computer Science Conference, ITCS 2021, January 6-8, 2021, Virtual Conference, volume 185 of LIPIcs, pages 44:1–44:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.ITCS.2021.44.

[bib.bib15] [15] Leszek Aleksander Kolodziejczyk and Neil Thapen. Approximate counting and NP search problems, 2021.

[bib.bib16] [16] Oliver Korten. The hardest explicit construction. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 433–444. IEEE, 2021. doi:10.1109/FOCS52979.2021.00051.

[bib.bib17] [17] Oliver Korten and Toniann Pitassi. Strong vs. weak range avoidance and the linear ordering principle. In 65th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2024, Chicago, IL, USA, October 27-30, 2024, pages 1388–1407. IEEE, 2024. doi:10.1109/FOCS61266.2024.00089.

[bib.bib18] [18] Jan Krajícek, Alan Skelley, and Neil Thapen. NP search problems in low fragments of bounded arithmetic. J. Symb. Log., 72(2):649–672, 2007. doi:10.2178/JSL/1185803628.

[bib.bib19] [19] Yuhao Li, William Pires, and Robert Robere. Intersection classes in TFNP and proof complexity. In Venkatesan Guruswami, editor, 15th Innovations in Theoretical Computer Science Conference, ITCS 2024, January 30 to February 2, 2024, Berkeley, CA, USA, volume 287 of LIPIcs, pages 74:1–74:22. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.ITCS.2024.74.

[bib.bib20] [20] Zeyong Li. Symmetric exponential time requires near-maximum circuit size: Simplified, truly uniform. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 2000–2007. ACM, 2024. doi:10.1145/3618260.3649615.

[bib.bib21] [21] Pavel Pudlák. On the complexity of finding falsifying assignments for herbrand disjunctions. Arch. Math. Log., 54(7-8):769–783, 2015. doi:10.1007/S00153-015-0439-6.

[bib.bib22] [22] Pavel Pudlák and Samuel R. Buss. How to lie without being (easily) convicted and the length of proofs in propositional calculus. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 151–162. Springer, 1994. doi:10.1007/BFB0022253.

[bib.bib23] [23] Pavel Pudlák and Neil Thapen. Alternating minima and maxima, nash equilibira and bounded arithmetic. Annals of Pure and Applied Logic, 72:604–614, 2012. doi:10.1016/J.APAL.2011.06.014.

[bib.bib24] [24] Alan Skelley and Neil Thapen. The provably total search problems of bounded arithmetic. Proceedings of the London Mathematical Society, 103(1):106–138, 2011.

[bib.bib25] [25] Neil Thapen. How to fit large complexity classes into TFNP. CoRR, 2024. doi:10.48550/arXiv.2412.09984.

Provably Total Functions in the Polynomial Hierarchy

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Definition 1.

Definition 2.

Our Results

Theorem 3 (Informal).

Theorem 4 (Informal).

Theorem 5 (Informal).

Theorem 6 (informal).

Comparison with Bounded Arithmetic.

Comparison with [25].

Open Problems.

2 Preliminaries on the Total Function Polynomial Hierarchy

Definition 7.

Definition 8.

Definition 9.

Syntactic and Uniform Classes.

3 Proof Systems for TFPH

3.1 Recap: Proof Systems for TFNP

Definition 10.

Claim 11.

3.2 Proof Systems and TFPH

Definition 12.

False Formula Search.

Lemma 13.

Proof.

Reduced Formula.

Definition 14.

Comparison with Proof Systems for QBF.

4 Sherali-Adams and Strong Range Avoidance

Definition 15.

Claim 16.

Proof.

Definition 17.

Theorem 18.

4.1 SA Proofs Imply sRA Reductions

Lemma 19.

Definition 20.

Lemma 21.

Proof.

Proof of Lemma 19.

4.2 sRA Reductions Imply SA Proofs

Lemma 22.

Proof of Lemma 22.

5 A Generic Correspondence

Theorem 23.

5.1 A Proof System for any 𝗧𝗙⁢𝚺𝒅 Problem

Definition 24.

Lemma 25.

Proof.

5.2 A 𝗧𝗙⁢𝚺𝒅 Problem for any Proof System which Reflects

Proof.

Definition 26.

Lemma 27.

Proof.

6 Characterizations in 𝗧𝗙⁢𝚺𝟐

Definition 28.

Lemma 29 (Theorem 3.6 in [8]).

Definition 30.

6.1 DNF Resolution

Definition 31.

Theorem 32.

Lemma 33.

Proof.

Claim 34.

Proof of Claim.

Lemma 35.

Proof of Lemma 35.

6.2 Circular and Reversible DNF Resolution

Definition 36.

5.1 A Proof System for any ${\mathsf{TF}}\Sigma_{d}$ Problem

5.2 A ${\mathsf{TF}}\Sigma_{d}$ Problem for any Proof System which Reflects

6 Characterizations in ${\mathsf{TF}}\Sigma_{2}$

6.3 Relationships in ${\mathsf{TF}}\Sigma_{2}$

7.2 Chracterizing PLS_d

The Iter_d Formula.