Intuitionistische Typentheorie

Eintragsnavigation

• Eintragsinhalt
• Literaturverzeichnis
• Akademische Werkzeuge
• Freunde PDF Vorschau
• Autor und Zitierinfo
• Zurück nach oben

Intuitionistische Typentheorie

Erstveröffentlichung am 12. Februar 2016; inhaltliche Überarbeitung Mo 8. Juni 2020

Die intuitionistische Typentheorie (auch konstruktive Typentheorie oder Martin-Löf-Typentheorie) ist ein formales logisches System und eine philosophische Grundlage für die konstruktive Mathematik. Es ist ein vollständiges System, das eine ähnliche Rolle für die konstruktive Mathematik spielen soll wie die Zermelo-Fraenkel-Mengenlehre für die klassische Mathematik. Es basiert auf dem Prinzip der Sätze als Typen und verdeutlicht die Brouwer-Heyting-Kolmogorov-Interpretation der intuitionistischen Logik. Es erweitert diese Interpretation auf die allgemeinere Einstellung der intuitionistischen Typentheorie und liefert somit eine allgemeine Vorstellung nicht nur davon, was ein konstruktiver Beweis ist, sondern auch davon, was ein konstruktives mathematisches Objekt ist. Die Hauptidee ist, dass mathematische Konzepte wie Elemente, Mengen und Funktionen anhand von Konzepten aus der Programmierung wie Datenstrukturen erklärt werden. Datentypen und Programme. Dieser Artikel beschreibt das formale System der intuitionistischen Typentheorie und ihre semantischen Grundlagen.

In diesem Beitrag geben wir zunächst einen Überblick über die wichtigsten Aspekte der intuitionistischen Typentheorie - eine Art „Extended Abstract“. Es ist für einen Leser gedacht, der mit der Theorie bereits einigermaßen vertraut ist. Abschnitt 2 hingegen ist für einen Leser gedacht, der mit der Theorie des intuitionistischen Typs noch nicht vertraut ist, aber mit der traditionellen Logik vertraut ist, einschließlich Aussagen- und Prädikatenlogik, Arithmetik und Mengenlehre. Hier stellen wir informell einige Aspekte vor, die die intuitionistische Typentheorie von diesen traditionellen Theorien unterscheiden. In Abschnitt 3 präsentieren wir eine grundlegende Version der Theorie, die der ersten veröffentlichten Version von Martin-Löf aus dem Jahr 1972 nahe kommt. Der Leser, der von der Informalität von Abschnitt 2 fasziniert war, wird nun im Detail sehen, wie die Theorie aufgebaut ist. Abschnitt 4 enthält dann eine Reihe wichtiger Erweiterungen der Grundtheorie. Bestimmtes,es betont die zentrale Rolle induktiver (und induktiv-rekursiver) Definitionen. In Abschnitt 5 werden die zugrunde liegenden philosophischen Ideen einschließlich der von Martin-Löf entwickelten Bedeutungstheorie vorgestellt. Während sich Abschnitt 5 mit Philosophie und Grundlagen befasst, gibt Abschnitt 6 einen Überblick über mathematische Modelle der Theorie. In Abschnitt 7 beschreiben wir schließlich einige wichtige Variationen der in den Abschnitten 3 und 4 beschriebenen Martin-Löf-Kerntheorie. Wir beschreiben einige wichtige Variationen der in den Abschnitten 3 und 4 beschriebenen Martin-Löf-Kerntheorie. Wir beschreiben einige wichtige Variationen der in den Abschnitten 3 und 4 beschriebenen Martin-Löf-Kerntheorie.

• 1. Übersicht

• 2. Sätze als Typen

  • 2.1 Intuitionistische Typentheorie: Eine neue Sichtweise auf Logik?
  • 2.2 Die Curry-Howard-Korrespondenz
  • 2.3 Sätze von Beweisobjekten
  • 2.4 Abhängige Typen
  • 2.5 Sätze als Typen in der intuitionistischen Typentheorie

• 3. Grundlegende intuitionistische Typentheorie

  • 3.1 Urteile
  • 3.2 Urteilsformulare
  • 3.3 Inferenzregeln
  • 3.4 Intuitionistische Prädikatenlogik
  • 3.5 Natürliche Zahlen
  • 3.6 Das Universum der kleinen Typen
  • 3.7 Aussagenidentität
  • 3.8 Das Axiom der Wahl ist ein Satz

• 4. Erweiterungen

  • 4.1 Das logische Framework
  • 4.2 A Former Identity Type Former
  • 4.3 Fundierte Bäume
  • 4.4 Iterative Mengen und CZF
  • 4.5 Induktive Definitionen
  • 4.6 Induktiv-rekursive Definitionen

• 5. Bedeutung Erklärungen

  • 5.1 Berechnung in kanonische Form
  • 5.2 Die Bedeutung kategorialer Urteile
  • 5.3 Die Bedeutung hypothetischer Urteile

• 6. Mathematische Modelle

  • 6.1 Kategoriale Modelle
  • 6.2 Mengen-theoretisches Modell
  • 6.3 Realisierbarkeitsmodelle
  • 6.4 Modell normaler Formen und Typprüfung

• 7. Varianten der Theorie

  • 7.1 Erweiterungstypentheorie
  • 7.2 Einwertige Grundlagen und Homotopietypentheorie
  • 7.3 Partielle und nicht standardmäßige Typentheorie
  • 7.4 Impredikative Typentheorie
  • 7.5 Beweisassistenten
• Literaturverzeichnis
• Akademische Werkzeuge
• Andere Internetquellen
• Verwandte Einträge

1. Übersicht

Wir beginnen mit einer Vogelperspektive einiger wichtiger Aspekte der intuitionistischen Typentheorie. Leser, die mit der Theorie nicht vertraut sind, können es vorziehen, sie bei der ersten Lesung zu überspringen.

Die Ursprünge der intuitionistischen Typentheorie sind Brouwers Intuitionismus und Russells Typentheorie. Wie die klassische einfache Typentheorie der Kirche basiert sie auf der Lambda-Rechnung mit Typen, unterscheidet sich jedoch darin, dass sie auf dem von Curry (1958) für die Aussagenlogik entdeckten und auf Prädikatenlogik ausgedehnten Prinzip basiert Howard (1980) und de Bruijn (1970). Diese Erweiterung wurde durch die Einführung indizierter Typenfamilien (abhängige Typen) zur Darstellung der Prädikate der Prädikatenlogik ermöglicht. Auf diese Weise können alle logischen Verknüpfungen und Quantifizierer von Typbildnern interpretiert werden. In der intuitionistischen Typentheorie werden weitere Typen hinzugefügt, wie beispielsweise eine Art natürlicher Zahlen, eine Art kleiner Typen (ein Universum) und eine Art fundierter Bäume. Die resultierende Theorie enthält eine intuitionistische Zahlentheorie (Heyting-Arithmetik) und vieles mehr.

Die Theorie wird in natürlicher Ableitung formuliert, wobei die Regeln für jeden ersteren Typ als Formations-, Einführungs-, Eliminierungs- und Gleichheitsregeln klassifiziert werden. Diese Regeln weisen gewisse Symmetrien zwischen den Einführungs- und Eliminierungsregeln auf, nachdem Gentzen und Prawitz die natürliche Deduktion behandelt haben, wie im Eintrag über die beweistheoretische Semantik erläutert.

Die Elemente von Sätzen werden, wenn sie als Typen interpretiert werden, Beweisobjekte genannt. Wenn dem natürlichen Deduktionskalkül Beweisobjekte hinzugefügt werden, wird es zu einem typisierten Lambda-Kalkül mit abhängigen Typen, das den ursprünglichen typisierten Lambda-Kalkül der Kirche erweitert. Die Gleichheitsregeln sind Berechnungsregeln für die Begriffe dieses Kalküls. Jede in der Theorie definierbare Funktion ist vollständig und berechenbar. Die intuitionistische Typentheorie ist somit eine typisierte funktionale Programmiersprache mit der ungewöhnlichen Eigenschaft, dass alle Programme enden.

