Pith. sign in

REVIEW 2 major objections 4 minor 1 cited by

How to fit large complexity classes into TFNP

T0 review · 2 major / 4 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Large complexity classes such as PSPACE and the polynomial hierarchy can be encoded as TFNP subclasses whose complete problems are characterized by the Frege and constant-depth Frege proof systems.

desk verdict A worthwhile framework paper whose Frege characterizations rest on an unproven type-2/decision-tree bridge in Section 9. read the letter →

arxiv 2412.09984 v2 pith:RMTFEEEB submitted 2024-12-13 cs.CC cs.LO

Neil Thapen This is my paper · ORCID
classification cs.CCcs.LO MSC 03F2068Q15
keywords TFNPtotalsearchproblemsInspector-AdversarygamescounterexamplereducibilityFregeproofsystemconstant-depthboundedarithmeticapproximatecounting
topics P versus NP
open problems P versus NP
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper gives two general ways to build subclasses of TFNP, the class of total NP search problems, from computational objects that live outside TFNP. The first is an Inspector-Adversary game: an untrustworthy Adversary claims to answer queries to some complexity class, and the resulting search problem asks for a run of a querying protocol that does not catch the Adversary in a contradiction. The second is counterexample reducibility for $\mathrm{TF}\Sigma_2^p$ problems, where a proposed solution is accepted unless a counterexample to the Adversary's answer is produced. The paper's headline results are that the subclass built from PSPACE is characterized by the Frege proof system, and the subclasses built from the polynomial hierarchy are characterized by the constant-depth Frege hierarchy. A reader should care because this extends the known dictionary between TFNP subclasses and propositional proof systems to much stronger systems, giving PSPACE and the polynomial hierarchy a concrete computational footprint inside total search problems.

What carries the argument

The load-bearing object is the Inspector-Adversary game, packaged as $\mathrm{Local}\text{-}\Gamma$. An Inspector sends queries about a formal oracle $A$ to an Adversary who is only constrained by universal axioms $\Gamma$; the Adversary must answer consistently, and the Inspector wins by either producing a solution to a target search problem or exposing an axiom failure. When $\Gamma$ has a real model, $\mathrm{Local}\text{-}\Gamma$ is a total search problem and is complete for the problems solvable over $\Gamma$. The second mechanism is counterexample reducibility: for a $\mathrm{TF}\Sigma_2^p$ problem $R$, the TFNP problem Checkable $R$ asks, given an input $x$ and a circuit $C$, to find $y$ such that $R(x,y,C(y))$ holds. This turns a coNP-verifiable totality notion into a concrete search problem, and yields PLS and PPADS as Checkable versions of $P^{NP}$ computation and Empty. The QBF axioms $\Gamma_{\mathrm{TQBF}}$ and their depth-restricted fragments $\Gamma^k_{\mathrm{TQBF}}$ are what connect the construction to proof systems: a run avoiding axiom failures corresponds to a Frege or depth-restricted Frege refutation via the decision-tree reductions of Section 8.

What would settle it

Find a narrow unsatisfiable CNF family with quasipolynomial-size Frege refutations whose false-clause search problem is not reducible to $\mathrm{Local}\text{-}\Gamma_{\mathrm{TQBF}}$ (equivalently, to FCon). Proposition 8.7 predicts this cannot happen; the standard lower-bound methods for constant-depth Frege are the place to look for such a counterexample.

Watch

Extended reading notes

Core claim

At the center of the first construction is the problem $\mathrm{Local}\text{-}\Gamma$: given a polynomial-time protocol with an oracle tape named $A$, find a sparse oracle of replies under which the protocol does not witness the failure of any axiom in a fixed finite list $\Gamma$. If $\Gamma$ holds for some genuine total oracle, $\mathrm{Local}\text{-}\Gamma$ is total, and it is complete for the class of TFNP problems solvable over $\Gamma$. The paper proves that parity axioms give a class complete for PPA; that two quite different axiomatizations of PSPACE, one by true quantified Boolean formulas and one by PSPACE computations, give equivalent problems; and that the restricted problems $\mathrm{Local}\text{-}\Gamma^k_{\mathrm{TQBF}}$ are equivalent to the previously studied $GI_k$ problems and are characterized by depth-$(k+1/2)$ Frege, while $\mathrm{Local}\text{-}\Gamma_{\mathrm{TQBF}}$ is equivalent to Frege consistency and is characterized by Frege. On the counting side, it recasts the approximate-counting class APPROX as the class of TFNP problems counterexample-reducible to the $\mathrm{TF}\Sigma_2^p$ weak pigeonhole principle, gives a direct reduction of Ramsey into APPROX, and shows that weakened forms of Long choice and Short choice live in APPROX.

