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\ge 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).

revision: more background info added