Proof interpretations: theoretical and practical aspects.
Technische Universität, Darmstadt
[Ph.D. Thesis], (2011)
Jaime Gaspar - Proof interpretations: theoretical and practical aspects -
(Jaime Gaspar - Proof interpretations: theoretical and practical aspects)
Available under Simple publication rights for ULB.
Download (1MB) | Preview
|Item Type:||Ph.D. Thesis|
|Title:||Proof interpretations: theoretical and practical aspects|
We study theoretical and practical aspects of proof theoretic tools called proof interpretations.
(1) Theoretical contributions.
(1.1) Completeness and omega-rule. Using a proof interpretation, we prove that Peano arithmetic with the omega-rule is a complete theory.
(1.2) Proof interpretations with truth. Proof interpretations without truth give information about the interpreted formula, not the original formula. We give three heuristics on hardwiring truth and apply them to several proof interpretations.
(1.3) Copies of classical logic in intuitionistic logic. The usual proof interpretations embedding classical logic in intuitionistic logic give the same copy of classical logic, suggesting uniqueness. We present three different copies.
(2) Practical contributions.
(2.1) "Finitary" infinite pigeonhole principles. Terence Tao studied finitisations of statements in analysis. We take a logic view at Tao's finitisations through the lenses of proof interpretations and reverse mathematics.
(2.2) Proof mining Hillam's theorem. Hillam's theorem characterises the convergence of fixed point iterations. We proof mine it, getting a "finitary rate of convergence" of the fixed point iteration.
|Place of Publication:||Darmstadt|
|Classification DDC:||500 Naturwissenschaften und Mathematik > 510 Mathematik|
|Divisions:||Fachbereich Mathematik > Logik|
|Date Deposited:||11 Jan 2012 11:35|
|Last Modified:||07 Dec 2012 12:04|
|Referees:||Kohlenbach, Prof. Dr. Ulrich and Oliva, Reader Dr. Paulo and Streicher, Prof. Dr. Thomas|
|Refereed:||6 December 2011|