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