Die intuitionistische Typentheorie ist nicht nur ein formales logisches System, sondern bietet auch einen umfassenden philosophischen Rahmen für den Intuitionismus. Es ist eine interpretierte Sprache, in der die Unterscheidung zwischen der Demonstration eines Urteils und dem Beweis eines Satzes eine grundlegende Rolle spielt (Sundholm 2012). Der Rahmen verdeutlicht die Brouwer-Heyting-Kolmogorov-Interpretation der intuitionistischen Logik und erweitert sie auf die allgemeinere Einstellung der intuitionistischen Typentheorie. Dabei liefert es eine allgemeine Vorstellung nicht nur davon, was ein konstruktiver Beweis ist, sondern auch davon, was ein konstruktives mathematisches Objekt ist. Die Bedeutung der Urteile der intuitionistischen Typentheorie wird anhand von Berechnungen der kanonischen Formen von Typen und Begriffen erklärt. Diese informellen,intuitive Bedeutungserklärungen sind „vormathematisch“und sollten formalen mathematischen Modellen gegenübergestellt werden, die in einem mathematischen Standardrahmen wie der Mengenlehre entwickelt wurden.

Diese Bedeutungstheorie rechtfertigt auch eine Vielzahl von induktiven, rekursiven und induktiv-rekursiven Definitionen. Obwohl beweistheoretisch starke Begriffe wie Analoga bestimmter großer Kardinäle gerechtfertigt werden können, wird das System als prädikativ angesehen. Impredikative Definitionen, wie sie in der Logik höherer Ordnung, der intuitionistischen Mengenlehre und der Topos-Theorie zu finden sind, sind nicht Teil der Theorie. Markovs Prinzip ist es auch nicht, und daher unterscheidet sich die Theorie vom russischen Konstruktivismus.

Ein alternatives formales logisches System für die prädikative konstruktive Mathematik ist die konstruktive Zermelo-Fraenkel-Mengenlehre (CZF) von Myhill und Aczel. Diese Theorie, die auf intuitionistischer Prädikatenlogik erster Ordnung basiert und einige der Axiome der klassischen Zermelo-Fraenkel-Mengenlehre schwächt, hat eine natürliche Interpretation in der intuitionistischen Typentheorie. Die Bedeutungserklärungen von Martin-Löf bilden somit auch indirekt eine Grundlage für CZF.

Varianten der intuitionistischen Typentheorie liegen mehreren weit verbreiteten Beweisassistenten zugrunde, darunter NuPRL, Coq und Agda. Diese Beweisassistenten sind Computersysteme, die zur Formalisierung großer und komplexer Beweise mathematischer Theoreme verwendet wurden, wie beispielsweise der Vierfarbensatz in der Graphentheorie und der Feit-Thompson-Satz in der Theorie endlicher Gruppen. Sie wurden auch verwendet, um die Richtigkeit eines realistischen C-Compilers (Leroy 2009) und anderer Computersoftware zu beweisen.

Philosophisch und praktisch ist die intuitionistische Typentheorie ein grundlegender Rahmen, in dem konstruktive Mathematik und Computerprogrammierung im tiefen Sinne gleich sind. Dieser Punkt wurde von (Gonthier 2008) in dem Artikel hervorgehoben, in dem er seinen Beweis des Vierfarbensatzes beschreibt:

Der Ansatz, der sich für diesen Beweis als erfolgreich erwies, bestand darin, fast jedes mathematische Konzept in eine Datenstruktur oder ein Programm im Coq-System umzuwandeln und so das gesamte Unternehmen in ein Programm zur Programmüberprüfung umzuwandeln.

2. Sätze als Typen

2.1 Intuitionistische Typentheorie: Eine neue Sichtweise auf Logik?

Die intuitionistische Typentheorie bietet eine neue Möglichkeit zur Analyse der Logik, hauptsächlich durch die Einführung expliziter Beweisobjekte. Dies bietet eine direkte rechnerische Interpretation der Logik, da es Berechnungsregeln für Beweisobjekte gibt. In Bezug auf die Ausdruckskraft kann die Theorie des intuitionistischen Typs als Erweiterung der Logik erster Ordnung betrachtet werden, ähnlich wie die Logik höherer Ordnung, aber prädikativ.

2.1.1 Eine Typentheorie

Russell entwickelte die Typentheorie als Reaktion auf seine Entdeckung eines Paradoxons in der naiven Mengenlehre. In seiner verzweigten Typentheorie werden mathematische Objekte nach ihren Typen klassifiziert: der Art der Sätze, der Art der Objekte, der Art der Eigenschaften von Objekten usw. Als Church seine einfache Typentheorie auf der Grundlage einer typisierten Version von ihm entwickelte Lambda-Kalkül fügte er die Regel hinzu, dass es eine Art von Funktionen zwischen zwei beliebigen Arten der Theorie gibt. Die intuitionistische Typentheorie erweitert den einfach typisierten Lambda-Kalkül weiter um abhängige Typen, dh indizierte Typenfamilien. Ein Beispiel ist die Familie der Typen von (n) - Tupeln, die durch (n) indiziert sind.

Typen sind seit langem in der Programmierung weit verbreitet. Frühe Programmiersprachen auf hoher Ebene führten Arten von ganzen Zahlen und Gleitkommazahlen ein. Moderne Programmiersprachen haben oft Rich-Type-Systeme mit vielen Konstrukten zur Bildung neuer Typen. Die intuitionistische Typentheorie ist eine funktionale Programmiersprache, in der das Typensystem so umfangreich ist, dass praktisch jede denkbare Eigenschaft eines Programms als Typ ausgedrückt werden kann. Typen können somit als Spezifikationen für die Aufgabe eines Programms verwendet werden.

2.1.2 Eine intuitionistische Logik mit Beweisobjekten

Brouwers Analyse der Logik führte ihn zu einer intuitionistischen Logik, die das Gesetz der ausgeschlossenen Mitte und das Gesetz der doppelten Negation ablehnt. Diese Gesetze sind in der intuitionistischen Typentheorie nicht gültig. Es enthält also keine klassische (Peano) Arithmetik, sondern nur eine intuitionistische (Heyting) Arithmetik. (Es ist eine andere Sache, dass die Peano-Arithmetik in der Heyting-Arithmetik durch die Interpretation der doppelten Negation interpretiert werden kann, siehe den Eintrag zur intuitionistischen Logik.)

Betrachten Sie einen Satz der intuitionistischen Arithmetik wie den Teilungssatz

) forall m, n. m> 0 \ supset \ existiert q, r. mq + r = n \ Keil m> r)

Ein formaler Beweis (im üblichen Sinne) dieses Satzes ist eine Folge (oder ein Baum) von Formeln, wobei die letzte (Wurzel-) Formel der Satz ist und jede Formel in der Folge entweder ein Axiom (ein Blatt) oder das Ergebnis von ist Anwenden einer Inferenzregel auf einige frühere (höhere) Formeln.

Wenn der Teilungssatz in der intuitionistischen Typentheorie bewiesen ist, bauen wir nicht nur einen formalen Beweis im üblichen Sinne auf, sondern auch eine Konstruktion (oder ein Beweisobjekt) „(divi)“, die die Wahrheit des Satzes bezeugt. Wir schreiben

) divi: \ forall m, n {:} N. \, m> 0 \ supset \ existiert q, r {:} N. \, mq + r = n \ Keil m> r)

um auszudrücken, dass (divi) ein Beweisobjekt für den Divisionssatz ist, dh ein Element des Typs, der den Divisionssatz darstellt. Wenn Sätze als Typen dargestellt werden, wird der (forall) - Quantifizierer mit dem abhängigen Funktionsraumbildner (oder dem allgemeinen kartesischen Produkt) (Pi) identifiziert, der (existiert) - Quantifizierer mit den abhängigen Paaren Typbildner (oder allgemeine disjunkte Summe) (Sigma), Konjunktion (Keil) mit kartesischem Produkt (times), Identitätsbeziehung = mit dem Typbildner (I) von Beweisobjekten von Identitäten und die größer als Beziehung (>) mit dem Typ früher (GT) von Beweisobjekten von größer als Aussagen. Mit „Typennotation“schreiben wir also

) divi: \ Pi m, n {:} N. \, \ GT (m, 0) rechter Pfeil \ Sigma q, r {:} N. \, \ I (N, mq + r, n) times \ GT (m, r))

