Kreuzer, Alexander P.
Proof mining and combinatorics :
Program extraction for Ramsey's theorem for pairs.
[Ph.D. Thesis], (2012)
Dissertation (Screen Optimized) -
Available under Simple publication rights for ULB.
Download (1430Kb) | Preview
|Item Type:||Ph.D. Thesis|
|Title:||Proof mining and combinatorics : Program extraction for Ramsey's theorem for pairs|
In this thesis we give a proof-theoretic account of the strength of Ramsey's theorem for pairs and related principles. We develop a method to extract programs from proofs using this theorem. Moreover, we consider the strength of different variants of the Bolzano-Weierstraß principle. We show that Ramsey's theorem for pairs implies a variant of the Bolzano-Weierstraß principle and, hence, show that our program extraction method is applicable to proofs using this principle. Also, we develop a method to extract programs from proofs that use non-principal ultrafilters and along with this we obtain a conservation result for the statement that a non-principal ultrafilter exists. This method is based on the techniques we developed for Ramsey's theorem for pairs.
|Uncontrolled Keywords:||proof-mining, proof-theory, Ramsey's theorem for pairs, ultrafilters, Bolzano-Weierstrass, weak compactness, cohesive principle, chain antichain principle, functional interpretation, bar recursion|
|Classification DDC:||500 Naturwissenschaften und Mathematik > 510 Mathematik|
Fachbereich Mathematik > Logik
|Date Deposited:||24 May 2012 09:37|
|Last Modified:||07 Dec 2012 12:04|
|Referees:||Kohlenbach, Prof. Dr. Ulrich and Avigad, Prof. PhD Jeremy and Martin, Prof. Dr. Ziegler|
|Refereed:||13 April 2012|
Actions (login required)