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

TL;DR

This paper explores the logical strength of non-principal ultrafilters in higher order arithmetic, demonstrating conservativity results and providing a method for extracting computational content from proofs involving ultrafilters.

Contribution

It establishes the conservativity of ACA_0^{ omannumeral} + U over ACA_0^{ omannumeral} and develops a program extraction technique for proofs with ultrafilters.

Findings

ACA_0^{ omannumeral} + U is -conservative over ACA_0^{ omannumeral}

A method for extracting realizing terms from proofs involving ultrafilters

Proofs of  statements yield explicit computational content

Abstract

We investigate the strength of the existence of a non-principal ultrafilter over fragments of higher order arithmetic. Let U be the statement that a non-principal ultrafilter exists and let ACA_0^{\omega} be the higher order extension of ACA_0. We show that ACA_0^{\omega}+U is \Pi^1_2-conservative over ACA_0^{\omega} and thus that ACA_0^{\omega}+\U is conservative over PA. Moreover, we provide a program extraction method and show that from a proof of a strictly \Pi^1_2 statement \forall f \exists g A(f,g) in ACA_0^{\omega}+U a realizing term in G\"odel's system T can be extracted. This means that one can extract a term t, such that A(f,t(f)).