arXiv · 2604.04830
Failure of the strong feasible disjunction property
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).
Explore related subjects
Keep this discovery
Jan Krajicek. 2026-04-06. Failure of the strong feasible disjunction property. https://arxiv.org/abs/2604.04830
Cite the original work for its findings. Save a collection to share your selection of sources.