October 19
Sam Sanders,
TU Darmstadt/University of Leeds
Computational costs of reducing the uncountable to the finite/countable
We study the logical and computational properties of basic theorems of uncountable mathematics, including the Cousin and Lindeloef lemmas, published in 1895 and 1903. Historically, these lemmas were among the first formulations of open-cover compactness and the Lindeloef property, respectively. These notions are of great conceptual importance: the former is commonly viewed as a way of treating uncountable sets like e.g. [0,1] as 'almost finite', while the latter allows one to treat uncountable sets like e.g. the real numbers R as 'almost countable'. This reduction of the uncountable to the finite/countable turns out to have a considerable logical and computational cost: we show that the aforementioned lemmas, and many related theorems, are extremely hard to prove, while the associated sub-covers are extremely hard to compute. Indeed, in terms of the standard scale (based on comprehension axioms), a proof of these lemmas requires at least the full extent of second-order arithmetic, a system originating from Hilbert-Bernays’ Grundlagen der Mathematik. This observation has far-reaching implications for the Grundlagen's spiritual successor, the program of Reverse Mathematics, and the associated Goedel hierachy. We discuss similar theorems relating to the gauge integral, a generalisation of the Lebesgue and improper Riemann integrals that also uniquely provides a direct formalisation of Feynman's path integral.