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$. It was proved by K. (2025) that no proof system strong enough admits this property assuming a computational complexity conjecture and a conjecture about proof complexity generators. Here we build on Ilango (2025) and Ren et al. (2025) and prove the same result under two purely computational complexity 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).
翻译:一个命题证明系统$P$具有强可行性析取性质,当且仅当存在常数$c \geq 1$,使得每当$P$接受一个大小为$s$的证明$\bigvee_i α_i$(其中任意两个$α_i$不共享原子)时,存在某个$α_i$具有大小不超过$s^c$的$P$-证明。K.(2025)证明,在假设一个计算复杂性猜想和一个关于证明复杂性生成器的猜想的前提下,任何足够强的证明系统都不具有此性质。本文基于Ilango(2025)及Ren等人(2025)的研究,在仅依赖两个纯粹的计算复杂性假设下证明了相同结论:存在一个属于E类的语言,即使允许其查询NP预言机,仍需指数大小电路;存在Rudich(1997)意义下的P/poly半比特。