Load-bearing premise

The Section 9 equivalences between the $\mathrm{Local}\text{-}\Gamma$ problems and the $GI_k$ and $FCon$ problems presuppose that the published bounded-arithmetic characterizations of $T^k_2$ and $U^1_2$ transfer unchanged to the type-2 versions of these problems, and that the type-2-to-decision-tree correspondence preserves the relevant reductions.

Editorial extensions

If this is right

  • The single TFNP problem $\mathrm{Local}\text{-}\Gamma_{\mathrm{TQBF}}$ contains PLS, PPA, PPP and their subclasses by natural reductions, and any TFNP problem with quasipolynomial-size Frege proofs of totality reduces to it.
  • Consecutive levels of the polynomial-hierarchy-in-TFNP hierarchy $\mathrm{Local}\text{-}\Gamma^k_{\mathrm{TQBF}}$ are characterized by depth-$(k+1/2)$ Frege, so separating these levels is equivalent to the long-standing open problem of separating depth-$k$ from depth-$(k+1)$ Frege.
  • Every TFNP problem counterexample-reducible to the $\mathrm{TF}\Sigma_2^p$ weak pigeonhole principle lies in APPROX, and Ramsey, Weak pigeon, Localopt, Checkable tournament and Checkable Min all lie in APPROX, while APPROX does not contain PPAD.
  • Weak long choice is a nontrivial intermediate: both Ramsey and Weak pigeon reduce to it, yet it lies inside APPROX, so the counting power needed for Ramsey can be separated from precise counting.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A direct, logic-free reduction of Ramsey to $\mathrm{Local}\text{-}\Gamma_{\mathrm{TQBF}}$ (or to $\mathrm{Local}\text{-}\Gamma^k_{\mathrm{TQBF}}$) would be a clean certificate that the Frege characterization captures the right class; the paper's reduction to APPROX is an intermediate step in that direction.
  • If Toda's theorem can be simulated in the $\Gamma_\#$ game, then the entire polynomial-hierarchy class would collapse into the single problem $\mathrm{Local}\text{-}\Gamma_\#$, giving a new algebraic proof system equivalent to constant-depth Frege with counting gates; the paper explicitly leaves this as an open direction.
  • The same construction applied to EXPTIME, which the paper expects to be connected to extended Frege, would put a class above the Frege 'hat'; this is a natural next test of whether the Inspector-Adversary recipe is a general correspondence between oracle complexity classes and proof systems.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper develops two abstract mechanisms for producing TFNP subclasses from objects outside TFNP. The first is an Inspector-Adversary game over a list Γ of universal axioms, yielding the class of problems reducible to the canonical problem Local-Γ (Section 3). The second is counterexample reducibility to TFΣ_2^p problems, whose projection to TFNP gives Checkable R (Section 6). The main results are: parity axioms Γ⊕ give exactly PPA (Theorem 4.1) with some robustness to the choice of axioms (Theorem 4.7); natural NP axioms give PLS (Proposition 6.10); PSPACE axioms, whether via QBF evaluation or via iterated circuits, give equivalent classes (Theorem 5.3) that contain the standard TFNP classes; and the stratified QBF axioms Γ_k^TQBF correspond to the previously studied GI_k problems and, in the decision-tree setting, to constant-depth Frege and Frege proof systems (Proposition 8.7). The paper also gives a simplified definition of the approximate-counting class APPROX, proves Ramsey, Weak long choice, and Weak short choice are in or reduce to APPROX, and compares these with Long choice and Short choice.

