We review and describe the main techniques for setting up systems of weak
analysis, i.e. formal systems of second-order arithmetic related to subexponential
classes of computational complexity. These involve techniques of proof theory
(e.g., Herbrand’s theorem and the cut-elimination theorem) and model theoretic
techniques like forcing. The techniques are illustrated for the particular case of
polytime computability. We also include a brief section where we list the known
results in weak analysis.
