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

Invitation to the Logic Seminar at the National University of Singapore

Date: Wednesday, 19 March 2014, 17:00 hrs

Room: S17#04-05, Department of Mathematics, NUS

Speaker: Alexander Kreuzer

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

URL: http://www.comp.nus.edu.sg/~fstephan/logicseminar.html

Abstract:
We investigate the strength of the existence of a non-principal
ultrafilters over fragments of higher order arithmetic.

Let (U) be the statement that a non-principal ultrafilter on N exists
and let ACA_0^w be the higher order extension of ACA_0 (arithmetical
comprehension).

We show that ACA_0^w+(U) is \Pi^1_2-conservative over ACA_0^w and thus
that ACA_0^w+(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_qf(f,g) in
ACA_0^w+(U)$ a realizing term in Goedel’s system T can be extracted. This
means that one can extract a term t, such that \forall f A_qf(f,t(f)).

Best wishes,
Alexander

Leave a Reply

Your email address will not be published. Required fields are marked *