Significance. If the headline characterizations are established, the paper makes a substantial contribution: it supplies natural TFNP classes sitting above the standard ones, connects PSPACE and the polynomial hierarchy to Frege and constant-depth Frege in the TFNPdt framework of [GHJ+22], and gives a clean computational route to APPROX and its applications to Ramsey. The framework of Inspector-Adversary games is a genuinely useful organizing idea, and the paper contains several explicit, carefully written reductions, such as the proof that Weak long choice is in APPROX (Proposition 7.14) and the independence result for parity axioms (Theorem 4.7). The paper is open about what is new versus translated from bounded arithmetic, and it does not engage in parameter-fitting: the dependence on [ST11] and [BB17] is explicit and appropriate. However, the central Frege and constant-depth Frege characterizations currently rest on an asserted and non-obvious passage from type-2 problems to decision-tree TFNP problems in Section 9.1, which needs to be made rigorous before the paper's main claim is fully supported.

major comments (2)
  1. [Section 9.1 and Corollaries 9.3, 9.8] The transfer from type-2 TFNP to TFNPdt is asserted rather than proved, and the assertion is not automatic. In TFNPdt (Definition 8.1) the input length is quasipolynomial in a and every solution predicate must be decidable by a decision tree of depth poly(log a). A type-2 problem, by contrast, is solved by a polynomial-time oracle machine whose input includes a quasipolynomial-length string β; converting that machine into decision trees in the natural way gives depth polynomial in a, not poly(log a), because the machine may query polynomially many positions of β. This matters concretely for Local-ΓTQBF: checking that a branch α is good requires evaluating QBFs with D-gates under axiom 3 of ΓTQBF as modified in Definition 9.1, and nothing in Section 9.1 bounds the size of the QBFs appearing on a depth-log a branch or the number of δ-queries needed to evaluate them. Therefore Corollary 9.3 does not follow from Proposition 9.2, and Corollary 9.8 does not follow from Corollary 9.7. Since Proposition 8.7 is the paper's headline, this is a load-bearing gap: the claimed Frege and constant-depth Frege characterizations of Local-ΓTQBF and Local-Γ_k^TQBF require a separate uniform argument showing that the relevant reductions and solution predicates can be made shallow.
  2. [Section 5.1, Theorem 5.3 and Lemmas 5.4-5.5] The equivalence Local-ΓPSPACE ≡ Local-ΓTQBF is stated as a theorem but is only sketched. Lemma 5.5 in particular relies on formalizing the assertion ∀u∃!v Reach_i(u,v) as a QBF and on converting a failure of ΓPSPACE into a failure of ΓTQBF by binary search, but the encoding of the uniqueness quantifier and the exact transformation of a failed PSPACE computation into a TQBF axiom violation are not spelled out. This equivalence is later used in Corollary 9.7 to transfer the FCon characterization, so the section would be easier to verify if the missing details were supplied.
minor comments (4)
  1. [Section 1.5] The outline says that Section 4 shows the subclass arising from ⊕P is PPAD; the actual theorem (Theorem 4.1) says PPA. Please correct the typo.
  2. [Definition 6.2(5)] The sentence 'Retraction weak pigeon becomes Left pigeon if we replace [2n+1] with [2n+1]' is garbled; the intended comparison with Left pigeon, with the roles of pigeons and holes and the intervals involved, should be stated carefully.
  3. [Proof of Lemma 4.5] In the paragraph beginning 'For non-leaf nodes u', the nodes v and w are called 'parents' of u; in the tree T they should be 'children'. In addition, the construction of the circuit describing the graph G is only asserted, with the statement that the details are clear; a few explicit encoding sentences would help.
  4. [Proof of Lemma 8.14] In the displayed cedent for a clause of CNF(GI_4), the first disjunct is written as x1 ≠ f_i^1(x'_i), which appears to be a typo for x1 ≠ f_i^1(x'_1).

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper's characterizations are built from independent published theorems and internal reductions, not from definitions that presuppose the target results.

full rationale

