Cousin's lemma in second-order arithmetic

TL;DR

This paper analyzes the logical strength of Cousin's lemma within second-order arithmetic, establishing equivalences with well-known subsystems for different classes of functions, thereby connecting compactness principles with reverse mathematics.

Contribution

It determines the axiomatic strength of Cousin's lemma for various function classes, linking it to subsystems like WKL0, ACA0, and ATR0 in reverse mathematics.

Findings

Cousin's lemma for continuous functions is equivalent to WKL0.

Cousin's lemma for Baire class 1 functions is equivalent to ACA0.

Cousin's lemma for Baire class 2 and Borel functions is equivalent to ATR0.

Abstract

Cousin's lemma is a compactness principle that naturally arises when studying the gauge integral, a generalisation of the Lebesgue integral. We study the axiomatic strength of Cousin's lemma for various classes of functions, using Friedman and Simpson's reverse mathematics in second-order arithmetic. We prove that, over $\mathsf{RCA}_0$: (i) Cousin's lemma for continuous functions is equivalent to $\mathsf{WKL}_0$; (ii) Cousin's lemma for Baire class 1 functions is equivalent to $\mathsf{ACA}_0$; (iii) Cousin's lemma for Baire class 2 functions, or for Borel functions, are both equivalent to $\mathsf{ATR}_0$ (modulo some induction).