um auszudrücken, dass das Beweisobjekt "(divi)" eine Funktion ist, die zwei Zahlen (m) und (n) und ein Beweisobjekt (p) abbildet, das bezeugt, dass (m> 0)) zu einem Vierfachen ((q, (r, (s, t)))), wobei (q) der Quotient und (r) der Rest ist, der erhalten wird, wenn (n) durch \ dividiert wird (m). Die dritte Komponente (s) ist ein Beweisobjekt, das die Tatsache bezeugt, dass (mq + r = n) und die vierte Komponente (t) ein Beweisobjekt ist, das (m> r) bezeugt.

Entscheidend ist, dass (divi) nicht nur eine Funktion im klassischen Sinne ist; es ist auch eine Funktion im intuitionistischen Sinne, dh ein Programm, das die Ausgabe ((q, (r, (s, t)))) berechnet, wenn (m), (n) gegeben wird, (p) als Eingaben. Dieses Programm ist ein Begriff in einem Lambda-Kalkül mit speziellen Konstanten, dh ein Programm in einer funktionalen Programmiersprache.

2.1.3 Eine Erweiterung der Prädikatenlogik erster Ordnung

Die Theorie des intuitionistischen Typs kann als Erweiterung der Logik erster Ordnung betrachtet werden, ebenso wie die Logik höherer Ordnung eine Erweiterung der Logik erster Ordnung ist. In der Logik höherer Ordnung finden wir einige einzelne Domänen, die als beliebige Mengen interpretiert werden können. Wenn die Signatur relationale Konstanten enthält, können diese als Beziehungen zwischen den Mengen interpretiert werden, die die einzelnen Domänen interpretieren. Darüber hinaus können wir über Beziehungen und über Beziehungen von Beziehungen usw. quantifizieren. Wir können uns Logik höherer Ordnung als Logik erster Ordnung vorstellen, die mit einer Möglichkeit ausgestattet ist, neue Bereiche der Quantifizierung einzuführen: if (S_1, \ ldots, S_n) sind Domänen der Quantifizierung, dann ist ((S_1, \ ldots, S_n)) eine neue Domäne der Quantifizierung, die aus allen n-fachen Beziehungen zwischen den Domänen (S_1, \ ldots, S_n) besteht. Logik höherer Ordnung hat eine einfache satztheoretische Interpretation, wobei ((S_1, \ ldots, S_n)) als Potenzmenge (P (A_1 \ times \ cdots \ times A_n)) interpretiert wird, wobei (A_i) ist die Interpretation von (S_i) für (i = 1, \ ldots, n). Dies ist die Art von Logik höherer Ordnung oder einfacher Typentheorie, die Ramsey, Church und andere eingeführt haben.

Die intuitionistische Typentheorie kann auf ähnliche Weise betrachtet werden, nur hier sind die Möglichkeiten zur Einführung von Quantifizierungsbereichen reicher, man kann (Sigma, \ Pi, +, \ I) verwenden, um neue aus alten zu konstruieren. (Abschnitt 3.1; Martin-Löf 1998 [1972]). Die intuitionistische Typentheorie hat auch eine einfache satztheoretische Interpretation, wobei (Sigma), (Pi) usw. als die entsprechenden satztheoretischen Konstruktionen interpretiert werden; siehe unten. Wir können der intuitionistischen Typentheorie nicht spezifizierte einzelne Domänen wie in HOL hinzufügen. Diese werden wie für HOL als Mengen interpretiert. Jetzt zeigen wir einen Unterschied zu HOL: In der intuitionistischen Typentheorie können wir nicht spezifizierte Familiensymbole einführen. Wir können (T) als eine Familie von Typen über die einzelne Domäne (S) einführen:

[T (x); { rm type}; (x {:} S).)

Wenn (S) als (A) interpretiert wird, kann (T) als jede durch (A) indizierte Familie von Mengen interpretiert werden. Als nicht-mathematisches Beispiel können wir die binäre Beziehung zwischen Mitgliedern einer einzelnen Domäne von Menschen wie folgt rendern. Stellen Sie die binäre Familie Loves over the domain People vor

[{ rm Loves} (x, y); { rm type}; (x {:} { rm People}, y {:} { rm People}).)

Die Interpretation kann eine beliebige Familie von Mengen (B_ {x, y}) ((x {:} A), (y {:} A)) sein. Wie deckt dies den Standardbegriff der Beziehung ab? Angenommen, wir haben eine binäre Beziehung (R) zu (A) im bekannten satztheoretischen Sinne. Wir können eine entsprechende binäre Familie wie folgt erstellen

[B_ {x, y} = \ begin {Fälle} {0 } & \ text {if} R (x, y) text {enthält} \ \ varnothing & \ text {if} R (x, y) text {ist falsch.} end {case})

Nun ist (B_ {x, y}) genau dann nicht leer, wenn (R (x, y)) gilt. (Wir hätten jedes andere Element aus unserem satztheoretischen Universum als 0 auswählen können, um die Wahrheit anzuzeigen.) Somit können wir aus jeder Beziehung eine Familie konstruieren, deren Wahrheit von (x, y) (B_ {x, y}) entspricht.) nicht leer sein. Beachten Sie, dass es dieser Interpretation egal ist, was der Beweis für (R (x, y)) ist, nur dass er gilt. Denken Sie daran, dass die intuitionistische Typentheorie Sätze als Typen interpretiert, also bedeutet (p {:} { rm Loves} ({ rm John}, { rm Mary})), dass ({ rm Loves} ({ rm John}, { rm Mary})) ist wahr.

Die Interpretation von Beziehungen als Familien ermöglicht es, Beweise oder Beweise zu verfolgen, die (R (x, y)) enthält, aber wir können uns auch dafür entscheiden, sie zu ignorieren.

In der Montague-Semantik wird eine Logik höherer Ordnung verwendet, um die Semantik der natürlichen Sprache (und Beispiele wie oben) anzugeben. Ranta (1994) führte die Idee ein, stattdessen die intuitionistische Typentheorie zu verwenden, um die Satzstruktur mit Hilfe abhängiger Typen besser zu erfassen.

Wie würde dagegen die mathematische Beziehung (>) zwischen natürlichen Zahlen in der intuitionistischen Typentheorie behandelt? Zunächst benötigen wir eine Art von Zahlen (N). Wir könnten im Prinzip eine nicht spezifizierte individuelle Domäne (N) einführen und dann Axiome hinzufügen, genau wie wir es in der Logik erster Ordnung tun, wenn wir das Axiomensystem für die Peano-Arithmetik einrichten. Dies würde uns jedoch nicht die wünschenswerte rechnerische Interpretation geben. Wie unten erläutert, legen wir Einführungsregeln für die Konstruktion neuer natürlicher Zahlen in (N) sowie Eliminierungs- und Berechnungsregeln für die Definition von Funktionen auf (N) (durch Rekursion) fest. Die Standardbestellungsbeziehung (>) sollte erfüllen

) mbox {(x> y) falls vorhanden (z {:} N), so dass (y + z + 1 = x)}.)

Die rechte Hand wird in der intuitionistischen Typentheorie als (Sigma z {:} N. \, \ I (N, y + z + 1, x)) dargestellt, und wir nehmen dies als Definition der Beziehung (>). ((+) wird durch rekursive Gleichungen definiert, (I) ist die Konstruktion des Identitätstyps). Nun werden alle Eigenschaften von (>) durch die erwähnten Einführungs- und Eliminierungs- und Berechnungsregeln für (N) bestimmt.

2.1.4 Eine Logik mit verschiedenen Urteilsformen

Das Typensystem der intuitionistischen Typentheorie ist sehr ausdrucksstark. Infolgedessen ist die Form eines Typs nicht mehr nur eine Frage des Parsens, sondern muss bewiesen werden. Die Form eines Typs ist eine Form der Beurteilung der intuitionistischen Typentheorie. Die Typizität eines Begriffs in Bezug auf einen Typ ist eine andere. Darüber hinaus gibt es Gleichstellungsurteile für Typen und Begriffe. Dies ist eine weitere Art und Weise, in der sich die intuitionistische Typentheorie von der gewöhnlichen Logik erster Ordnung unterscheidet, indem sie sich auf das alleinige Urteil konzentriert, das die Wahrheit eines Satzes ausdrückt.

