# Some Axioms for Mathematics

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
Abstract : The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory $\mathcal{U}$, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of $\mathcal{U}$ corresponding to each of these systems, and prove that, when a proof in $\mathcal{U}$ uses only symbols of a sub-theory, then it is a proof in that sub-theory.
Keywords :
Document type :
Conference papers
Domain :

https://hal.inria.fr/hal-03279749
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Tuesday, July 6, 2021 - 4:46:08 PM
Last modification on : Saturday, May 21, 2022 - 3:57:02 AM
Long-term archiving on: : Thursday, October 7, 2021 - 7:02:49 PM

### File

LIPIcs-FSCD-2021-20.pdf
Publication funded by an institution

### Citation

Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré. Some Axioms for Mathematics. FSCD 2021 - 6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires / Virtual, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.20⟩. ⟨hal-03279749⟩

Record views