Equiconsistency of the Minimalist Foundation with its classical version

TL;DR

This paper demonstrates that the Minimalist Foundation's two levels are equiconsistent and compatible with classical mathematics, extending these results to impredicative versions and related type theories.

Contribution

It establishes the equiconsistency of the Minimalist Foundation's levels and its classical extension, showing compatibility with classical and impredicative mathematics.

Findings

The two levels of MF are equiconsistent via interpretation.

The classical extension emTT^c is equiconsistent with emTT.

Impredicative versions of MF are also equiconsistent with classical counterparts.

Abstract

The Minimalist Foundation, for short MF, was conceived by the first author with G. Sambin in 2005, and fully formalized in 2009, as a common core among the most relevant constructive and classical foundations for mathematics. To better accomplish its minimality, MF was designed as a two-level type theory, with an intensional level mTT, an extensional one emTT, and an interpretation of the latter into the first. Here, we first show that the two levels of MF are indeed equiconsistent by interpreting mTT into emTT. Then, we show that the classical extension emTT^c is equiconsistent with emTT by suitably extending the G\"odel-Gentzen double-negation translation of classical logic in the intuitionistic one. As a consequence, MF turns out to be compatible with classical predicative mathematics \`a la Weyl, contrary to the most relevant foundations for constructive mathematics. Finally, we show that the chain of equiconsistency results for MF can be straightforwardly extended to its impredicative version to deduce that Coquand-Huet's Calculus of Constructions equipped with basic inductive types is equiconsistent with its extensional and classical versions too.