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.