TU Darmstadt / ULB / TUbiblio

From constructive mathematics to computable analysis via the realizability interpretation

Lietz, Peter (2005)
From constructive mathematics to computable analysis via the realizability interpretation.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

Kurzbeschreibung (Abstract)

Constructive mathematics is mathematics without the use of the principle of the excluded middle. There exists a wide array of models of constructive logic. One particular interpretation of constructive mathematics is the realizability interpretation. It is utilized as a metamathematical tool in order to derive admissible rules of deduction for systems of constructive logic or to demonstrate the equiconsistency of extensions of constructive logic. In this thesis, we employ various realizability models in order to logically separate several statements about continuity in constructive mathematics. A trademark of some constructive formalisms is predicativity. Predicative logic does not allow the definition of a set by quantifying over a collection of sets that the set to be defined is a member of. Starting from realizability models over a typed version of partial combinatory algebras we are able to show that the ensuing models provide the features necessary in order to interpret impredicative logics and type theories if and only if the underlying typed partial combinatory algebra is equivalent to an untyped pca. It is an ongoing theme in this thesis to switch between the worlds of classical and constructive mathematics and to try and use constructive logic as a method in order to obtain results of interest also for the classically minded mathematician. A classical mathematician can see the value of a solution algorithm as opposed to an abstract proof of the existence of a solution, but he or she would not insist on a constructive correctness proof for that algorithm. We introduce a class of formulae which is supposed to capture this pragmatic point of view. The class is defined in such a way that existence statements have a strong status, yet the correctness of an operation need only be proved classically. Moreover, this theory contains only classically true formulae. We pose the axiomatization of this class of formulae as an open problem and provide partial results. Like ordinary recursion theory, computable analysis is a branch of classical mathematics. It applies the concept of computability to entities of analysis by equipping them with a generalization of Gödelizations called representations. Representations can be organized into a realizability category with rich logical properties. In this way, natural representations of spaces can be found by categorically interpreting the description of the underlying set of a space. Computability and non-computability results can be and are shown on an abstract, logical level. Finally, we turn to another application of realizability models, the field of strong normalization proofs for type theoretic frameworks. We will argue why we think that the modified realizability topos is not suited for this purpose and propose an alternative.

Typ des Eintrags: Dissertation
Erschienen: 2005
Autor(en): Lietz, Peter
Art des Eintrags: Erstveröffentlichung
Titel: From constructive mathematics to computable analysis via the realizability interpretation
Sprache: Englisch
Referenten: Simpson, Dr. Alex
Berater: Streicher, Prof. Dr. Thomas
Publikationsjahr: 9 Februar 2005
Ort: Darmstadt
Verlag: Technische Universität
Datum der mündlichen Prüfung: 11 Februar 2004
URL / URN: urn:nbn:de:tuda-tuprints-5285
Kurzbeschreibung (Abstract):

Constructive mathematics is mathematics without the use of the principle of the excluded middle. There exists a wide array of models of constructive logic. One particular interpretation of constructive mathematics is the realizability interpretation. It is utilized as a metamathematical tool in order to derive admissible rules of deduction for systems of constructive logic or to demonstrate the equiconsistency of extensions of constructive logic. In this thesis, we employ various realizability models in order to logically separate several statements about continuity in constructive mathematics. A trademark of some constructive formalisms is predicativity. Predicative logic does not allow the definition of a set by quantifying over a collection of sets that the set to be defined is a member of. Starting from realizability models over a typed version of partial combinatory algebras we are able to show that the ensuing models provide the features necessary in order to interpret impredicative logics and type theories if and only if the underlying typed partial combinatory algebra is equivalent to an untyped pca. It is an ongoing theme in this thesis to switch between the worlds of classical and constructive mathematics and to try and use constructive logic as a method in order to obtain results of interest also for the classically minded mathematician. A classical mathematician can see the value of a solution algorithm as opposed to an abstract proof of the existence of a solution, but he or she would not insist on a constructive correctness proof for that algorithm. We introduce a class of formulae which is supposed to capture this pragmatic point of view. The class is defined in such a way that existence statements have a strong status, yet the correctness of an operation need only be proved classically. Moreover, this theory contains only classically true formulae. We pose the axiomatization of this class of formulae as an open problem and provide partial results. Like ordinary recursion theory, computable analysis is a branch of classical mathematics. It applies the concept of computability to entities of analysis by equipping them with a generalization of Gödelizations called representations. Representations can be organized into a realizability category with rich logical properties. In this way, natural representations of spaces can be found by categorically interpreting the description of the underlying set of a space. Computability and non-computability results can be and are shown on an abstract, logical level. Finally, we turn to another application of realizability models, the field of strong normalization proofs for type theoretic frameworks. We will argue why we think that the modified realizability topos is not suited for this purpose and propose an alternative.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

