Failure of the strong feasible disjunction property

TL;DR

This paper investigates the failure of the strong feasible disjunction property in propositional proof systems under certain complexity-theoretic assumptions, combining recent work and gadget proof complexity generators.

Contribution

It combines recent research and gadget proof complexity techniques to show the property fails for strong proof systems under specific complexity hypotheses.

Findings

The property does not hold for strong proof systems under the given hypotheses.

It connects proof complexity with circuit complexity and oracle query limitations.

The results rely on assumptions about exponential circuit lower bounds and P/poly demi-bits.

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