Failure of the strong feasible disjunction property
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910124432424960 |
|---|---|
| author | Krajicek, Jan |
| author_facet | Krajicek, Jan |
| contents | 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 α_i$ with no two $α_i$ sharing an atom then one of $α_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). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_04830 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Failure of the strong feasible disjunction property Krajicek, Jan Computational Complexity Logic O3F20, 68Q15 F.1.3; F.4.1 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 α_i$ with no two $α_i$ sharing an atom then one of $α_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). |
| title | Failure of the strong feasible disjunction property |
| topic | Computational Complexity Logic O3F20, 68Q15 F.1.3; F.4.1 |
| url | https://arxiv.org/abs/2604.04830 |