Konstruktive Mathematik ist Mathematik ohne die Verwendung des Prinzips tertium non datur. Es gibt eine Vielzahl unterschiedlicher Modelle für die konstruktive Logik. Eine bestimmte Interpretation der konstruktiven Mathematik ist die Realisierbarkeits-Interpretation. Sie findet Anwendung als ein metamathematisches Werkzeug welches es gestattet, zulässige Regeln oder Äquikonsistenzaussagen für logische Kalküle nachzuweisen. In dieser Dissertation verwenden wir die Realisierbarkeits-Interpretation zum Zwecke der Separierung verschiedener Aussagen über Stetig- keit im Rahmen der konstruktiven Mathematik. Eine Eigenart einiger konstruktiver Formalismen ist die Prädikativität. Prädikative Logik verbietet die Definition einer Menge durch Quantifikation über eine Familie von Mengen, welche die zu definierende Menge enthält. Ausgehend von Realisierbarkeits-Modellen über einer getypten Version partieller kombinatorischer Algebren zeigen wir, dass die zugehörigen Modelle die nötigen Eigenschaften zur Interpretation im- prädikativer Logik und Typ Theorie genau dann besitzen, wenn die zugrundeliegende partielle kombinatorische Algebra äquivalent ist zu einer ungetypten pca. Der Wechsel zwischen den Welten der konstruktiven und der klassischen Mathematik und der Versuch, die konstruktive Logik als eine Methode zu benutzen, um Resultate zu erzielen, welche von Interesse für klassische Mathematiker sind, ist ein wiederkehrendes Thema dieser Dissertation. Ein klassischer Mathematiker erkennt sehr Wohl den Wert eines Lösungsalgorithmus im Vergleich zu einem bloßen Beweis der Existenz einer Lösung, aber er wird gewöhnlich nicht darauf bestehen, dass der Korrektheitsbeweis für den Algorithmus konstruktiv ist. Wir führen eine Klasse von Formeln ein, welche diesen pragmatischen Blickwinkel erfassen soll. Die Klasse ist derart definiert, dass Existenzaussagen einen starken Status haben, Korrektheitsbeweise für Operationen jedoch nur klassisch geführt werden brauchen. Die besagte Klasse von Formeln enthält nur klassisch wahre Formeln. Wir stellen die Axiomatisierung dieser Klasse als ein Problem und bieten Teilergebnisse. Wie die Rekursionstheorie, so ist auch die berechenbare Analysis ein Zweig der klassischen Mathematik. Die berechenbare Analysis wendet das Konzept der Berechenbarkeit an auf Größen der Analysis, indem sie sie mit einer Verallgemeinerung von Gödelisierungen, genannt Darstellungen, ausstattet. Darstellungen können in einer Realisierbarkeits-Kategorie mit reichhaltigen logischen Eigenschaften zusammengefasst werden. Auf diesem Wege können natürliche Darstellungen von Räumen gefunden werden, indem man die Beschreibung der unterliegenden Menge der Räume kategoriell interpretiert. Berechenbarkeits- und Nicht-Berechenbarkeitsresultate können so auf einer abstrakten, logischen Ebene hergeleitet werden. Zuletzt wenden wir uns einer weiteren Anwedung der Realisierbarkeitsmodelle zu, nämlich dem Gebiet der starken Normalisierungbeweise für typtheoretische Kalküle. Wir legen dar warum wir denken, dass der modified realizability topos nicht das geeignete Modell für diesen Zweck ist und schlagen eine Alternative vor.

Deutsch
Freie Schlagworte: Realisierbarkeit
Schlagworte:
Einzelne SchlagworteSprache
realizabilityEnglisch
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 500 Naturwissenschaften und Mathematik > 510 Mathematik
Fachbereich(e)/-gebiet(e): 04 Fachbereich Mathematik
Hinterlegungsdatum: 17 Okt 2008 09:21
Letzte Änderung: 26 Aug 2018 21:25
PPN:
Referenten: Simpson, Dr. Alex
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 11 Februar 2004
Schlagworte:
Einzelne SchlagworteSprache
realizabilityEnglisch
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen