# name
The mountain pass theorem on subsystems of second order arithmetic

# metadata.dc.description[].value
Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona. Curs: 2023-2024. Tutor: David Fernández-Duque

# metadata.dc.description.abstract[].value
The 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.

# metadata.dc.source[].value
Màster Oficial - Pure and Applied Logic / Lògica Pura i aplicada

# metadata.dc.title[].value
The mountain pass theorem on subsystems of second order arithmetic