Extracting programs from proofs : using Friedman's A-translation and realizability

Abstract

Das Thema dieser Dissertation basiert auf der starken Verbindung zwischen mathematischen Beweisen und Programmen, in dem Sinne, dass Beweise einen Rechengehalt haben, zusätzlich zur bloßen Vermittlung der Wahrheit ihrer Schlussfolgerung. Insbesondere beschreiben wir eine Methode zum Extrahieren von Programmen aus gegebenen klassischen arithmetischen Beweisen erster Ordnung von $\Pi_2$-Sätzen. Dies geschieht mit Hilfe einer Beweisübersetzung, die klassische Beweise in intuitionistische Beweise umwandelt, und einer Realisierbarkeitsinterpretation, die es erlaubt, intuitionistische Zeugen für Sätze aus ihren Beweisen in Form von Programmen zu extrahieren. Wir werden Kolmogorovs negative Übersetzung und Friedman's A-Übersetzung verwenden, um die Beweise zu transformieren und Realisatoren nach Kreisels modifizierter Realisierbarkeit zu extrahieren. Wir interessieren uns speziell für diese intuitionistischen Zeugen für Theoreme, weil sie Programme in Bezug auf eine Spezifikation sind, die in der Schlussfolgerung des Beweises ausgedrückt wird. Eine logische Formel $A$ mit den freien Variablen $x_1,\dots,x_r$ und $y$ kann als Spezifikation verstanden werden, wobei ein Programm, das diese Spezifikation erfüllt, eine Funktion $f$ berechnet, so dass für alle möglichen Eingabewerte $n_1,\dots,n_r$, der Satz $A[n_1 / x_1] \dots [n_r / x_r] [f (n_1, \dots, n_r) / y]$ wahr ist. Die in dieser Arbeit beschriebene Methode extrahiert Programme, die solchen Spezifikationen $A$ entsprechen, aus Beweisen, die die Existenz einer Funktion für $A$ implizieren, also aus Beweisen von Sätzen $\forall x_1 \dots \forall x_r \exists y A$. Insbesondere bietet uns die Realisierbarkeitsinterpretation eine Möglichkeit, Programme aus konstruktiven Beweisen zu extrahieren, und die Beweistransformation ermöglicht uns, diese Extraktion auch auf klassische Beweise auszuweiten.

Das Thema dieser Dissertation basiert auf der starken Verbindung zwischen mathematischen Beweisen und Programmen, in dem Sinne, dass Beweise einen Rechengehalt haben, zusätzlich zur bloßen Vermittlung der Wahrheit ihrer Schlussfolgerung. Insbesondere beschreiben wir eine Methode zum Extrahieren von Programmen aus gegebenen klassischen arithmetischen Beweisen erster Ordnung von $\Pi_2$-Sätzen. Dies geschieht mit Hilfe einer Beweisübersetzung, die klassische Beweise in intuitionistische Beweise umwandelt, und einer Realisierbarkeitsinterpretation, die es erlaubt, intuitionistische Zeugen für Sätze aus ihren Beweisen in Form von Programmen zu extrahieren. Wir werden Kolmogorovs negative Übersetzung und Friedman's A-Übersetzung verwenden, um die Beweise zu transformieren und Realisatoren nach Kreisels modifizierter Realisierbarkeit zu extrahieren. Wir interessieren uns speziell für diese intuitionistischen Zeugen für Theoreme, weil sie Programme in Bezug auf eine Spezifikation sind, die in der Schlussfolgerung des Beweises ausgedrückt wird. Eine logische Formel $A$ mit den freien Variablen $x_1,\dots,x_r$ und $y$ kann als Spezifikation verstanden werden, wobei ein Programm, das diese Spezifikation erfüllt, eine Funktion $f$ berechnet, so dass für alle möglichen Eingabewerte $n_1,\dots,n_r$, der Satz $A[n_1 / x_1] \dots [n_r / x_r] [f (n_1, \dots, n_r) / y]$ wahr ist. Die in dieser Arbeit beschriebene Methode extrahiert Programme, die solchen Spezifikationen $A$ entsprechen, aus Beweisen, die die Existenz einer Funktion für $A$ implizieren, also aus Beweisen von Sätzen $\forall x_1 \dots \forall x_r \exists y A$. Insbesondere bietet uns die Realisierbarkeitsinterpretation eine Möglichkeit, Programme aus konstruktiven Beweisen zu extrahieren, und die Beweistransformation ermöglicht uns, diese