Non-principal ultrafilters, program extraction and higher-order reverse mathematics (Q2909619)

The author studies the strength of a non-principal ultrafilter in the context of higher-order reverse mathematics. This field, as described by \textit{U. Kohlenbach} [Lect. Notes Log. 21, 281--295 (2005; Zbl 1097.03053)], involves a generalization of second-order theories of arithmetic, such as \(\text{RCA}_0\) and \(\text{ACA}_0\), to corresponding theories of arithmetic in all finite types, such as \(\text{RCA}_0^\omega\) and \(\text{ACA}_0^\omega\). The author defines a principle \(U\), in the language of third-order arithmetic, stating the existence of a non-principal ultrafilter on the natural numbers.NEWLINENEWLINEThe main result is that, although \(\text{ACA}_0^\omega + U\) is strictly stronger than \(\text{ACA}_0^\omega\), it is \(\Pi^1_2\) conservative over second-order \(\text{ACA}_0\), and thus conservative over \(\text{PA}\) for sentences of first-order arithmetic. The conservation results are proved as corollaries of a program extraction theorem that produces a witnessing term in Gödel's system \(T\). Key steps include a normalization theorem due to the author and \textit{U. Kohlenbach} [J. Symb. Log. 77, No. 3, 853--895 (2012; Zbl 1254.03112)] and an approximation result using ultrafilters on countable algebras of sets. The author states that the theorems and techniques of the paper can be applied to analyze mathematical theorems with proofs that use ultralimits and nonstandard methods that can be formalized in \(\text{ACA}_0^\omega + U\), but that the techniques of the paper do not directly address the problem of the strength of Hindman's theorem.