The derivation chain is not circular. The core constructions are defined from scratch: Local-Γ is introduced in Definitions 3.1–3.4 with the completeness Proposition 3.6 proved directly, and the standard classes PPA, PLS and PPP are obtained by explicit reductions (Theorems 4.1, 6.8 and 5.10). The Frege and constant-depth Frege characterizations in Proposition 8.7 are obtained in two stages: Section 8 proves characterizations of the standard problems GIk and FCon (Theorems 8.17 and 8.20), and Section 9 proves equivalences Local-Γk_TQBF ≡ GIk and Local-ΓTQBF ≡ FCon (Propositions 9.2 and 9.6, Corollary 9.7). Some of these results rely on prior work by the same author, notably [ST11] and [KNT11], so self-citation is present and is load-bearing. However, the cited results are published, independent theorem statements about bounded arithmetic and propositional proof systems; they do not assume the paper's Local-Γ claims as hypotheses, and the paper's own reductions do not reduce to a fitted parameter or a definitional identity. There is no instance where a quantity fitted to a data set is later renamed as a prediction, and no axiom system is chosen so that the target equivalence holds by construction. The most serious technical gap is in Section 9.1: the passage from type-2 problems to TFNPdt families is asserted rather than proved, so Corollaries 9.3 and 9.8 do not explicitly verify that the reductions have polylogarithmic depth. That is a correctness or rigor concern, not a circularity, and it does not affect the circularity score.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The central claims rest on several published theorems from bounded arithmetic and proof complexity, listed above. These are taken as black boxes; the paper's contribution is to connect them via new reduction frameworks rather than to prove them from scratch.

assumptions (6)
  • domain assumption The provably total NP search problems of T^k_2 are exactly those reducible to GI_k (Skelley-Thapen, 2011).
    Used in Proposition 9.2 to show Local-Γk_TQBF ≡ GIk; not proved in this paper.
  • domain assumption The provably total NP search problems of U^1_2 are exactly those reducible to FCon (Beckmann-Buss, 2017).
    Used in Corollary 9.7 to identify Local-ΓPSPACE with FCon.
  • domain assumption APPROX contains precisely the TFNP problems provably total in APC2 (Kołodziejczyk-Thapen, 2022).
    Used in Proposition 7.3 to simplify the definition of APPROX via counterexample reducibility.
  • domain assumption The translation of U^1_2 proofs into quasipolynomial-size Frege proofs (Krajíček, 1995).
    Used in Lemma 8.19 to show CNF(FCon) has quasipolynomial-size Frege refutations.
  • domain assumption Known oracle separation between PLS and PPADS (Morioka 2001, Göös et al. 2022).
    Used in Corollary 6.9 to show no counterexample reduction between PNP computation and Empty.
  • domain assumption Exponential lower bounds for bounded-depth Frege proofs of the pigeonhole principle (Pitassi-Beame-Impagliazzo, Krajíček-Pudlák-Woods).
    Used in Corollary 9.5 to show Local-Γk_TQBF does not contain PPAD.

how reviews work

0 comments
Cite this review

Pith. "Pith review of How to fit large complexity classes into TFNP." pith.science (2026). https://pith.science/paper/RMTFEEEB

@misc{pith2026241209984,
  author       = {Pith},
  title        = {Pith review of: How to fit large complexity classes into TFNP},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RMTFEEEB}},
  note         = {Machine review of arXiv:2412.09984}
}
read the original abstract

Subclasses of TFNP (total functional NP) are usually defined by specifying a complete problem, which is necessarily in TFNP, and including all problems many-one reducible to it. We study two notions of how a TFNP problem can be reducible to an object, such as a complexity class, outside TFNP. This gives rise to subclasses of TFNP which capture some properties of that outside object. We show that well-known subclasses can arise in this way, for example PPA from reducibility to parity P and PLS from reducibility to P^NP. We study subclasses arising from PSPACE and the polynomial hierarchy, and show that they are characterized by the propositional proof systems Frege and constant-depth Frege, extending the known pairings between natural TFNP subclasses and proof systems. We study approximate counting from this point of view, and look for a subclass of TFNP that gives a natural home to combinatorial principles such as Ramsey which can be proved using approximate counting. We relate this to the recently-studied Long choice and Short choice problems.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Separations above TFNP from Sherali-Adams Lower Bounds

    cs.CC 2026-02 conditional novelty 8.0 of 10

    LOP is separated from Strong Avoid and Least Number in the black-box TFΣ2 setting, via Σ2-variant Sherali-Adams pseudo-expectations.

Reference graph

Works this paper leans on

