Proof mining and combinatorics. Program extraction for Ramsey's theorem for pairs (Q2898881)

In this PhD thesis, the author develops a program extraction method for proofs that use Ramsey's theorem for pairs, using proof mining methods. Furthermore, he analyzes the strength of different variants of the Bolzano-Weierstrass principle and provides a program extraction and conservativity result for non-principal ultrafilters. In the last chapter, he shows that a generalization of the Banach contraction mapping principle follows from Ramsey's theorem for pairs over a weak basis theory. NEWLINENEWLINENEWLINE NEWLINEThe research carried out in this thesis can also be found in the following papers of the author [Math. Log. Q. 57, No. 3, 292--298 (2011; Zbl 1243.03016); Notre Dame J. Formal Logic 53, No. 2, 245--265 (2012; Zbl 1253.03090); J. Math. Log. 12, No. 1, 1250002, 16 p. (2012; Zbl 1269.03021); J. Log. Anal. 4, Article 17, 16 p. (2012; Zbl 1291.03013); Computability 1, No. 2, 171--179 (2012; Zbl 1270.03128); with \textit{U. Kohlenbach}, Notre Dame J. Formal Logic 50, No. 4, 427--444 (2009; Zbl 1221.03059); J. Symb. Log. 77, No. 3, 853--895 (2012; Zbl 1254.03112)].