A growing collection of my own surveys and notes, alongside recommendations of other writing I’ve found valuable. Entries marked Mine are my own.
Bounded arithmetic (or feasible mathematics) corresponds to mathematical theories relying on concepts only from a complexity class, ranging from AC⁰, P, PSPACE, and even beyond.
A gentle introduction to Cook’s theory PV targeting to computer scientists. Compared to existing textbooks, it features an informal definition of PV based on three postulates, which captures the high-level intuition, as well as a careful roadmap from axioms to formalizations of complicated mathematics.
A recent comprehensive survey on unprovability results in bounded arithmetic.
The comprehensive reference for proof complexity and bounded arithmetic — a standard textbook to reach for when you want a full picture of the field.