64 extracted references · 62 canonical work pages · cited by 1 Pith paper

  1. [1]

    , " * write output.state after.block = add.period write newline

    ") INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence := #2 'after.sentence := #3 'after.block := STRINGS s t FUNCTION output.nonnull 's := output.state mid.sentence = ", " * write output.state after.block = add.period write newline " " write output.state before.all = 'wri...

  2. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION fin.entry add.period write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION new.sentence output.state after.block = 'skip output.state before.all = 'skip after.sentence 'output.state := if if FUNCTION not #0 #1 if FUNCTION and 'skip pop #0 if FUNCTIO...

  3. [3]

    M. Ajtai. The complexity of the pigeonhole principle. Combinatorica , 14:417--433, 1994

    work page 1994

  4. [4]

    Beckmann and S

    A. Beckmann and S. R. Buss. Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic. Journal of Mathematical Logic , 9(01):103--138, 2009

    work page 2009

  5. [5]

    Beckmann and S

    A. Beckmann and S. R. Buss. Characterising definable search problems in bounded arithmetic via proof notations. Ways of proof theory , pages 65--134, 2010

    work page 2010

  6. [6]

    Beckmann and S

    A. Beckmann and S. R. Buss. Improved witnessing and local improvement principles for second-order bounded arithmetic. ACM Transactions on Computational Logic (TOCL) , 15(1):1--35, 2014

    work page 2014

  7. [7]

    Beckmann and S

    A. Beckmann and S. Buss. The NP search problems of Frege and extended Frege proofs. ACM Transactions on Computational Logic (TOCL) , 18(2):1--19, 2017

    work page 2017

  8. [8]

    Beame, S

    P. Beame, S. Cook, J. Edmonds, R. Impagliazzo, and T. Pitassi. The relative complexity of NP search problems. In Annual ACM symposium on Theory of Computing , pages 303--314, 1995

    work page 1995

