Failure of the strong feasible disjunction property
Computational Complexity
2026-04-14 v2 Logic
Abstract
A propositional proof system has the strong feasible disjunction property iff there is a constant such that whenever admits a size proof of with no two sharing an atom then one of has a -proof of size . 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