Abstract

The notion of conservativity traces back to the method of ideal elements, which has been widely used in various areas of mathematics throughout history. Since Hilbert’s program, conservativity has become a key topic in logic and foundations of mathematics, promoting the design of foundational systems, which, on the one hand, have rich and expressive languages and allow for smooth development of mathematics, and, on the other hand, can be reduced to more basic theories such as those of arithmetic. In this work, we will discuss the conservativity over arithmetic for the Minimalist Foundation, a two-level dependent type theory, first conceived by M.E. Maietti and G. Sambin in [1] and later fully formalized by Maietti in [2], proposed as a common core among the plurality of foundations for mathematics. In particular, we will show that its classical, first-order version is conservative over Peano Arithmetic, and we will argue why this is a peculiar property of the Minimalist Foundation compared to other major foundations. The main tool used to obtain such result is an extension of Gödel’s double-negation translation for arithmetic to the Minimalist Foundation developed in joint work with Maietti [3].

[1] Maietti, M. E. and Sambin, G. (2005). “Toward a minimalist foundation for constructive mathematics”. From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics”, (L. Crosilla and P. Schuster eds.) Oxford University Press.

[2] Maietti, M. E. (2009). “A minimalist two-level foundation for constructive mathematics”. Annals of Pure and Applied Logic.

[3] Maietti, M. E. and Sabelli, P. (2025). “Equiconsistency of the Minimalist Foundation with its classical version”. Annals of Pure and Applied Logic.