Proof mining and combinatorics : Program extraction for Ramsey's theorem for pairs (original) (raw)
Kreuzer, Alexander P. (2012)
Proof mining and combinatorics : Program extraction for Ramsey's theorem for pairs.
Technische Universität Darmstadt
Ph.D. Thesis, Primary publication
| Item Type: | Ph.D. Thesis |
|---|---|
| Type of entry: | Primary publication |
| Title: | Proof mining and combinatorics : Program extraction for Ramsey's theorem for pairs |
| Language: | English |
| Referees: | Kohlenbach, Prof. Dr. Ulrich ; Avigad, Prof. PhD Jeremy ; Martin, Prof. Dr. Ziegler |
| Date: | 21 May 2012 |
| Place of Publication: | Darmstadt |
| Date of oral examination: | 13 April 2012 |
| Corresponding Links: | Related workRelated workRelated work |
| 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. |
| Alternative Abstract: | Alternative AbstractLanguageIn dieser Arbeit untersuchen wir die beweistheoretische Stärke des Satzes von Ramsey für Paare. Wir entwickeln eine Methode, um Programme aus Beweisen, die diesen Satz verwenden, zu extrahieren. Des weiteren analysieren wir die Stärke von Varianten des Bolzano-Weierstraß Prinzips. Wir zeigen, dass der Satz von Ramsey eine Variante impliziert und dass damit unsere Programmextraktionsmethode anwendbar ist. Wir entwickeln auch eine Methode zur Extraktion von Programm aus Beweisen, die freie Ultrafilter verwenden. Die Methode basiert auf Techniken, die wir für die Extraktion von Programmen aus Beweisen, die den Satz von Ramsey verwenden, entwickelt haben.German |
| 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 |
| URN: | urn:nbn:de:tuda-tuprints-29720 |
| Classification DDC: | 500 Science and mathematics > 510 Mathematics |
| Divisions: | 04 Department of Mathematics04 Department of Mathematics > Logic |
| Date Deposited: | 24 May 2012 09:37 |
| Last Modified: | 09 Jul 2020 00:03 |
| URI: | https://tuprints.ulb.tu-darmstadt.de/id/eprint/2972 |
| PPN: | 301298130 |
| Export: |
Actions (login required)
 |
View Item |
|---|