Show all 64 references
  1. [9]

    S. Buss, N. Fleming, and R. Impagliazzo. TFNP characterizations of proof systems and monotone circuits. In 14th Innovations in Theoretical Computer Science Conference (ITCS 2023) , 2023

    2023

  2. [10]

    S. Buss, R. Impagliazzo, J. Kraj \' c ek, P. Pudl \'a k, A. A. Razborov, and J. Sgall. Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Computational Complexity , 6:256--298, 1996

    1996

  3. [11]

    S. R. Buss and A. S. Johnson. Propositional proofs and reductions between NP search problems. Annals of Pure and Applied Logic , 163(9):1163--1182, 2012

    2012

  4. [12]

    S. R. Buss and J. Kraj \' c ek. An application of Boolean complexity to separation problems in bounded arithmetic. Proceedings of the London Mathematical Society , 3(1):1--21, 1994

    1994

  5. [13]

    S. R. Buss, L. A. Ko odziejczyk, and N. Thapen. Fragments of approximate counting. The Journal of Symbolic Logic , 79(2):496--525, 2014

    2014

  6. [14]

    S. Buss, L. Ko odziejczyk, and K. Zdanowski. Collapsing modular counting in bounded arithmetic and constant depth propositional proofs. Transactions of the American Mathematical Society , 367(11):7517--7563, 2015

    2015

  7. [15]

    Buresh-Oppenheim and T

    J. Buresh-Oppenheim and T. Morioka. Relativized NP search problems and propositional proof systems. In Proceedings. 19th IEEE Annual Conference on Computational Complexity, 2004. , pages 54--67, 2004

    2004

  8. [16]

    S. R. Buss. Bounded arithmetic . Princeton University, 1985

    1985

  9. [17]

    S. Buss. Axiomatizations and conservation results for fragments of bounded arithmetic. In Logic and Computation , volume 106 of Contemporary Mathematics , pages 57--84. ACM, 1990

    1990

  10. [18]

    S. R. Buss. First-order proof theory of arithmetic. Handbook of proof theory , 137:79--147, 1998

    1998

  11. [19]

    S. R. Buss. An introduction to proof theory. Handbook of proof theory , 137:1--78, 1998

    1998

  12. [20]

    Chiari and J

    M. Chiari and J. Kraj \' c ek. Witnessing functions in bounded arithmetic and search problems. Journal of Symbolic Logic , 63(3):1095--1115, 1998

    1998

  13. [21]

    S. A. Cook. Feasibly constructive proofs and the propositional calculus (preliminary version). In Proceedings of the seventh annual ACM symposium on Theory of computing , pages 83--97, 1975

    1975

  14. [22]

    De Rezende, O

    S. De Rezende, O. Meir, J. Nordstr \"o m, T. Pitassi, R. Robere, and M. Vinyals. Lifting with simple gadgets and applications to circuit and proof complexity. In 2020 IEEE 61st Annual Symposium on Foundations of Computer Science (FOCS) , pages 24--30, 2020

    2020

  15. [23]

    G \"o \"o s, A

    M. G \"o \"o s, A. Hollender, S. Jain, G. Maystre, W. Pires, R. Robere, and R. Tao. Separations in proof complexity and TFNP . In IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS) , pages 1150--1161, 2022

    2022

  16. [24]

    G \"o \"o s, P

    M. G \"o \"o s, P. Kamath, R. Robere, and D. Sokolov. Adventures in monotone complexity and TFNP . In Innovations in Theoretical Computer Science Conference (ITCS 2019) , 2019

    2019

  17. [25]

    P. W. Goldberg and C. H. Papadimitriou. Towards a unified complexity theory of total functions. Journal of Computer and System Sciences , 94:167--192, 2018

    2018

  18. [26]

    J. Hanika. Herbrandizing search problems in bounded arithmetic. Mathematical Logic Quarterly , 50(6):577--586, 2004

    2004

  19. [27]

    Hub \'a c ek, E

    P. Hub \'a c ek, E. Khaniki, and N. Thapen. TFNP intersections through the lens of feasible disjunction. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024) . Schloss-Dagstuhl-Leibniz Zentrum f \"u r Informatik, 2024

    2024

  20. [28]

    Impagliazzo and J

    R. Impagliazzo and J. Krajíček. A note on conservativity relations among bounded arithmetic theories. Mathematical Logic Quarterly , 48(3):375--377, 2002

    2002

  21. [29]

    Je r \'a bek

    E. Je r \'a bek. Dual weak pigeonhole principle, Boolean complexity, and derandomization. Annals of Pure and Applied Logic , 129:1--37, 2004

    2004

  22. [30]

    Je r \'a bek

    E. Je r \'a bek. Approximate counting in bounded arithmetic. The Journal of Symbolic Logic , 72:959--993, 2007

    2007

  23. [31]

    Je r \'a bek

    E. Je r \'a bek. Approximate counting by hashing in bounded arithmetic. The Journal of Symbolic Logic , 74:829--860, 2009

    2009

  24. [32]

    D. S. Johnson, C. H. Papadimitriou, and M. Yannakakis. How easy is local search? Journal of computer and system sciences , 37(1):79--100, 1988

    1988

  25. [33]

    Kleinberg, O

    R. Kleinberg, O. Korten, D. Mitropolsky, and C. Papadimitriou. Total functions in the polynomial hierarchy. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021) , 2021

    2021

  26. [34]

    L. A. Kołodziejczyk, P. Nguyen, and N. Thapen. The provably total NP search problems of weak second order bounded arithmetic. Annals of Pure and Applied Logic , 162(6):419--446, 2011

    2011

  27. [35]

    O. Korten. The hardest explicit construction. In 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS) , pages 433--444, 2022

    2021

  28. [36]

    Kraj \' c ek, P

    J. Kraj \' c ek, P. Pudl \'a k, and A. Woods. An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random structures & algorithms , 7(1):15--39, 1995

    1995

  29. [37]

    Kraj \' c ek

    J. Kraj \' c ek. On Frege and extended Frege proof systems. In Feasible Mathematics II , pages 284--319. Springer, 1995

    1995

  30. [38]

    Kraj \' c ek

    J. Kraj \' c ek. On the weak pigeonhole principle. Fundamenta Mathematicae , 170:123--140, 2001

    2001

  31. [39]

    Kraj \' c ek

    J. Kraj \' c ek. Proof complexity , volume 170. Cambridge University Press, 2019

    2019

  32. [40]

    Kraj \' c ek, A

    J. Kraj \' c ek, A. Skelley, and N. Thapen. NP search problems in low fragments of bounded arithmetic. The Journal of Symbolic Logic , 72(2):649--672, 2007

    2007

  33. [41]

    L. A. Ko odziejczyk and N. Thapen. Approximate counting and NP search problems. Journal of Mathematical Logic , 22(03):2250012, 2022

    2022

  34. [42]

    Lov\' a sz, M

    L. Lov\' a sz, M. Naor, I. Newman, and A. Wigderson. Search problems in the decision tree model. SIAM Journal on Discrete Mathematics , 8(1):119--132, 1995

    1995

  35. [43]

    Li and I

    J. Li and I. C. Oliveira. Unprovability of strong complexity lower bounds in bounded arithmetic. In Proceedings of the 55th Annual ACM Symposium on Theory of Computing , pages 1051--1057, 2023

    2023

  36. [44]

    T. Morioka. Classification of search problems and their definability in bounded arithmetic . PhD thesis, 2001. Master's thesis, University of Toronto

    2001

  37. [45]

    Megiddo and C

    N. Megiddo and C. H. Papadimitriou. On total functions, existence theorems and computational complexity. Theoretical Computer Science , 81(2):317--324, 1991

    1991

  38. [46]

    M \"u ller and J

    M. M \"u ller and J. Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic , 171(2):102735, 2020

    2020

  39. [47]

    Maciel, T

    A. Maciel, T. Pitassi, and A. R. Woods. A new proof of the weak pigeonhole principle. In Proceedings of the 32nd Annual ACM Symposium on Theory of Computing , pages 368--377, 2000

    2000

  40. [48]

    C. H. Papadimitriou. On the complexity of the parity argument and other inefficient proofs of existence. Journal of Computer and System Sciences , 48(3):498--532, 1994

    1994

  41. [49]

    Pudl \'a k and S

    P. Pudl \'a k and S. R. Buss. How to lie without being (easily) convicted and the lengths of proofs in propositional calculus. In Computer Science Logic: 8th Workshop, CSL'94 , pages 151--162, 1995

    1995

  42. [50]

    Pitassi, P

    T. Pitassi, P. Beame, and R. Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational complexity , 3:97--140, 1993

    1993

  43. [51]

    Pasarkar, C

    A. Pasarkar, C. Papadimitriou, and M. Yannakakis. Extremal combinatorics, iterated pigeonhole arguments and generalizations of PPP . In 14th Innovations in Theoretical Computer Science Conference (ITCS 2023) , volume 251, page 88, 2023

    2023

  44. [52]

    Pudl \'a k and N

    P. Pudl \'a k and N. Thapen. Alternating minima and maxima, Nash equilibria and bounded arithmetic. Annals of Pure and Applied Logic , 163(5):604--614, 2012

    2012

  45. [53]

    Pudl \'a k

    P. Pudl \'a k. Ramsey's theorem in bounded arithmetic. In Proceedings of the 4th Workshop on Computer Science Logic , pages 308--317, 1990

    1990

  46. [54]

    Pudl \'a k

    P. Pudl \'a k. The canonical pairs of bounded depth Frege systems. Annals of Pure and Applied Logic , 172(2):102892, 2021

    2021

  47. [55]

    J. B. Paris, A. J. Wilkie, and A. R. Woods. Provability of the pigeonhole principle and the existence of infinitely many primes. The Journal of Symbolic Logic , 53:1235--1244, 1988

    1988

  48. [56]

    A. A. Razborov. Pseudorandom generators hard for k - DNF resolution and polynomial calculus resolution. Annals of Mathematics , pages 415--472, 2015

    2015

  49. [57]

    R. A. Reckhow. On the lengths of proofs in the propositional calculus . PhD thesis, University of Toronto, 1975

    1975

  50. [58]

    H. Ren, R. Santhanam, and Z. Wang. On the range avoidance problem for circuits. In 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS) , pages 640--650, 2022

    2022

  51. [59]

    L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time (preliminary report). In Annual ACM Symposium on Theory of Computing , pages 1--9, 1973

    1973

  52. [60]

    Skelley and N

    A. Skelley and N. Thapen. The provably total search problems of bounded arithmetic. Proceedings of the London Mathematical Society , 103(1):106--138, 2011

    2011

  53. [61]

    N. Thapen. A model-theoretic characterization of the weak pigeonhole principle. Annals of Pure and Applied Logic , 118(1-2):175--195, 2002

    2002

  54. [62]

    N. Thapen. Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem. Archive for Mathematical Logic , 50(7):665--680, 2011

    2011

  55. [63]

    S. Toda. PP is as hard as the polynomial-time hierarchy. SIAM Journal on Computing , 20(5):865--877, 1991

    1991

  56. [64]

    Valiant and V

    L. Valiant and V. Vazirani. NP is a easy as detecting unique solutions. Theoretical computer science , 47(1):85--93, 1986

    1986

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.