2.1.5 Semantik

Während eine Standarddarstellung der Logik erster Ordnung Tarski bei der Definition des Begriffs des Modells folgen würde, folgt die intuitionistische Typentheorie der Tradition der Brouwerschen Bedeutungstheorie, wie sie von Heyting und Kolmogorov weiterentwickelt wurde, der sogenannten BHK-Interpretation der Logik. Der entscheidende Punkt ist, dass der Beweis einer Implikation (A \ supset B) eine Methode ist, die einen Beweis von (A) in einen Beweis von (B) umwandelt. In der intuitionistischen Typentheorie wird diese Methode formal durch das Programm (f {:} A \ supset B) oder (f {:} A \ rightarrow B) dargestellt: die Art der Beweise einer Implikation (A \ supset) B) ist die Art von Funktionen, die Beweise von (A) Beweisen von (B) zuordnen.

Während die Tarski-Semantik normalerweise metamathematisch dargestellt wird und die Mengenlehre voraussetzt, sollte Martin-Löfs Bedeutungstheorie der intuitionistischen Typentheorie direkt und „vormathematisch“verstanden werden, dh ohne eine Metasprache wie die Mengenlehre anzunehmen.

2.1.6 Eine funktionale Programmiersprache

Leser mit einem Hintergrund in der Lambda-Rechnung und der funktionalen Programmierung können eine alternative erste Annäherung an die intuitionistische Typentheorie erhalten, indem sie sie als typisierte funktionale Programmiersprache im Stil von Haskell oder einem der Dialekte von ML betrachten. Es unterscheidet sich jedoch von diesen in zwei entscheidenden Aspekten: (i) es hat abhängige Typen (siehe unten) und (ii) alle typisierbaren Programme werden beendet. (Beachten Sie, dass die intuitionistische Typentheorie die jüngsten Erweiterungen von Haskell mit verallgemeinerten algebraischen Datentypen beeinflusst hat, die manchmal eine ähnliche Rolle spielen können wie induktiv definierte abhängige Typen.)

2.2 Die Curry-Howard-Korrespondenz

Wie bereits erwähnt, ist das Prinzip, dass

Ein Satz ist die Art seiner Beweise.

ist grundlegend für die intuitionistische Typentheorie. Dieses Prinzip wird auch als Curry-Howard-Korrespondenz oder sogar als Curry-Howard-Isomorphismus bezeichnet. Curry entdeckte eine Entsprechung zwischen dem impliziten Fragment der intuitionistischen Logik und dem einfach typisierten Lambda-Kalkül. Howard erweiterte diese Entsprechung auf Prädikatenlogik erster Ordnung. In der intuitionistischen Typentheorie wird diese Entsprechung zu einer Identifikation von Sätzen und Typen, die um die Quantifizierung über höhere Typen und mehr erweitert wurde.

2.3 Sätze von Beweisobjekten

Wie sind diese Beweisobjekte? Sie sollten nicht als logische Ableitungen betrachtet werden, sondern als (strukturierte) symbolische Beweise dafür, dass etwas wahr ist. Ein anderer Begriff für solche Beweise ist "Wahrheitsmacher".

Es ist als etwas grobe erste Annäherung lehrreich, Typen durch gewöhnliche Mengen in dieser Entsprechung zu ersetzen. Definieren Sie eine Menge (E_ {m, n}) in Abhängigkeit von (m, n \ in {{ mathbb N}}) durch:

) E_ {m, n} = \ left { begin {array} {ll} {0 } & \ mbox {if (m = n)} \ \ varnothing & \ mbox {if (m \ ne n).} end {array} right.)

Dann ist (E_ {m, n}) genau dann nicht leer, wenn (m = n). Die Menge (E_ {m, n}) entspricht dem Satz (m = n), und die Zahl (0) ist ein Beweisobjekt (Wahrheitsmacher), das die Mengen (E_) bewohnt. {m, m}).

Betrachten Sie den Satz, dass (m) eine gerade Zahl ist, ausgedrückt als Formel (existiert n \ in {{ mathbb N}}. M = 2n). Wir können eine Menge von Beweisobjekten erstellen, die dieser Formel entsprechen, indem wir die allgemeine satztheoretische Summenoperation verwenden. Angenommen, (A_n) ((n \ in {{ mathbb N}})) ist eine Familie von Mengen. Dann ist seine disjunkte Summe durch die Menge der Paare gegeben

[(Sigma n \ in {{ mathbb N}}) A_n = {(n, a): n \ in {{ mathbb N}}, a \ in A_n }.)

Wenn wir diese Konstruktion auf die Familie (A_n = \ E_ {m, 2n}) anwenden, sehen wir, dass ((Sigma n \ in {{ mathbb N}}) E_ {m, 2n}) ist nicht leer genau dann, wenn es ein (n \ in {{ mathbb N}}) mit (m = 2n) gibt. Mit der allgemeinen satztheoretischen Produktoperation ((Pi n \ in {{ mathbb N}}) A_n) können wir auf ähnliche Weise eine Menge erhalten, die einem universell quantifizierten Satz entspricht.

2.4 Abhängige Typen

In der intuitionistischen Typentheorie gibt es primitive Typbildner (Sigma) und (Pi) für allgemeine Summen und Produkte und (I) für Identitätstypen, analog zu den oben beschriebenen satztheoretischen Konstruktionen. Der Identitätstyp (I (N, m, n)), der der Menge (E_ {m, n}) entspricht, ist ein Beispiel für einen abhängigen Typ, da er von (m) und \ abhängt (n). Es wird auch als indizierte Typenfamilie bezeichnet, da es sich um eine durch (m) und (n) indizierte Typenfamilie handelt. In ähnlicher Weise können wir die allgemeine disjunkte Summe (Sigma x {:} A. \, B) und das allgemeine kartesische Produkt (Pi x {:} A. \, B) einer solchen Familie von Typen bilden (B) indiziert durch (x {:} A), entsprechend der oben festgelegten theoretischen Summe und den Produktoperationen.

Abhängige Typen können auch durch primitive Rekursion definiert werden. Ein Beispiel ist der Typ von (n) - Tupeln (A ^ n) von Elementen vom Typ (A) und indiziert durch (n {:} N), definiert durch die Gleichungen

) begin {align *} A ^ 0 & = 1 \\ A ^ {n + 1} & = A \ times A ^ n \ end {align *})

Dabei ist (1) ein Ein-Element-Typ und (times) das kartesische Produkt zweier Typen. Wir stellen fest, dass abhängige Typen die Berechnung in Typen einführen: Die obigen Definitionsregeln sind Berechnungsregeln. Zum Beispiel ist das Ergebnis der Berechnung von (A ^ 3) (A \ mal (A \ mal (A \ mal 1))).

2.5 Sätze als Typen in der intuitionistischen Typentheorie

Mit Aussagen als Typen werden Prädikate zu abhängigen Typen. Zum Beispiel wird das Prädikat (mathrm {Prime} (x)) zur Art der Beweise, dass (x) eine Primzahl ist. Dieser Typ hängt von (x) ab. In ähnlicher Weise ist (x <y) die Art von Beweisen, dass (x) kleiner als (y) ist.

Nach der Curry-Howard-Interpretation von Sätzen als Typen werden die logischen Konstanten als Typbildner interpretiert:

) begin {align *} bot & = \ varnothing \\ \ top & = 1 \\ A \ vee B & = A + B \\ A \ Keil B & = A \ mal B \\ A \ supset B. & = A \ rightarrow B \\ \ existiert x {:} A. \, B & = \ Sigma x {:} A. \, B \\ \ forall x {:} A. \, B & = \ Pi x {:} A. \, B \ end {align *})

Dabei ist (Sigma x {:} A. \, B) die disjunkte Summe der (A) - indizierten Familie von Typen (B) und (Pi x {:} A. \, B) ist sein kartesisches Produkt. Die kanonischen Elemente von (Sigma x {:} A. \, B) sind Paare ((a, b)), so dass (a {:} A) und (b {:} B [x: = a]) (der Typ, der durch Ersetzen aller freien Vorkommen von (x) in (B) durch (a) erhalten wird). Die Elemente von (Pi x {:} A. \, B) sind (berechenbare) Funktionen (f), so dass (f \, a {:} B [x: = a]), wann immer (a {:} A).

Betrachten Sie zum Beispiel den Satz

) begin {Gleichung} forall m {:} N. \, \ existiert n {:} N. \, m \ lt n \ wedge \ mathrm {Prime} (n) tag {1} label {prop1} end {Gleichung})

zum Ausdruck bringen, dass es beliebig große Primzahlen gibt. Unter der Curry-Howard-Interpretation wird dies zum Typ (Pi m {:} N. \, \ Sigma n {:} N. \, m \ lt n \ times \ mathrm {Prime} (n)) von Funktionen, die eine Zahl (m) einem Tripel ((n, (p, q))) zuordnen, wobei (n) eine Zahl ist, ist (p) ein Beweis dafür, dass (m \ lt n) und (q) ist ein Beweis dafür, dass (n) Primzahl ist. Dies ist das Prinzip der Beweise als Programme: Ein konstruktiver Beweis, dass es beliebig große Primzahlen gibt, wird zu einem Programm, das bei einer beliebigen Anzahl eine größere Primzahl zusammen mit Beweisen, dass es tatsächlich größer und tatsächlich Primzahl ist, erzeugt.

Beachten Sie, dass der Beweis, der einen Widerspruch aus der Annahme ableitet, dass es eine größte Primzahl gibt, nicht konstruktiv ist, da er nicht explizit die Möglichkeit bietet, eine noch größere Primzahl zu berechnen. Um diesen Beweis in einen konstruktiven zu verwandeln, müssen wir explizit zeigen, wie man die größere Primzahl konstruiert. (Da der obige Satz (ref {prop1}) eine (Pi ^ 0_2) - Formel ist, können wir beispielsweise Friedmans A-Übersetzung verwenden, um einen solchen Beweis in der klassischen Arithmetik in einen Beweis in der intuitionistischen Arithmetik und damit in einen zu verwandeln Beweis in der intuitionistischen Typentheorie.)

3. Grundlegende intuitionistische Typentheorie

Wir präsentieren nun eine Kernversion der intuitionistischen Typentheorie, die eng mit der ersten Version der Theorie verwandt ist, die Martin-Löf 1972 vorstellte (Martin-Löf 1998 [1972]). Zusätzlich zu den Typbildnern, die für die Curry-Howard-Interpretation der oben aufgeführten typisierten intuitionistischen Prädikatenlogik benötigt werden, gibt es zwei Typen: den Typ (N) natürlicher Zahlen und den Typ (U) kleiner Typen.

Es kann gezeigt werden, dass die resultierende Theorie die intuitionistische Zahlentheorie (HA) (Heyting-Arithmetik), Gödels System (T) primitiver rekursiver Funktionen höheren Typs und die Theorie (HA ^ \ omega) enthält. der Heyting-Arithmetik höheren Typs.

Diese intuitionistische Kerntheorie ist nicht nur die ursprüngliche, sondern vielleicht auch die minimale Version, die die wesentlichen Merkmale der Theorie aufweist. Spätere Erweiterungen mit primitiven Identitätstypen, fundierten Baumtypen, Universumshierarchien und allgemeinen Vorstellungen von induktiven und induktiv-rekursiven Definitionen haben die beweistheoretische Stärke der Theorie erhöht und sie auch für die Programmierung und Formalisierung der Mathematik bequemer gemacht. Zum Beispiel können wir durch Hinzufügen von fundierten Bäumen die konstruktive Zermelo-Fraenkel-Mengenlehre (CZF) von Aczel (1978 [1977]) interpretieren. Wir werden jedoch bis zum nächsten Abschnitt warten, um diese Erweiterungen zu beschreiben.

3.1 Urteile

In Martin-Löf (1996) wird eine allgemeine Logikphilosophie vorgestellt, in der der traditionelle Begriff des Urteils erweitert und eine zentrale Position eingenommen wird. Ein Urteil ist nicht länger nur eine Bestätigung oder Ablehnung eines Satzes, sondern ein allgemeiner Akt des Wissens. Wenn wir mathematisch argumentieren, urteilen wir über mathematische Objekte. Eine Form der Beurteilung besteht darin, festzustellen, dass eine mathematische Aussage wahr ist. Eine andere Form der Beurteilung besteht darin, festzustellen, dass etwas ein mathematisches Objekt ist, beispielsweise eine Menge. Die logischen Regeln geben Methoden an, um aus früheren Urteilen korrekte Urteile zu ziehen. Die durch solche Regeln erlangten Urteile können in Baumform dargestellt werden

) infer [r_4] {J_8} { infer [r_1] {J_3} {J_1 & J_2} & \ infer [r_3] {J_7} { infer [r_5] {J_5} {J_4} & J_6}}]]

oder in sequentieller Form

• (1) (J_1 \ quad \ text {axiom})
• (2) (J_2 \ quad \ text {axiom})
• (3) (J_3 \ quad \ text {nach Regel (r_1) aus (1) und (2)})
• (4) (J_4 \ quad \ text {axiom})
• (5) (J_5 \ quad \ text {nach Regel (r_2) aus (4)})
• (6) (J_6 \ quad \ text {axiom})
• (7) (J_7 \ quad \ text {nach Regel (r_3) aus (5) und (6)})
• (8) (J_8 \ quad \ text {nach Regel (r_4) aus (3) und (7)})

Die letztere Form ist in mathematischen Argumenten üblich. Eine solche Folge oder ein solcher Baum, der durch logische Regeln aus Axiomen gebildet wird, ist eine Ableitung oder Demonstration eines Urteils.

Argumente erster Ordnung können mit einer einzigen Art von Urteil präsentiert werden:

Der Satz (B) ist wahr unter der Hypothese, dass die Sätze (A_1, \ ldots, A_n) alle wahr sind.

Wir schreiben dieses hypothetische Urteil als sogenannte Gentzen-Sequenz

[A_1, \ ldots, A_n { vdash} B.)

Beachten Sie, dass dies ein einzelnes Urteil ist, das nicht mit der Ableitung des Urteils ({ vdash} B) aus den Urteilen ({ vdash} A_1, \ ldots, { vdash} A_n) verwechselt werden sollte. Wenn (n = 0), dann besagt das kategoriale Urteil ({ vdash} B), dass (B) ohne Annahmen wahr ist. Mit der sequentiellen Notation wird die bekannte Regel für die konjunktive Einführung

) infer [(land I)] {A_1, \ ldots, A_n { vdash} B \ land C} {A_1, \ ldots, A_n { vdash} B & A_1, \ ldots, A_n { vdash} C}.)

3.2 Urteilsformulare

Die Martin-Löf-Typentheorie hat vier Grundformen von Urteilen und ist ein wesentlich komplizierteres System als die Logik erster Ordnung. Ein Grund ist, dass aufgrund der Identifizierung von Aussagen und Typen mehr Informationen in den Ableitungen herumgetragen werden. Ein weiterer Grund ist, dass die Syntax stärker involviert ist. Zum Beispiel müssen die wohlgeformten Formeln (Typen) gleichzeitig mit den nachweislich wahren Formeln (bewohnten Typen) erzeugt werden.

Die vier Formen der kategorialen Beurteilung sind

• (vdash A \; { rm type}), was bedeutet, dass (A) ein wohlgeformter Typ ist,
• (vdash a {:} A), was bedeutet, dass (a) den Typ (A) hat,
• (vdash A = A '), was bedeutet, dass (A) und (A') gleiche Typen sind,
• (vdash a = a '{:} A), was bedeutet, dass (a) und (a') gleiche Elemente vom Typ (A) sind.

Im Allgemeinen ist ein Urteil hypothetisch, das heißt, es wird in einem Kontext (Gamma) getroffen, dh in einer Liste (x_1 {:} A_1, \ ldots, x_n {:} A_n) von Variablen, die können im Urteil zusammen mit ihren jeweiligen Typen frei auftreten. Beachten Sie, dass die Typen in einem Kontext von Variablen früherer Typen abhängen können. Zum Beispiel kann (A_n) von (x_1 {:} A_1, \ ldots, x_ {n-1} {:} A_ {n-1}) abhängen. Die vier Formen hypothetischer Urteile sind

