pith. sign in

arxiv: 2604.04830 · v2 · submitted 2026-04-06 · 💻 cs.CC · math.LO

Failure of the strong feasible disjunction property

Jan Krajicek This is my paper

Pith reviewed 2026-05-10 19:00 UTC · model grok-4.3

classification 💻 cs.CC math.LO
keywords proof complexityfeasible disjunction propertypropositional proof systemscircuit complexitydemi-bitsgadget generators
0
0 comments X

The pith

Strong proof systems fail the strong feasible disjunction property under two hardness hypotheses.

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

The paper establishes that the strong feasible disjunction property fails for sufficiently strong propositional proof systems. This property requires that a short proof of a disjunction of variable-disjoint formulas yields a short proof of at least one individual formula. The argument combines a gadget-based proof generator with recent circuit lower bound techniques to derive the failure from two assumptions on exponential hardness. A reader would care because the property captures a basic efficiency expectation for how proofs handle independent alternatives, and its absence limits what strong systems can achieve.

Core claim

Under the assumptions that some language in E requires exponential-size circuits even with NP-oracle gates and that a P/poly demi-bit exists, the strong feasible disjunction property does not hold for strong enough proof systems.

What carries the argument

The gadget proof complexity generator, which converts circuit hardness into families of hard disjunctions whose individual disjuncts remain hard to prove.

If this is right

  • Strong proof systems cannot efficiently reduce proofs of variable-disjoint disjunctions to proofs of single disjuncts.
  • The efficiency of disjunction handling is separated from the overall strength of the proof system.
  • Proof lower bounds derived from the gadget construction apply directly to any system possessing the property.

Where Pith is reading between the lines

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

  • The result tightens the connection between circuit hardness in E and structural limitations inside proof systems.
  • If the hypotheses hold, similar gadget reductions may rule out other natural proof properties.
  • One could test the conclusion by seeking explicit disjunctions that remain hard even when one disjunct is easy.

Load-bearing premise

The two hypotheses on exponential NP-oracle circuit hardness for an E-language and the existence of a P/poly demi-bit; if either is false the failure of the property need not follow.

What would settle it

Either construct a strong proof system that satisfies the strong feasible disjunction property for some constant c, or disprove one of the two hypotheses by showing all E-languages have subexponential NP-oracle circuits or that no P/poly demi-bit exists.

read the original abstract

A propositional proof system $P$ has the strong feasible disjunction property iff there is a constant $c \geq 1$ such that whenever $P$ admits a size $s$ proof of $\bigvee_i \alpha_i$ with no two $\alpha_i$ sharing an atom then one of $\alpha_i$ has a $P$-proof of size $\le s^c$. We combine the work of Ilango (2025) and Ren et al. (2025) with the gadget proof complexity generator of K. (2007) and rule out the property for strong enough proof systems under the following two hypotheses: - there exists a language in class E that requires exponential size circuits even if they are allowed to query an NP oracle, - there exists a P/poly demi-bit in the sense of Rudich (1997).

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

1 major / 2 minor

