Some axioms for mathematics, with Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, 19 pages, to appear in the proceedings of FSCD'21, LIPIcs 195.
The λΠ-calculus modulo theory is a logical framework in which many logical systems can be easily encoded as theories, by using rewriting rules to define functions and dependent types. In this paper, we present in this framework a theory, called U, where the proofs of several logical systems can be expressed: Minimal, Constructive, and Ecumenical predicate logic; Minimal, Constructive, and Ecumenical simple type theory; Simple type theory with predicate subtyping, prenex predicative polymorphism, or both; the Calculus of constructions, and the Calculus of constructions with prenex predicative polymorphism. Moreover, we identify a sub-theory of U corresponding to each of these systems, and prove that, when a proof in U uses only symbols of a sub-theory, then it is a proof in that system. We obtain this last result by proving a general theorem of the λΠ-calculus modulo theory on how typing depends on the symbol types and rewriting rules declared by users.