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^ω be the higher order extension of ACA_0. We show that ACA_0^ω+U is Π^1_2-conservative over ACA_0^ω and thus that ACA_0^ω+\U is conservative over PA. Moreover, we provide a program extraction method and show that from a proof of a strictly Π^1_2 statement \forall f \exists g A(f,g) in ACA_0^ω+U a realizing term in Gödel's system T can be extracted. This means that one can extract a term t, such that A(f,t(f)).
Connections
Explore this paper’s authors, topics and related work.
Building this map preview
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Reviews 0
Write a review
No reviews yet.
Discussion 0
Add a comment
No comments yet.