Summary. The paper claims that the strong feasible disjunction property fails for sufficiently strong propositional proof systems, conditionally on two hypotheses: the existence of a language in E requiring exponential-size circuits even with NP-oracle access, and the existence of a P/poly demi-bit (in Rudich's sense). The argument combines results from Ilango (2025) and Ren et al. (2025) with the gadget generator construction of K. (2007) to rule out the property.

Significance. If the composition of the cited 2025 results with the 2007 gadget generator can be verified in detail, the manuscript would supply a useful conditional negative result in proof complexity, showing that a natural strengthening of the feasible disjunction property is incompatible with standard complexity assumptions for strong enough systems. The conditional framing is appropriate and avoids overclaiming; the work builds directly on recent circuit-complexity advances without introducing new unstated parameters.

major comments (1)
  1. [Main construction / proof of Theorem 1 (or equivalent)] The high-level strategy in the abstract and introduction combines Ilango (2025), Ren et al. (2025), and the K. (2007) gadget generator, but the manuscript contains a derivation gap in the explicit verification that the gadget can be applied to the 2025 constructions without additional hypotheses or size blow-ups that would invalidate the exponential lower bound. This step is load-bearing for the central claim that the strong feasible disjunction property fails.
minor comments (2)
  1. [Introduction] Clarify the precise statement of the two hypotheses in the introduction (including any implicit size parameters) so that readers can immediately see the exact conditions under which the disjunction property is ruled out.
  2. [Introduction or related-work section] Add a short paragraph comparing the obtained conditional failure with known unconditional results or barriers for the (non-strong) feasible disjunction property.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for identifying the need for more explicit details in the central construction. We have revised the paper to address this concern directly.

read point-by-point responses

  1. Referee: [Main construction / proof of Theorem 1 (or equivalent)] The high-level strategy in the abstract and introduction combines Ilango (2025), Ren et al. (2025), and the K. (2007) gadget generator, but the manuscript contains a derivation gap in the explicit verification that the gadget can be applied to the 2025 constructions without additional hypotheses or size blow-ups that would invalidate the exponential lower bound. This step is load-bearing for the central claim that the strong feasible disjunction property fails.

    Authors: We agree that the original manuscript presented the composition at a high level and did not include a fully expanded verification of the parameter settings. In the revised version we have inserted a new subsection (immediately following the statement of Theorem 1) that carries out the explicit verification. The gadget generator of K. (2007) is applied to the E-language lower bound of Ilango (2025) and the demi-bit of Ren et al. (2025) in a black-box manner; the only size overhead is a polynomial factor in the input length, which does not disturb the exponential lower bound because the original circuit-size lower bounds are of the form 2^Ω(n). No additional hypotheses are introduced, and the NP-oracle access is preserved throughout the reduction. We have also added a short appendix containing the full size calculations for the referee's convenience. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper presents a conditional result ruling out the strong feasible disjunction property for strong proof systems, explicitly under two external hypotheses (an E-language requiring exponential NP-oracle circuits and existence of a P/poly demi-bit). The derivation combines independent prior results from Ilango (2025), Ren et al. (2025), and the 2007 gadget construction. No step reduces by definition or construction to its own inputs, no parameter is fitted and renamed as a prediction, and the self-citation to the 2007 gadget serves as a reusable tool rather than a load-bearing justification that collapses the new claim. The hypotheses are stated as sufficient conditions, not derived internally, so the argument remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on two unproven domain assumptions from complexity theory plus the correctness of the three cited prior works; no free parameters or invented entities are introduced.

axioms (2)
  • domain assumption There exists a language in class E that requires exponential size circuits even if they are allowed to query an NP oracle.
    First hypothesis invoked to rule out the property.
  • domain assumption There exists a P/poly demi-bit in the sense of Rudich (1997).
    Second hypothesis invoked to rule out the property.

pith-pipeline@v0.9.0 · 5434 in / 1307 out tokens · 70717 ms · 2026-05-10T19:00:36.450956+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]

    Alekhnovich, E

    M. Alekhnovich, E. Ben-Sasson, A. A. Razborov, and A. Wigderson, Pseudorandom generators in propositional proof complexity,SIAM J. on Computing,34(1), (2004), pp.67-88

    work page 2004

  2. [2]

    S. A. Cook and J. Kraj´ ıˇ cek, Consequences of the provability ofN P⊆ P/polyJ. of Symbolic Logic,72(4), (2007), pp.1353-1371

    work page 2007

  3. [3]

    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

  4. [4]

    R.Ilango, The Oracle Derandomization Hypothesis is False (And More) Assuming No Natural Proofs, in:Electronic Colloquium on Computa- tional Complexity, Report No.190, (2025)

    work page 2025

  5. [5]

    Khaniki, Jump operators, Interactive Proofs and Proof Complex- ity Generators, in:Proc

    E. Khaniki, Jump operators, Interactive Proofs and Proof Complex- ity Generators, in:Proc. 65th Annual Symposium on Foundations of Computer Science(FOCS 2024), (2024), pp.573-593

    work page 2024

  6. [6]

    Kraj´ ıˇ cek, On the weak pigeonhole principle,Fundamenta Mathemat- icae, Vol.170(1-3), (2001), pp.123-140

    J. Kraj´ ıˇ cek, On the weak pigeonhole principle,Fundamenta Mathemat- icae, Vol.170(1-3), (2001), pp.123-140

    work page 2001

  7. [7]

    Kraj´ ıˇ cek, A proof complexity generator, in:Proc

    J. Kraj´ ıˇ cek, A proof complexity generator, in:Proc. from the 13th Int. Congress of Logic, Methodology and Philosophy of Science (Beijing, Au- gust 2007), King’s College Publications, London, ser. Studies in Logic and the Foundations of Mathematics. Eds. C.Glymour, W.Wang, and D.Westerstahl, (2009), pp.185-190

    work page 2007

  8. [8]

    Kraj´ ıˇ cek, Dual weak pigeonhole principle, pseudo-surjective func- tions, and provability of circuit lower bounds,J

    J. Kraj´ ıˇ cek, Dual weak pigeonhole principle, pseudo-surjective func- tions, and provability of circuit lower bounds,J. of Symbolic Logic, 69(1), (2004), pp.265-286

    work page 2004

  9. [9]

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

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

    work page 2011

  10. [10]

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

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

    work page 2019

  11. [11]

    Kraj´ ıˇ cek, On the existence of strong proof complexity generators, Bull

    J. Kraj´ ıˇ cek, On the existence of strong proof complexity generators, Bull. of Symbolic Logic,30(1), (March 2024), pp.20-40. 10

    work page 2024

  12. [12]

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

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

    work page 2025

  13. [13]

    A. A. Razborov, Unprovability of lower bounds on the circuit size in cer- tain fragments of bounded arithmetic,Izvestiya of the R.A.N.,59(1), (1995), pp.201-224

    work page 1995

  14. [14]

    H.Ren, Y.Wang, and Y.Zhong, Hardness of Range Avoidance and Proof Complexity Generators from Demi-Bits, in:Innovations in Theoretical Computer Science(ITCS 2026), accepted

    work page 2026

  15. [15]

    Rudich, Super-bits, demi-bits, andN P/qpoly-natural proofs, in: Proc

    S. Rudich, Super-bits, demi-bits, andN P/qpoly-natural proofs, in: Proc. of the 1st Int.Symp. on Randomization and Approximation Tech- niques in Computer Science, LN in Computer Science, Springer-Verlag, 1269, (1997), pp.85-93

    work page 1997

  16. [16]

    Sipser, A complexity theoretic approach to randomness, in:Proc

    M. Sipser, A complexity theoretic approach to randomness, in:Proc. 15th Annual ACM Symp. on Theory of Computing, ACM Press, (1983), pp.330-335

    work page 1983

  17. [17]

    Tzameret and L

    I. Tzameret and L. M. Zhang, Stretching demi-bits and nondeterminis- tic secure pseudorandomness, in:Leibniz International Proceedings in Informatics(LIPIcs),287, Dagstuhl, Leibniz-Zentrum f¨ ur Informatik, (2024), pp.95:195:22. 11

    work page 2024