• (Gamma \ vdash A \; { rm type}), was bedeutet, dass (A) im Kontext (Gamma) ein wohlgeformter Typ ist,
• (Gamma \ vdash a {:} A), was bedeutet, dass (a) im Kontext (Gamma) den Typ (A) hat.
• (Gamma \ vdash A = A '), was bedeutet, dass (A) und (A') im Kontext (Gamma) gleiche Typen sind,
• (Gamma \ vdash a = a '{:} A), was bedeutet, dass (a) und (a') gleiche Elemente vom Typ (A) im Kontext (Gamma) sind..

Unter dem Satz als Typeninterpretation

) tag {2} label {analytic} vdash a {:} A)

kann als das Urteil verstanden werden, dass (a) ein Beweisobjekt für den Satz (A) ist. Wenn wir dieses Objekt unterdrücken, erhalten wir ein Urteil, das dem in der gewöhnlichen Logik erster Ordnung entspricht (siehe oben):

) tag {3} label {synthetisch} vdash A \; { rm true}.)

Bemerkung 3.1. Martin-Löf (1994) argumentiert, dass Kants analytisches Urteil a priori und synthetisches Urteil a priori im Bereich der Logik durch ([analytisch]) bzw. ([synthetisch]) veranschaulicht werden können. Im analytischen Urteil ([analytisch]) ist alles explizit, was erforderlich ist, um das Urteil offensichtlich zu machen. Für seine synthetische Version ([synthetisch]) muss eine möglicherweise komplizierte Beweiskonstruktion (a) bereitgestellt werden, um dies offensichtlich zu machen. Dieses Verständnis von Analytizität und Synthetizität hat die überraschende Konsequenz, dass „die logischen Gesetze in ihrer üblichen Formulierung alle synthetisch sind“. Martin-Löf (1994: 95). Seine Analyse ergibt weiter:

"[…] Die Logik analytischer Urteile, dh die Logik zur Ableitung von Urteilen der beiden analytischen Formen, ist vollständig und entscheidbar, während die Logik synthetischer Urteile unvollständig und unentscheidbar ist, wie Gödel gezeigt hat." Martin-Löf (1994: 97).

Die Entscheidbarkeit der beiden analytischen Urteile ((vdash a {:} A) und (vdash a = b {:} A)) hängt von den metamathematischen Eigenschaften der Typentheorie ab: starke Normalisierung und entscheidbare Typprüfung.

Manchmal werden auch die folgenden Formen ausdrücklich als Urteile der Theorie angesehen:

• (Gamma \; { rm context}), was bedeutet, dass (Gamma) ein wohlgeformter Kontext ist.
• (Gamma = \ Gamma '), was bedeutet, dass (Gamma) und (Gamma') gleiche Kontexte sind.

Im Folgenden werden wir das Urteil (Gamma \ vdash A \; { rm type}) als (Gamma \ vdash A) und (Gamma \; { rm context}) als (abkürzen) Gamma \ vdash.)

3.3 Inferenzregeln

Wenn wir die Regeln angeben, verwenden wir den Buchstaben (Gamma) als Metavariable, die sich über Kontexte erstreckt, (A, B, \ ldots) als Metavariablen, die sich über Typen erstrecken, und (a, b, c, d, e, f, \ ldots) als Metavariablen, die sich über Begriffe erstrecken.

Die erste Gruppe von Inferenzregeln sind allgemeine Regeln, einschließlich Regeln für Annahme, Substitution und Kontextbildung. Es gibt auch Regeln, die ausdrücken, dass Gleichheiten Äquivalenzbeziehungen sind. Es gibt zahlreiche solcher Regeln, und wir zeigen nur die besonders wichtige Regel der Typengleichheit, die für die Berechnung in Typen entscheidend ist:

) frac { Gamma \ vdash a {:} A \ hspace {2em} Gamma \ vdash A = B} { Gamma \ vdash a {:} B})

Die übrigen Regeln gelten nur für die Typbildner. Diese werden als Regeln für Bildung, Einführung, Beseitigung und Gleichstellung klassifiziert.

3.4 Intuitionistische Prädikatenlogik

Wir geben nur die Regeln für (Pi) an. Es gibt analoge Regeln für die anderen Typbildner, die den logischen Konstanten der typisierten Prädikatenlogik entsprechen.

Im Folgenden bedeutet (B [x: = a]) den Begriff, der durch Ersetzen des Ausdrucks (a) für jedes freie Auftreten der Variablen (x) in (B) erhalten wird (Vermeidung der Variablenerfassung).

(Pi) - Bildung.) frac { Gamma \ vdash A \ hspace {2em} Gamma, x {:} A \ vdash B} { Gamma \ vdash \ Pi x {:} A. B}) (Pi) -Einführung.) frac { Gamma, x {:} A \ vdash b {:} B} { Gamma \ vdash \ lambda x. b {:} Pi x {:} A. B}) (Pi) - Eliminierung.) frac { Gamma \ vdash f {:} Pi x {:} AB \ hspace {2em} Gamma \ vdash a {:} A} { Gamma \ vdash f \, a {:} B [x: = a]}) (Pi) - Gleichheit.) frac { Gamma, x {:} A \ vdash b {:} B \ hspace {2em} Gamma \ vdash a {:} A} { Gamma \ vdash (lambda xb), a = b [x: = a] {:} B [x: = a]}) Dies ist die Regel der (beta) - Konvertierung. Wir können auch die Regel der (eta) - Konvertierung hinzufügen:) frac { Gamma \ vdash f {:} Pi x {:} A. B} { Gamma \ vdash \ lambda x. f \, x = f {:} Pi x {:} A. B}.)

Darüber hinaus gibt es Kongruenzregeln, die ausdrücken, dass Operationen, die durch die Regeln für Bildung, Einführung und Beseitigung eingeführt werden, die Gleichheit bewahren. Beispielsweise lautet die Kongruenzregel für (Pi)

) frac { Gamma \ vdash A = A '\ hspace {2em} Gamma, x {:} A \ vdash B = B'} { Gamma \ vdash \ Pi x {:} A. B = \ Pi x {:} A '. B '}.)

3.5 Natürliche Zahlen

Wie in der Peano-Arithmetik werden die natürlichen Zahlen durch 0 und die Nachfolgeoperation (s) erzeugt. Die Eliminierungsregel besagt, dass dies die einzig möglichen Wege sind, eine natürliche Zahl zu erzeugen.

Wir schreiben (f (c) = \ R (c, d, xy.e)) für die Funktion, die durch primitive Rekursion auf die natürliche Zahl (c) mit Basisfall (d) und Schritt definiert ist Funktion (xy.e) (oder alternativ (lambda xy.e)), die den Wert (y) für die vorherige Zahl (x {:} N) dem Wert für (s (x)). Beachten Sie, dass (R) ein neuer Variablenbindungsoperator ist: Die Variablen (x) und (y) werden in (e) gebunden.

(N) - Bildung.) Gamma \ vdash \ N) (N) - Einführung.) Gamma \ vdash 0 {:} N \ hspace {2em} frac { Gamma \ vdash a {:} N} { Gamma \ vdash s (a) {:} N}) (N) - Beseitigung.) frac { Gamma, x {:} N \ vdash C \ hspace {1em} Gamma \ vdash c {:} N \ hspace {1em} Gamma \ vdash d {:} C [x: = 0] hspace {1em} Gamma, y {:} N, z {:} C [x: = y] vdash e {:} C [x: = s (y)]} { Gamma \ vdash \ R (c, d, yz.e) {:} C [x: = c]}) (N) - Gleichheit (unter geeigneten Voraussetzungen).) begin {align *} R (0, d, yz.e) & = d {:} C [x: = 0] \ \ R (s (a), d, yz.e) & = e [y: = a, z: = \ R (a, d, yz.e)] {:} C [x: = s (a)] end {align *})

Die Regel der (N) - Eliminierung drückt gleichzeitig den Typ einer durch primitive Rekursion definierten Funktion und nach der Curry-Howard-Interpretation die Regel der mathematischen Induktion aus: Wir beweisen die Eigenschaft (C) einer natürlichen Zahl (x) durch Induktion auf (x).

