pith. sign in

arxiv: 2506.20221 · v5 · submitted 2025-06-25 · 💻 cs.CC · math.LO

On NP cap coNP proof complexity generators

Jan Krajicek This is my paper

Pith reviewed 2026-05-19 08:32 UTC · model grok-4.3

classification 💻 cs.CC math.LO
keywords proof complexityNP versus coNPstudent-teacher modelbounded arithmeticone-way permutationspropositional proof systemssearch problemstautology
0
0 comments X

The pith

Hardness of a disjunction search problem for proof systems implies NP not equal to coNP under a model-theoretic assumption.

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

The paper defines a search problem DD_P tied to a propositional proof system P. Given a P-proof of a disjunction whose formulas share no atoms, the task is to locate the tautological formula. It formulates hypothesis (ST) that for some strong P this search problem admits no solution in the student-teacher model using a polynomial-time student and a constant number of rounds. The hypothesis follows from the existence of hard one-way permutations. Under an assumption on the existence of extensions of models of bounded arithmetic, the paper shows that (ST) implies NP not equal to coNP.

Core claim

Motivated by the theory of proof complexity generators we consider the Σ₂ᵖ search problem DD_P determined by a propositional proof system P: given a P-proof π of a disjunction ∨ᵢ αᵢ, no two αᵢ having an atom in common, find i such that αᵢ ∈ TAUT. We formulate a hypothesis (ST) that for some strong proof system P the problem DD_P is not solvable in the student-teacher model with a p-time student and a constant number of rounds. The hypothesis follows from the existence of hard one-way permutations. We prove, using a model-theoretic assumption, that (ST) implies NP ≠ coNP. The assumption concerns the existence of extensions of models of a bounded arithmetic theory.

What carries the argument

The search problem DD_P for a propositional proof system P, which requires identifying the tautological disjunct in a proven variable-disjoint disjunction.

If this is right

  • Hard one-way permutations imply (ST) for some strong proof system P.
  • Under the model assumption, (ST) yields NP not equal to coNP.
  • The student-teacher model with constant rounds and a polynomial-time student cannot decide the relevant tautology search task.
  • Connections between proof complexity generators and the NP versus coNP question can be established via model theory of bounded arithmetic.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Establishing the model extension property for concrete bounded arithmetic theories would make the separation of NP and coNP follow directly from the existence of hard one-way permutations.
  • The student-teacher protocol for DD_P may correspond to restricted forms of interactive computation that separate complexity classes when combined with proof system strength.
  • One could test the approach by checking whether specific strong proof systems admit constant-round student-teacher solutions for variable-disjoint disjunctions.
  • Similar search problems could be defined for other proof systems to derive additional conditional separations in complexity theory.

Load-bearing premise

The model-theoretic assumption on the existence of extensions of models of a bounded arithmetic theory holds.

What would settle it

A concrete model of the relevant bounded arithmetic theory that admits no proper extension satisfying the required properties, or an explicit constant-round polynomial-time student strategy solving DD_P for a strong proof system together with a demonstration that NP equals coNP.

read the original abstract

Motivated by the theory of proof complexity generators we consider the following $\Sigma^p_2$ search problem $\mbox{DD}_P$ determined by a propositional proof system $P$: given a $P$-proof $\pi$ of a disjunction $\bigvee_i {\alpha}_i$, no two $\alpha_i$ having an atom in common, find $i$ such that $\alpha_i \in \mbox{TAUT}$. We formulate a hypothesis (ST) that for some strong proof system $P$ the problem $\mbox{DD}_P$ is not solvable in the student-teacher model with a $p$-time student and a constant number of rounds. The hypothesis follows from the existence of hard one-way permutations. We prove, using a model-theoretic assumption, that (ST) implies $NP \neq coNP$. The assumption concerns the existence of extensions of models of a bounded arithmetic theory and it is open at present if it holds.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript introduces the Σ₂ᵖ search problem DD_P associated to a propositional proof system P: on input a P-proof of a disjunction ∨_i α_i in which the α_i are pairwise atom-disjoint, output an index i such that α_i is a tautology. It formulates hypothesis (ST) that, for some sufficiently strong P, DD_P is not solvable in the student-teacher model with a polynomial-time student and a constant number of rounds. The paper derives that (ST) follows from the existence of hard one-way permutations and, under an explicitly stated open model-theoretic assumption (existence of certain extensions of models of a bounded arithmetic theory), proves that (ST) implies NP ≠ coNP.

Significance. If the model-theoretic assumption holds, the result supplies a conditional proof that NP ≠ coNP from a proof-complexity hypothesis that is itself implied by standard cryptographic assumptions. This constitutes a novel model-theoretic reduction linking proof-complexity generators to the NP/coNP question. The explicit openness of the assumption and the conditional framing are clearly stated, so the contribution is appropriately scoped; it may stimulate further work on model-theoretic techniques in complexity.

minor comments (3)
  1. §2 (or the section defining DD_P): the precise syntactic requirements on the disjunction (atom-disjointness and the form of the formulas α_i) should be stated with an explicit example to clarify the search problem for readers unfamiliar with proof-complexity generators.
  2. The student-teacher protocol in the definition of (ST) is described only at a high level; adding a short formal definition (student function, teacher responses, acceptance condition) would improve readability without lengthening the paper.
  3. The manuscript should include a brief comparison, even if negative, with existing conditional separations of NP and coNP that rely on cryptographic or proof-complexity assumptions, to situate the new implication.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment and accurate summary of our manuscript. We appreciate the recognition that our conditional result provides a novel link between proof-complexity hypotheses and the NP vs coNP question, and that the openness of the model-theoretic assumption is clearly stated. Below we respond to the referee's summary.

read point-by-point responses

  1. Referee: The manuscript introduces the Σ₂ᵖ search problem DD_P associated to a propositional proof system P: on input a P-proof of a disjunction ∨_i α_i in which the α_i are pairwise atom-disjoint, output an index i such that α_i is a tautology. It formulates hypothesis (ST) that, for some sufficiently strong P, DD_P is not solvable in the student-teacher model with a polynomial-time student and a constant number of rounds. The paper derives that (ST) follows from the existence of hard one-way permutations and, under an explicitly stated open model-theoretic assumption (existence of certain extensions of models of a bounded arithmetic theory), proves that (ST) implies NP ≠ coNP.

    Authors: We thank the referee for this precise summary, which correctly reflects the definition of the search problem DD_P, the formulation of hypothesis (ST), its derivation from hard one-way permutations, and the conditional implication to NP ≠ coNP under the stated model-theoretic assumption on extensions of bounded arithmetic models. revision: no

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper derives a conditional implication: hypothesis (ST) follows from the external cryptographic assumption of hard one-way permutations, and under an explicitly open model-theoretic assumption on extensions of models of bounded arithmetic theory, (ST) implies NP ≠ coNP. This is presented as a model-theoretic reduction with the key assumption stated as unresolved in the abstract. No self-definitional equivalences, fitted inputs renamed as predictions, load-bearing self-citations, or ansatzes smuggled via prior work appear in the derivation chain. The result remains dependent on independent external assumptions rather than reducing to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central implication rests on an open model-theoretic assumption about model extensions in bounded arithmetic and on the existence of hard one-way permutations; no free parameters or new entities are introduced.

axioms (1)
  • domain assumption Existence of extensions of models of a bounded arithmetic theory
    Invoked to derive NP ≠ coNP from hypothesis (ST); explicitly noted as open.

pith-pipeline@v0.9.0 · 5687 in / 1106 out tokens · 30936 ms · 2026-05-19T08:32:31.847769+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

