强可行析取性质的失效

命题证明系统 $P$ 具有强可行析取性质，当且仅当存在常数 $c \geq 1$，使得每当 $P$ 承认 $\bigvee_i \alpha_i$ 的大小为 $s$ 的证明且任意两个 $\alpha_i$ 不共享原子时，则某个 $\alpha_i$ 具有大小 $\le s^c$ 的 $P$-证明。我们结合 Ilango (2025) 和 Ren 等人 (2025) 的工作与 K. (2007) 的 gadget 证明复杂度生成器，在以下两个假设下排除了足够强证明系统的该性质：- 存在一个在允许查询 NP 预言机的情况下仍需要指数规模电路的语言，- 存在 Rudich (1997) 意义上的 P/poly 半比特。