Gödels System (T) ist im Wesentlichen eine intuitionistische Typentheorie mit nur den Typbildnern (N) und (A \ rightarrow B) (der Art der Funktionen von (A) bis (B) Dies ist der Sonderfall von ((Pi x {:} A) B), wobei (B) nicht von (x {:} A) abhängt. Da es in System (T) keine abhängigen Typen gibt, können die Regeln vereinfacht werden.

3.6 Das Universum der kleinen Typen

Martin-Löfs erste Version der Typentheorie (Martin-Löf 1971a) hatte ein Axiom, das besagt, dass es einen Typ aller Typen gibt. Dies wurde von Girard als inkonsistent erwiesen, der feststellte, dass das Burali-Forti-Paradoxon in dieser Theorie kodiert werden kann.

Um diese pathologische Impredikativität zu überwinden, aber dennoch einen Teil ihrer Ausdruckskraft zu bewahren, führte Martin-Löf 1972 ein Universum (U) kleiner Typen ein, das unter allen Typbildnern der Theorie geschlossen ist, außer dass es sich nicht selbst enthält (Martin- Löf 1998 [1972]). Die Regeln sind:

(U) - Bildung.) Gamma \ vdash \ U) (U) - Einführung.) Gamma \ vdash \ varnothing {:} U \ hspace {3em} Gamma \ vdash 1 {:} U)) frac { Gamma \ vdash A {:} U \ hspace {2em} Gamma \ vdash B {:} U} { Gamma \ vdash A + B {:} U} hspace {3em} frac { Gamma \ vdash A {:} U \ hspace {2em} Gamma \ vdash B {:} U} { Gamma \ vdash A \ mal B {:} U})) frac { Gamma \ vdash A {:} U \ hspace {2em} Gamma \ vdash B {:} U} { Gamma \ vdash A \ rightarrow B {:} U})) frac { Gamma \ vdash A {:} U \ hspace {2em} Gamma, x {:} A \ vdash B {:} U} { Gamma \ vdash \ Sigma x {:} A. \, B {:} U} hspace {3em} frac { Gamma \ vdash A {:} U. \ hspace {2em} Gamma, x {:} A \ vdash B {:} U} { Gamma \ vdash \ Pi x {:} A. \, B {:} U})) Gamma \ vdash \ N {:} U) (U) - Eliminierung.) frac { Gamma \ vdash A {:} U} { Gamma \ vdash A})

Da (U) ein Typ ist, können wir (N) - Elimination verwenden, um kleine Typen durch primitive Rekursion zu definieren. Wenn beispielsweise (A: \ U), können wir den Typ von (n) - Tupeln von Elementen in (A) wie folgt definieren:

[A ^ n = \ R (n, 1, xy. A \ mal y) {:} U)

Dieses typentheoretische Universum (U) ist analog zu einem Grothendieck-Universum in der Mengenlehre, das eine Menge von Mengen ist, die unter allen Möglichkeiten geschlossen sind, wie Mengen in der Zermelo-Fraenkel-Mengenlehre konstruiert werden können. Die Existenz eines Grothendieck-Universums kann mit den üblichen Axiomen der Zermelo-Fraenkel-Mengenlehre nicht bewiesen werden, sondern benötigt ein neues Axiom.

In Martin-Löf (1975) wird das Universum auf eine zählbare Hierarchie von Universen erweitert

) U_0: \ U_1: \ U_2: \ cdots.)

Auf diese Weise hat jeder Typ einen Typ, nicht nur jeder kleine Typ.

3.7 Aussagenidentität

Oben haben wir das Gleichstellungsurteil eingeführt

) tag {4} label {defeq} Gamma \ vdash a = a '{:} A.)

Dies wird normalerweise als "definitive Gleichheit" bezeichnet, da dies durch Normalisieren der Begriffe (a) und (a ') und Überprüfen der Identität der Normalformen entschieden werden kann. Diese Gleichheit ist jedoch ein Urteil und kein Satz (Typ), und wir können solche Urteilsgleichheiten daher nicht durch Induktion beweisen. Aus diesem Grund müssen wir Aussagenidentitätstypen einführen. Zum Beispiel kann der Identitätstyp für natürliche Zahlen (I (N, m, n)) durch (U) -wertige primitive Rekursion definiert werden. Wir können dann die Peano-Axiome ausdrücken und beweisen. Darüber hinaus kann die Erweiterungsgleichheit von Funktionen definiert werden durch

) I (N \ rechter Pfeil \ N, f, f ') = \ Pi x {:} N. \ I (N, f \, x, f '\, x).)

3.8 Das Axiom der Wahl ist ein Satz

Die folgende Form des Axioms der Wahl ist eine unmittelbare Folge der BHK-Interpretation der intuitionistischen Quantifizierer und lässt sich in der Theorie des intuitionistischen Typs leicht beweisen:

[(Pi x {:} A. \ Sigma y {:} B. C) rightarrow \ Sigma f {:} (Pi x {:} A. B). C [y: = f \, x])

Der Grund ist, dass (Pi x {:} A. \ Sigma y {:} B. C) die Art von Funktionen ist, die Elemente (x {:} A) Paaren ((y, z)) mit (y {:} B) und (z {:} C). Die Auswahlfunktion (f) wird erhalten, indem die erste Komponente (y {:} B) dieses Paares zurückgegeben wird.

Es ist vielleicht überraschend, dass die intuitionistische Typentheorie ein Axiom der Wahl direkt validiert, da dieses Axiom aus konstruktiver Sicht oft als problematisch angesehen wird. Eine mögliche Erklärung für diesen Sachverhalt ist, dass das Obige ein Axiom der Wahl für Typen ist und dass Typen im Allgemeinen keine angemessenen konstruktiven Approximationen von Mengen im klassischen Sinne sind. Zum Beispiel können wir eine reelle Zahl als Cauchy-Sequenz in der intuitionistischen Typentheorie darstellen, aber die Menge der reellen Zahlen ist nicht der Typ der Cauchy-Sequenzen, sondern der Typ der Cauchy-Sequenzen bis zur Äquikonvergenz. Im Allgemeinen wird eine Menge in Bishops konstruktiver Mathematik durch einen Typ (allgemein als „Voreinstellung“bezeichnet) zusammen mit einer Äquivalenzbeziehung dargestellt.

Wenn (A) und (B) mit Äquivalenzrelationen ausgestattet sind, gibt es natürlich keine Garantie dafür, dass die Auswahlfunktion (f) oben in dem Sinne erweiterbar ist, dass sie äquivalente Elemente äquivalenten Elementen zuordnet. Dies ist das Versagen des Extensionsaxioms der Wahl, siehe Martin-Löf (2009) für eine Analyse.

4. Erweiterungen

4.1 Das logische Framework

Das Obige vervollständigt die Beschreibung einer Kernversion der intuitionistischen Typentheorie, die der von (Martin-Löf 1998 [1972]) nahe kommt.

1986 schlug Martin-Löf eine Neuformulierung der intuitionistischen Typentheorie vor; siehe Nordström, Peterson und Smith (1990) für eine Darstellung. Der Zweck bestand darin, eine kompaktere Formulierung zu erhalten, wobei (lambda) und (Pi) die einzigen variablen Bindungsoperationen sind. Es wird heutzutage als die Hauptversion der Theorie angesehen. Es ist auch die Basis für den Agda Proof Assistant. Die Theorie von 1986 besteht aus zwei Teilen:

• die Theorie der Typen (der logische Rahmen);
• die Theorie der Mengen (kleine Typen).

Bemerkung 4.1. Beachten Sie, dass das Wort „Menge“im logischen Rahmen nicht mit der Art und Weise übereinstimmt, wie es in Bishops konstruktiver Mathematik verwendet wird. Um diese Verwirrung zu vermeiden, werden Typen zusammen mit Äquivalenzbeziehungen in der intuitionistischen Typentheorie üblicherweise als "Setoide" oder "Extensionsmengen" bezeichnet.

Das logische Framework hat nur zwei Typbildner: (Pi x {:} A. B) (normalerweise geschrieben ((x {:} A) B) oder ((x {:} A) rightarrow B.) in der logischen Rahmenformulierung) und (U) (normalerweise als (Set) bezeichnet). Die Regeln für (Pi x {:} A. B) (((x {:} A) rightarrow B)) sind die gleichen wie oben angegeben (einschließlich (eta) - Konvertierung). Die Regeln für (U) ((Set)) sind ebenfalls dieselben, außer dass das logische Framework nur den Abschluss unter (Pi) - Typbildung vorsieht.

