One Mathematic(s) or Many? Foundations of Mathematics in Today's Mathematical Practice

TL;DR

This paper discusses the limitations of traditional Hilbert-style foundations of mathematics and explores alternative foundations like Univalent Foundations, emphasizing their interpretability and the multiplicity of mathematical foundations.

Contribution

It analyzes the practical and theoretical roles of different mathematical foundations, highlighting the compatibility and reconstructive potential of alternative systems like Univalent Foundations.

Findings

Hilbert-style foundations are limited for practical verification tasks

Alternative foundations like Univalent Foundations are mutually interpretable with set-theoretic foundations

Mathematical theories can be reconstructed on different foundational systems

Abstract

The received Hilbert-style axiomatic foundations of mathematics has been designed by Hilbert and his followers as a tool for meta-theoretical research. Foundations of mathematics of this type fail to satisfactory perform more basic and more practically-oriented functions of theoretical foundations such as verification of mathematical constructions and proofs. Using alternative foundations of mathematics such as the Univalent Foundations is compatible with using the received set-theoretic foundations for meta-mathematical purposes provided the two foundations are mutually interpretable. Changes in foundations of mathematics do not, generally, disqualify mathematical theories based on older foundations but allow for reconstruction of these theories on new foundations. Mathematics is one but its foundations are many.