Fernández Duque, DavidAguilar Enríquez, Miguel Alejandro2024-10-012024-10-012024-09https://hdl.handle.net/2445/215518Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona. Curs: 2023-2024. Tutor: David Fernández-DuqueThe main goal of this work is to formalize the Mountain Pass Theorem of Ambrosetti and Rabinowitz within the formal subsystem of second order arithmetic known as ACA0. We develop some Analysis within this system to have access to the space of continuous functions from [0, 1] into a separable Banach space and from there built formalized proofs of the basic ingredients of the Mountain Pass Theorem: The deformation lemma and the minimax principle that proves the theorem itself.72 p.application/pdfengcc by-nc-nd (c) Aguilar Enríquez, 2024http://creativecommons.org/licenses/by-nc-nd/3.0/es/Lògica matemàticaAritmèticaEspais de HilbertEspais de BanachTreballs de fi de màsterMathematical logicArithmeticHilbert spaceBanach spacesMaster's thesisinfo:eu-repo/semantics/masterThesisinfo:eu-repo/semantics/openAccess