Fernandes, AntónioFerreira, FernandoFerreira, Gilda2021-02-112021-02-112013-099781575867243 (Online)9781575867236 (Print)http://hdl.handle.net/10400.2/10484We 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.engWeak analysisConservation resultsBounded arithmeticCut-eliminationForcingPolytime computabilityjournal article