By popular demand, we will study Bounded Arithmetic as a tool for understanding the meta-mathematics of computational complexity. Our reading list will address many questions, including but not limited to:

1. Why is it so difficult to prove circuit lower bounds?
2. How do we translate between propositional tautologies and first-order statements, and when is this useful?
3. Can we prove P vs. NP is independent of some reasonable formal system?
4. How do we formalize the Natural Proofs barrier, how does such a formalization differ from Natural Properties extracted "by hand" from proofs of circuit lower bounds?

We are seeking volunteers to give talks! Please see the topics list below for suggestions, or just ask any of the organizers.

1. Overview of Topics and Organizational Meeting, Jan Pich, Jan 31.
2. Introduction to Formal Theories of Bounded Arithmetic, Antonina Kolokolova, Feb 7.

• PV, S12, APC1, Example of a PV-formalization (e.g. Cook-Levin Thm or the Reflection principle for EF)
• Cook's translation of S12 to EF
• Witnessing theorems (Herbrand, Buss, KPT)
• Ajtai's model theoretic approach to proof complexity lower bounds [Kpc, Lemma 20.1.5]

• S12-unprovability of EF lower bounds (Follows directly from Cook's translation)
• Natural proofs as unprovability results and their connection to automatability
  • Bounded Arithmetic and Theory of Razborov and Rudich, Pich.
  • Forcing with Random Variables and Proof Complexity, Krajíček. (last chapter)
• Towards the ultimate barriers: Razborov's conjecture, Rudich's conjecture
  • Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution, Razborov.
  • Super-bits, demi-bits, and NP/qpoly-natural proofs, Rudich.
  • Forcing with Random Variables and Proof Complexity, Krajíček. (again, last chapter)
• Unprovability of strong circuit lower bounds, Pich, Santhanam.
• Modular Unprovability of Circuit Upper Bounds, via KPT Witnessing, Carmosino, Kabanets, Kolokolova, Oliveira.