Techniques in weak analysis for conservation results
António M. Fernandes, Fernando A.F. Ferreira, Gilda Ferreira · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · 2013
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.