Consistency of NEXP Not in P/poly in a Strong Theory
summary
Shows a concrete consistency result: there is a model of V^0_2 in which the canonical NEXP complete bounded halting problem has no polynomial size circuits, so NEXP ⊄ P/poly holds inside that model. Proof stitches bounded arithmetic formalizations, PV/Cobham symbols and a nonstandard model where the propositional Jewel theorem failure of pigeonhole gives an exponential witness that translates to NEXP, then blocks polynomial witnesses via a version of the easy witness lemma. Result is unconditional and the constructed model succeeds.
AI-written summary · about
chapters (12)
- 0:00Introduction to the theorem
- 1:04Complexity and formal theories
- 3:47Consistency of formal statements
- 6:03Bounded arithmetic hierarchy
- 10:42Representing exponential time
- 14:04Witnessing and lower bounds
- 18:13Contributions of the research
- 19:35Defining the theory v02
- 27:30Formalizing the statement
- 33:34Using witness circuits
- 39:06Proof strategy and steps
- 48:43Discussion and concluding remarks
related talks
51mAllender's Conjecture and its Impacts on Meta-Complexity
49mHard Languages in NP ∩ coNP and NIZK Proofs from Unstructured Hardness
58mDichotomy Theorems for Counting Problems II
53mNew Lower Bounds and Derandomization for ACC, and a...
56mEntropy, Capacity, and Counting
01h 17mInapproximability of Constraint Satisfaction Problems V
01h 30mInapproximability of Constraint Satisfaction Problems II
52mThe Mystery of the Missing String