Kreuzer, Alexander P. (2012)
Proof mining and combinatorics : Program extraction for Ramsey's theorem for pairs.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung
Kurzbeschreibung (Abstract)
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.
| Typ des Eintrags: | Dissertation | ||||
|---|---|---|---|---|---|
| Erschienen: | 2012 | ||||
| Autor(en): | Kreuzer, Alexander P. | ||||
| Art des Eintrags: | Erstveröffentlichung | ||||
| Titel: | Proof mining and combinatorics : Program extraction for Ramsey's theorem for pairs | ||||
| Sprache: | Englisch | ||||
| Referenten: | Kohlenbach, Prof. Dr. Ulrich ; Avigad, Prof. PhD Jeremy ; Martin, Prof. Dr. Ziegler | ||||
| Publikationsjahr: | 21 Mai 2012 | ||||
| Datum der mündlichen Prüfung: | 13 April 2012 | ||||
| URL / URN: | urn:nbn:de:tuda-tuprints-29720 | ||||
| Zugehörige Links: | |||||
| Kurzbeschreibung (Abstract): | 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. |
||||
| Alternatives oder übersetztes Abstract: |
|
||||
| Freie Schlagworte: | proof-mining, proof-theory, Ramsey's theorem for pairs, ultrafilters, Bolzano-Weierstrass, weak compactness, cohesive principle, chain antichain principle, functional interpretation, bar recursion | ||||
| Sachgruppe der Dewey Dezimalklassifikatin (DDC): | 500 Naturwissenschaften und Mathematik > 510 Mathematik | ||||
| Fachbereich(e)/-gebiet(e): | 04 Fachbereich Mathematik 04 Fachbereich Mathematik > Logik |
||||
| Hinterlegungsdatum: | 24 Mai 2012 09:37 | ||||
| Letzte Änderung: | 05 Mär 2013 10:01 | ||||
| PPN: | |||||
| Referenten: | Kohlenbach, Prof. Dr. Ulrich ; Avigad, Prof. PhD Jeremy ; Martin, Prof. Dr. Ziegler | ||||
| Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: | 13 April 2012 | ||||
| Zugehörige Links: | |||||
| Export: | |||||
| Suche nach Titel in: | TUfind oder in Google | ||||
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum