Unprovability of Strong Complexity Lower Bounds in Bounded Arithmetic
summary
Unconditional result: APC_1 cannot prove LB3 — a single sentence asserting a mild average‑case separation between ∃∀∃ and ∀∃∀ circuits (poly‑size π3 versus subexp‑size σ3) is not derivable in TiPV for fixed i and hence not in APC_1. Proof extracts a contradictory upper bound from any purported bounded‑arithmetic proof by a new game‑theoretic witnessing that yields algorithmic “refuters” (extensions of Krajíček’s technique and Pich–Santhanam ideas), uses log‑log truth‑table encodings and limited recursion machinery, and amplifies weak correlation into the impossible lower bound.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:36Complexity theory context
- 3:35Result summary
- 5:31Bounded arithmetic overview
- 7:23Formalization of complexity
- 10:18Theories of bounded logic
- 15:47The APC1 theory
- 18:15Previous research
- 20:43The LBI formalization
- 24:43Main results
- 28:04Proof strategy and toy model
- 37:15Formal proof overview
- 44:54Future directions
related talks
53mNew Lower Bounds and Derandomization for ACC, and a...
01h 17mInapproximability of Constraint Satisfaction Problems V
37mJourney with Eric Allender: From Turing Machines to Circuits, and Back
47mRange Avoidance, Remote Point, and Hard Partial Truth Table via Satisfying-Pairs Algorithms
56mApproximate Counting II
01h 01mThe Gospel According to TCS
51mAllender's Conjecture and its Impacts on Meta-Complexity
01h 30mInapproximability of Constraint Satisfaction Problems II