2017/11/30 by Dag Normann, Sam Sanders · 1 citation
Mathematics · #Algebraic and Geometric Analysis #Compact space #Countable set #Extension (predicate logic) #Generalization #Lemma (botany) #Mathematical and Theoretical Analysis #Path (computing) #Set theory #Uncountable set #advanced mathematical theories #math.LO #msc:03B30 #msc:03D65
paper · pdf · doi:10.1142/s0219061319500016
published as Journal of Mathematical Logic, 2018 · 35 pages with one figure. The content of this version extends the published version in that Sections 3.3.4 and 3.4 below are new. Small corrections/additions have also been made to reflect new developments
openalex created_date 2017/12/04 · openalex publication_date 2018/11/09 · arxiv created 2019/03/11 · arxiv updated 2019/03/12 · openalex updated_date 2026/08/05
We study the logical and computational properties of basic theorems of uncountable mathematics, including the Cousin and Lindelöf lemma published in 1895 and 1903. Historically, these lemmas were among the first formulations of open-cover compactness and the Lindelöf 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. ℝ 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 Gödel hierachy. We also show that the Cousin lemma is essential for the development of the gauge integral, a generalisation of the Lebesgue and improper Riemann integrals that also uniquely provides a direct formalisation of Feynman's path integral.