17 extracted references · 17 canonical work pages

  1. [1]

    Ajtai, Σ 1 1 - formulas on finite structures, Annals of Pure and Applied Logic, 24, (1983), pp.1-48

    M. Ajtai, Σ 1 1 - formulas on finite structures, Annals of Pure and Applied Logic, 24, (1983), pp.1-48

    work page 1983

  2. [2]

    Ajtai, The complexity of the pigeonhole principle, in: Proc

    M. Ajtai, The complexity of the pigeonhole principle, in: Proc. IEEE 29th Annual Symp. on Foundation of Computer Science , (1988), pp. 346-355

    work page 1988

  3. [3]

    S. R. Buss, Bounded Arithmetic. Naples, Bibliopolis, (1986)

    work page 1986

  4. [4]

    S. A. Cook, Feasibly constructive proofs and the propositional calculus, in: Proc. 7th Annual ACM Symp. on Theory of Computing (STOC), (1975), pp. 83-97. ACM Press

    work page 1975

  5. [5]

    S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems, J. Symbolic Logic, 44(1), (1979), pp.36-50

    work page 1979

  6. [6]

    S. A. Cook and N. Thapen, The strength of replacement in weak arithmetic, ACM Transactions on Computational Logic , 7:4, (2006)

    work page 2006

  7. [7]

    Kraj´ ıˇ cek,Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol

    J. Kraj´ ıˇ cek,Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol. 60, Cambridge University Press, (1995)

    work page 1995

  8. [8]

    Kraj´ ıˇ cek, On the proof complexity of the Nisan-Wigderson generator based on a hard N P ∩ coN P function, J

    J. Kraj´ ıˇ cek, On the proof complexity of the Nisan-Wigderson generator based on a hard N P ∩ coN P function, J. of Mathematical Logic , 11(1), (2011), pp.11-27. 8

    work page 2011

  9. [9]

    Kraj´ ıˇ cek, Expansions of pseudofinite structures and circuit and proof complexity, in: Liber Amicorum Alberti, eds.Jan van Eijck, Rosalie Iemhoff and Joost J

    J. Kraj´ ıˇ cek, Expansions of pseudofinite structures and circuit and proof complexity, in: Liber Amicorum Alberti, eds.Jan van Eijck, Rosalie Iemhoff and Joost J. Joosten, Tributes Ser. 30, College Publications, London, (2016), pp.195-203

    work page 2016

  10. [10]

    Kraj´ ıˇ cek,Proof complexity, Encyclopedia of Mathematics and Its Appli- cations, Vol

    J. Kraj´ ıˇ cek,Proof complexity, Encyclopedia of Mathematics and Its Appli- cations, Vol. 170, Cambridge University Press, (2019)

    work page 2019

  11. [11]

    Kraj´ ıˇ cek, A limitation on the KPT interpolation, Logical Methods in Computer Science, Volume 16, Issue 3, (2020), pp

    J. Kraj´ ıˇ cek, A limitation on the KPT interpolation, Logical Methods in Computer Science, Volume 16, Issue 3, (2020), pp. 9:19:5

    work page 2020

  12. [12]

    Kraj´ ıˇ cek,Proof complexity generators , London Mathematical Society Lecture Note Series, No

    J. Kraj´ ıˇ cek,Proof complexity generators , London Mathematical Society Lecture Note Series, No. 497, Cambridge University Press, (2025)

    work page 2025

  13. [13]

    Kraj´ ıˇ cek and P

    J. Kraj´ ıˇ cek and P. Pudl´ ak, Propositional proof systems, the consistency of first-order theories and the complexity of computations, J. Symbolic Logic, 54(3), (1989), pp.1063-1079

    work page 1989

  14. [14]

    Kraj´ ıˇ cek and P

    J. Kraj´ ıˇ cek and P. Pudl´ ak, Propositional provability in models of weak arithmetic, in: Computer Science Logic (Kaiserlautern, Oct. ’89) , eds. E. Boerger, H. Kleine-Bunning and M.M. Richter, Lecture Notes in Computer Science 440, (1990), pp. 193-210. Springer-Verlag

    work page 1990

  15. [15]

    Kraj´ ıˇ cek, P

    J. Kraj´ ıˇ cek, P. Pudl´ ak, and J. Sgall, Interactive Computations of Optimal Solutions, in: B. Rovan (ed.): Mathematical Foundations of Computer Sci- ence (B. Bystrica, August ’90), Lecture Notes in Computer Science 452, Springer-Verlag, (1990), pp. 48-60

    work page 1990

  16. [16]

    Kraj´ ıˇ cek, P

    J. Kraj´ ıˇ cek, P. Pudl´ ak and G. Takeuti, Bounded arithmetic and the polyno- mial hierarchy, Annals of Pure and Applied Logic , 52, (1991), pp.143-153

    work page 1991

  17. [17]

    Pich and R

    J. Pich and R. Santhanam, Strong Co-Nondeterministic Lower Bounds for NP Cannot be Proved Feasibly, in:Proc. of the 53rd Annual ACM SIGACT Symposium on Theory of Computing (STOC), (2021), pp.223-233. 9

    work page 2021