NON-PRINCIPAL ULTRAFILTERS, PROGRAM EXTRACTION AND HIGHER-ORDER REVERSE MATHEMATICS

作者：Kreuzer Alexander P^*

来源：Journal of Mathematical Logic, 2012, 12(1): 1250002.

DOI：10.1142/S021906131250002X

• Ultrafilter
• conservation
• program extraction
• functional interpretation
• higher-order reverse mathematics

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 on N 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 for all f there exists g A(qf)(f, g) in ACA(0)(omega) + (U) a realizing term in Godel%26apos;s system T can be extracted. This means that one can extract a term t epsilon T, such that for all f A(qf)(f, t(f)).

• 出版日期2012-6