# Proof interpretations: theoretical and practical aspects

## Abstract

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.

Item Type: Ph.D. Thesis
Erschienen: 2011
Creators: Gaspar, Jaime
Title: Proof interpretations: theoretical and practical aspects
Language: English
Abstract:

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.

Divisions: 04 Department of Mathematics > Logic
04 Department of Mathematics
Date Deposited: 11 Jan 2012 11:35
Official URL: urn:nbn:de:tuda-tuprints-28518
License: only the rights of use according to UrhG
Referees: Kohlenbach, Prof. Dr. Ulrich and Oliva, Reader Dr. Paulo and Streicher, Prof. Dr. Thomas
Refereed / Verteidigung / mdl. Prüfung: 6 December 2011
Alternative Abstract:
Alternative abstract Language
Wir untersuchen theoretische und praktische Aspekte von Beweisinterpretationen. (1) Theoretische Ergebnisse. (1.1) Vollständigkeit und Omega-Regel. Mit Hilfe einer Beweisinterpretation zeigen wir, dass die Peano-Arithmetik mit der Omega-Regel eine vollständige Theorie ist. (1.2) Beweisinterpretationen mit Wahrheitsprädikat. Beweisinterpretationen ohne Wahrheitsprädikat geben Informationen über die interpretierte Formel und nicht mehr über die ursprüngliche Formel. Wir präsentieren drei Heuristiken, um Wahrheitsprädikate zu Beweisinterpretationen hinzuzufügen, und geben einige Beispiele. (1.3) Kopien von klassischer Logik in intuitionistischer Logik. Die üblichen Einbettungen von klassischer Logik in intuitionistische Logik mit Hilfe von Beweisinterpretationen erzeugen alle die gleiche Kopie der klassischen Logik. Dies deutet darauf hin, dass diese Kopie eindeutig sein könnte. Wir zeigen, dass dies nicht der Fall ist und präsentieren drei verschiedene Kopien. (2) Angewandte Ergebnisse. (2.1) "Finitisierungen" des unendlichen Schubfachprinzips. Terence Tao untersucht Finitisierungen von Sätzen der Analysis. Wir betrachten Taos Ergebnisse aus dem Blickwinkel der Beweisinterpretationen und reverse mathematics. (2.2) Proof mining des Satzes von Hillam. Der Satz von Hillam charakterisiert die Konvergenz von Fixpunktiterationen. Wir extrahieren mit Hilfe von proof mining eine Rate der Konvergenz für die Fixpunktiteration.German
Export:
Suche nach Titel in: TUfind oder in Google
 Send an inquiry

#### Options (only for editors)

 View Item