English

Failure of the strong feasible disjunction property

Computational Complexity 2026-04-14 v2 Logic

Abstract

A propositional proof system PP has the strong feasible disjunction property iff there is a constant c1c \geq 1 such that whenever PP admits a size ss proof of iαi\bigvee_i \alpha_i with no two αi\alpha_i sharing an atom then one of αi\alpha_i has a PP-proof of size sc\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).

Keywords

Cite

@article{arxiv.2604.04830,
  title  = {Failure of the strong feasible disjunction property},
  author = {Jan Krajicek},
  journal= {arXiv preprint arXiv:2604.04830},
  year   = {2026}
}

Comments

revision: more background info added