Around the Minimalist Foundation: (Co)Induction and Equiconsistency

We study extensions and meta-mathematical properties of the Minimalist Foundation. The first chapter is introductory: we recall the systems of the Minimalist Foundation, reviewing their philosophical cores and main meta-mathematical results, together with a thorough exposition on how to work in them. The second chapter is devoted to considering two dual extensions of the Minimalist Foundation and their topological interpretations: with inductive predicates, adapted from the joint work with M.E. Maietti in [1], and with coinductive predicates, adapted from the preprint [2]. The last two chapters, taken from joint works with M.E. Maietti, focus on the level tower of the Minimalist Foundation, showing in particular the overall equiconsistency between the intensional level, the intuitionistic extensional level, and the classical extensional level. Bibliography [1] 2022. A topological counterpart of well-founded trees in dependent type theory. With M. E. Maietti. Electronic Notes in Theoretical Informatics and Computer Science, Volume 3. Proceedings of MFPS XXXIX. DOI: 10.46298/entics.11755 [2] 2024. A topological reading of inductive and coinductive definitions in Dependent Type Theory. arXiv preprint arXiv:2404.03494