Non-principal ultrafilters, program extraction and higher order reverse mathematics
Logic
2013-03-01 v1
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)).
Keywords
Cite
@article{arxiv.1109.4277,
title = {Non-principal ultrafilters, program extraction and higher order reverse mathematics},
author = {Alexander P. Kreuzer},
journal= {arXiv preprint arXiv:1109.4277},
year = {2013}
}