Die anderen kleinen Typbildner ("Mengenbildner") werden in die Mengenlehre eingeführt. In der logischen Rahmenformulierung kann jede Formations-, Einführungs- und Eliminierungsregel als Typisierung einer neuen Konstante ausgedrückt werden. Zum Beispiel werden die Regeln für natürliche Zahlen

) begin {align *} N &: \ Set, \\ 0 &: \ N, \\ \ s &: \ N \ rightarrow \ N, \\ \ R &: (C {:} N \ rechter Pfeil \ Set) rechter Pfeil C \, 0 \ rechter Pfeil ((x {:} N) rechter Pfeil C \, x \ rechter Pfeil C \, (s \, x)) rechter Pfeil (c {:} N) rightarrow C \, c. \ end {align *})

wo wir den gemeinsamen Kontext (Gamma) weggelassen haben, da die Typen dieser Konstanten geschlossen sind. Beachten Sie, dass der Rekursionsoperator (R) im Gegensatz zur ursprünglichen Formulierung ein erstes Argument (C {:} N \ rightarrow \ Set) hat.

Darüber hinaus können die Gleichheitsregeln als Gleichungen ausgedrückt werden

) begin {align *} R \, C \, d \, e \, 0 & = d {:} C \, 0 \\ \ R \, C \, d \, e \, (s \, a) & = e \, a \, (R \, C \, d \, e \, a) {:} C \, (s \, a) end {align *})

unter geeigneten Annahmen.

In der Folge werden wir einige Erweiterungen der Typentheorie vorstellen. Um die Darstellung einheitlich zu halten, verwenden wir jedoch nicht die logische Rahmendarstellung der Typentheorie, sondern dieselbe Notation wie in Abschnitt 2.

4.2 A Former Identity Type Former

Wie oben erwähnt, kann die Identität auf natürlichen Zahlen durch primitive Rekursion definiert werden. Identitätsbeziehungen zu anderen Typen können auch in der in Abschnitt 2 vorgestellten Grundversion der intuitionistischen Typentheorie definiert werden.

Martin-Löf (1975) erweiterte jedoch die intuitionistische Typentheorie mit einem einheitlichen primitiven Identitätstypformer (I) für alle Typen. Die Regeln für (I) drücken aus, dass die Identitätsbeziehung durch den Beweis der Reflexivität, einer kanonischen Konstante namens (r), induktiv erzeugt wird. (Beachten Sie, dass (r) in der einleitenden Darstellung von Beweisobjekten in 2.3 durch die Nummer 0 codiert wurde. Die Eliminierungsregel für den Identitätstyp ist eine Verallgemeinerung der Identitätseliminierung in der Prädikatenlogik und führt eine Eliminierungskonstante (ein Wir zeigen hier eher die Formulierung von Paulin-Mohring (1993) als die ursprüngliche Formulierung von Martin-Löf (1975). Die Inferenzregeln sind die folgenden.

(I) - Bildung.) frac { Gamma \ vdash A \ hspace {1em} Gamma \ vdash a {:} A \ hspace {1em} Gamma \ vdash a '{:} A} { Gamma \ vdash \ I (A, a, a ')})

\(I. Einleitung.) frac { Gamma \ vdash A \ hspace {1em} Gamma \ vdash a {:} A} { Gamma \ vdash \ r {:} I (A, a, a)})

(I) - Beseitigung.

) frac { Gamma, x {:} A, y {:} I (A, a, x) vdash C \ hspace {1em} Gamma \ vdash b {:} A \ hspace {1em} Gamma \ vdash c {:} I (A, a, b) hspace {1em} Gamma \ vdash d {:} C [x: = a, y: = r]} { Gamma \ vdash \ J (c, d) {:} C [x: = b, y: = c]})

(I) - Gleichheit (unter geeigneten Annahmen).

) begin {align *} J (r, d) & = d \ end {align *})

Beachten Sie, dass wenn (C) nur von (x: A) und nicht vom Beweis (y: \ I (A, a, x)) abhängt (und wir auch Beweisobjekte unterdrücken) in der Regel von (I) - Eliminierung Wir stellen die Regel der Identitätseliminierung in der Prädikatenlogik wieder her.

Hofmann und Streicher (1998) haben durch die Konstruktion eines Modells der Typentheorie, bei dem Typen als Gruppoide interpretiert werden (Kategorien, bei denen alle Pfeile Isomorphismen sind), gezeigt, dass in der intuitionistischen Typentheorie nicht bewiesen werden kann, dass alle Beweise von (I (A, a, b)) sind identisch. Dies mag als Unvollständigkeit der Theorie erscheinen, und Streicher schlug ein neues Axiom (K) vor, aus dem folgt, dass alle Beweise von (I (A, a, b)) mit (r) identisch sind).

Der Typ (I) - wird oft als intensiver Identitätstyp bezeichnet, da er das Prinzip der Funktionserweiterung nicht erfüllt. Die Theorie des intuitionistischen Typs mit dem Typ der intensiven Identität wird häufig auch als Theorie des intuitionistischen Typs bezeichnet, um sie von der Theorie des extensiven intuitionistischen Typs zu unterscheiden, die in Abschnitt 7.1 vorgestellt wird.

4.3 Fundierte Bäume

Eine Art begründeter Bäume der Form (W x {:} A. B) wurde 1982 in Martin-Löf eingeführt (und in einer eingeschränkteren Form von Scott 1970). Elemente von (W x {:} A. B) sind Bäume mit variierender und willkürlicher Verzweigung: variierend, weil der Verzweigungstyp (B) durch (x {:} A) indiziert ist und willkürlich, weil (B) kann beliebig sein. Der Typ wird durch eine verallgemeinerte induktive Definition angegeben, da die begründeten Bäume unendlich verzweigt sein können. Wir können uns (W x {:} A. B) als die freie Termalgebra vorstellen, wobei jedes (a {:} A) einen Termkonstruktor (sup \, a) mit (möglicherweise) darstellt unendliche Arität (B [x: = a]).

(W) - Bildung.) frac { Gamma \ vdash A \ hspace {2em} Gamma, x {:} A \ vdash B} { Gamma \ vdash \ W x {:} A. B}) (W) -Einführung.) frac { Gamma \ vdash a {:} A \ hspace {2em} Gamma, y {:} B [x: = a] vdash b: Wx {:} A. B} { Gamma \ vdash \ sup (a, yb): \ W x {:} A. B})

Wir lassen die Regeln von (W) - Eliminierung und (W) - Gleichheit weg.

Das Hinzufügen fundierter Bäume zur intuitionistischen Typentheorie erhöht ihre beweistheoretische Stärke erheblich (Setzer (1998)).

4.4 Iterative Mengen und CZF

Eine wichtige Anwendung fundierter Bäume ist Aczels (1978) Konstruktion eines typentheoretischen Modells der konstruktiven Zermelo-Fraenkel-Mengen-Theorie. Zu diesem Zweck definiert er den Typ der iterativen Mengen als

) V = \ W x {:} U. x.)

Sei (A {:} U) ein kleiner Typ und (x {:} A \ vdash M) eine indizierte Familie iterativer Mengen. Dann ist (sup (A, xM)) oder mit einer suggestiveren Notation ({M \ mid x {:} A }) eine iterative Menge. Um es zu paraphrasieren: Eine iterative Menge ist eine Familie von iterativen Mengen, die durch einen kleinen Typ indiziert sind.

Beachten Sie, dass eine iterative Menge ein alt = "sep man icon" /> Zitieren dieses Eintrags ist.

Vorschau der PDF-Version dieses Eintrags bei den Freunden der SEP-Gesellschaft.

Schlagen Sie dieses Eintragsthema im Internet Philosophy Ontology Project (InPhO) nach.

Erweiterte Bibliographie für diesen Eintrag bei PhilPapers mit Links zu seiner Datenbank.

Andere Internetquellen

• Internet-Enzyklopädie der Philosophie: Konstruktive Mathematik
• Scholarpedia: Computational Type Theory
• nLab: Typentheorie