Exponential lower bound for bounded-depth Frege proofs of
OpenFdVersusFdSucc.php_depth_frege_lower_boundlogicproof-complexity
Fix a depth . There is such that for all sufficiently large , every -proof of the pigeonhole principle satisfies
This is the classical exponential lower bound for bounded-depth Frege systems, the prototype of the switching-lemma lower bounds on which separations between and rest.
Preamble
import Definitions.Def_FdVersusFdSucc_defs open Filter
Formal statement
namespace FdVersusFdSucc
/-- (Krajíček–Pudlák–Woods 1995; Pitassi–Beame–Impagliazzo 1993.) For every fixed depth `d`,
`F_d`-proofs of the pigeonhole principle `PHP^{n+1}_n` require size `2^(n^ε)` for some
`ε = ε(d) > 0` and all sufficiently large `n`. -/
theorem php_depth_frege_lower_bound (d : ℕ) :
∃ ε : ℝ, 0 < ε ∧ ∀ᶠ n in atTop, ∀ π : List Sequent, IsDepthProofOf d π (php n) →
(2 : ℝ) ^ ((n : ℝ) ^ ε) ≤ (proofSize π : ℝ) := by sorry
end FdVersusFdSucc
Source
J. Krajíček, P. Pudlák, A. Woods, An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Structures & Algorithms 7(1), 1995; T. Pitassi, P. Beame, R. Impagliazzo, Exponential lower bounds for the pigeonhole principle, Computational Complexity 3, 1993. Context: Open Problem Garden, 'F_d versus F_{d+1}' (J. Krajíček), http://www.openproblemgarden.org/op/f_d_versus_f_d_1
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.