Pincherle's theorem in reverse mathematics and computability theory (Q2304540)

The authors analyze higher-order arithmetic formalizations of Pincherle's theorem. Informally, Pincherle's theorem states that a locally bounded function on a bounded and closed subset of \(\mathbb R ^n\) is bounded. The main results concern two versions of the theorem adapted to Cantor space, \(2^{\mathbb N}\). A functional \(G:2^{\mathbb N} \to {\mathbb N}\) realizes local boundedness for the function \(F:2^{\mathbb N}\to {\mathbb N}\) if for every \(x\in 2^{\mathbb N}\) and for every \(y\) in the ball of radius \(2^{-G(x)}\) around \(x\), we have \(F(y) \le G(x)\). The original version of Pincherle's theorem, \(\mathsf{PIT_o}\), asserts that for all functionals \(F\) and \(G\), if \(G\) realizes the local boundedness of \(F\), then there is a number \(n\) such that \(F(x) \le n\) for all \(x \in 2^{\mathbb N}\). A stronger uniform version, \(\mathsf{PIT_u}\) asserts that for every \(G\) there is an \(n\) such that for every \(F\) the conclusion of the original version holds. Many equivalence results are proven in extensions of \(\mathsf{RCA}_0^\omega\), the base system for higher-order reverse mathematics created by \textit{U. Kohlenbach} [Lect. Notes Log. 21, 281--295 (2005; Zbl 1097.03053)]. For example, using \(\mathsf{IND}\) to denote the induction for all higher-order formulas, \(\mathsf{RCA}_0^\omega + \mathsf{IND} \vdash \mathsf{PIT_u} \leftrightarrow \mathsf{HBU_c}\), where \(\mathsf{HBU_c}\) is the Heine-Borel theorem for uncountable covers of \(2^{\mathbb N}\). Consequently, for all \(k\), \(\Pi^1_k \text{-}\mathsf{CA}_0^\omega + \mathsf{QF}\text{-}\mathsf{AC}^{0,1}\) cannot prove \(\mathsf{PIT_u}\). Note that \(\mathsf{QF}\text{-}\mathsf{AC}^{0,1}\) is a stronger version of choice than \(\mathsf{QF}\text{-}\mathsf{AC}^{1,0}\), which is an axiom of \(\mathsf{RCA}_0^\omega\). For the original version \(\mathsf{PIT_o}\), \(\mathsf{RCA}_0^\omega + \mathsf{QF}\text{-}\mathsf{AC}^{0,1}\vdash \mathsf{PIT_o} \leftrightarrow \mathsf{WKL}\). Working in the original base system, \(\mathsf{RCA}_0^\omega \vdash \mathsf{WKL}_0 \leftrightarrow ( \mathsf{ACA}_0 \lor \mathsf{PIT_o})\), a rare appearance of a disjunction in a reverse mathematical equivalence. Section 3 of the paper explores the relative computability of realizers associated with the theorems. Other theorems discussed include Heine's theorem, Fejé{}r's theorem, and the Lindelö{}f lemma. The paper extends previous work of \textit{D. Normann} and \textit{S. Sanders} [Ann. Pure Appl. Logic 170, No. 11, Article ID 102710, 42 p. (2019; Zbl 1430.03035)].