Relative Konsistenz von PA und einigen Typentheorien

Für eine Typentheorie meine ich mit Konsistenz, dass es einen Typ gibt, der nicht bewohnt ist. Aus der starken Normalisierung des Lambda-Würfels folgt, dass System und System konsistent sind. Die induktiven Typen MLTT + sind auch normierungssicher. Diese sollten jedoch alle leistungsfähig genug sein, um ein PA-Modell zu konstruieren, das beweist, dass PA mit diesen Theorien konsistent ist. System ist ziemlich leistungsfähig , daher erwarte ich, dass es in der Lage ist, die Konsistenz von PA durch die Konstruktion eines Modells unter Verwendung von Church-Zahlen zu beweisen. MLTT + IT hat einen induktiven Typ mit natürlichen Zahlen und sollte auch Konsistenz nachweisen.$F$$F_\omega$$F$

Dies alles impliziert, dass die Normalisierungsbeweise für diese Theorien nicht in PA internalisiert werden können. So:

1. Können System , System und MLTT + IT tatsächlich die Konsistenz von PA nachweisen?$F$$F_\omega$
2. Wenn ja, welche Metatheorie ist dann erforderlich, um die Normalisierung für System , und MLTT + IT zu beweisen ?$F$$F_\omega$
3. Gibt es eine gute Referenz für die Beweistheorie der Typentheorien im Allgemeinen oder für einige dieser Typentheorien im Besonderen?

Die kurze Antwort auf Ihre Frage 1 ist nein , aber vielleicht aus subtilen Gründen.

Zunächst System und$F$ können die erste Ordnung Theorie der Arithmetik nicht ausdrücken, und noch weniger die Konsistenz von P A .$F_\omega$ $\mathrm{PA}$

Zweitens, und das ist wirklich überraschend ist, nachweisen kann , tatsächlich Konsistenz beider dieser Systeme! Dies geschieht mit dem sogenannten Proof-irrelevanten Modell , das Typen als Mengen ∈ { ∅ , { ∙ } } interpretiert , wobei ∙ ein Dummy-Element ist, das einen Bewohner eines nicht leeren Typs darstellt. Dann kann man ziemlich einfach einfache Regeln für die Operation von → und ∀ auf solche Typen aufschreiben , um ein Modell für System F zu erhalten , in dem der Typ ∀ X ist . X wird mit ∅ interpretiert$\mathrm{PA}$$\in\{\varnothing,\{\bullet\}\}$$\bullet$$\rightarrow$$\forall$$F$$\forall X.X$$\varnothing$. Ähnliches kann man für tun , indem man etwas vorsichtiger höhere Arten als Räume mit endlichen Funktionen interpretiert.$F_\omega$

Es gibt eine scheinbare Paradoxon hier, wo Konsistenz dieser scheinbar leistungsfähigen Systemen unter Beweis stellen können, aber nicht die Normalisierung (wie ich in einem Moment zeigen werde).$\mathrm{PA}$

Die fehlende Zutat ist hier die Realisierbarkeit . Durch die Realisierbarkeit können bestimmte Programme bestimmten Aussagen entsprechen, typischerweise in arithmetischer Form. Ich werde nicht in die Details hier, aber wenn ein Programm einen Vorschlag realisiert φ , geschrieben p ⊩ φ , dann haben wir ein gewisses Beweisstück für φ , insbesondere wenn p Normalisieren ist, dann p ⊮ ⊥ . Wir haben:$p$$\phi$$p\Vdash \phi$$\phi$$p$$p\not\Vdash\bot$

Theorem: Wenn ein Satz 2. Ordnung Arithmetik ist P A 2 , dann gibt es einige geschlossenen Begriff t von System F , so dass t ⊩ $\phi$$\mathrm{PA}_2$$t$$F$

$$t\Vdash\phi$$

Dieser Satz kann in bewiesen werden , und so haben wir P A ⊢ F  ist normalisierend ⇒ P A 2  ist konsistent und Gödels Argument gilt (und P A kann keine Normalisierung von System F beweisen ). Es ist nützlich anzumerken, dass auch die umgekehrte Implikation gilt, so dass wir eine genaue Charakterisierung der beweistheoretischen Potenz haben, die zum Nachweis der Normalisierung von System F erforderlich ist .$\mathrm{PA}$

$$\mathrm{PA}\vdash F\mbox{ is normalizing}\Rightarrow\mbox{$\mathrm{PA}_2$ is consistent}$$ $\mathrm{PA}$$F$$F$

Für das System gibt es eine ähnliche Geschichte , die meiner Meinung nach einer höheren arithmetischen Zahl P A ω entspricht .$F_\omega$$\mathrm{PA}_\omega$

---

Schließlich haben wir den kniffligen Fall von MLTT mit induktiven Typen. Auch hier ergibt sich eine etwas subtile Frage. Sicherlich können wir hier die Konsistenz auszudrücken , so dass kein Problem, und es gibt keinen Beweis-irrelevant Modell, wie wir beweisen können , dass der Typ N a t mindestens 2 Elemente (eine unendliche Menge an unterschiedlichen Elementen , eigentlich).$\mathrm{PA}$$\mathrm{Nat}$

Wir stoßen jedoch auf eine überraschende Tatsache intuitionistischer Theorien höherer Ordnung: , die höherwertige Version von Heyting Arithmetic, ist konservativ gegenüber H A ! Insbesondere können wir nicht die Konsistenz der beweisen P A , (die zu der äquivalent ist , H A ). Ein intuitiver Grund dafür ist, dass Sie mit intuitionistischen Funktionsräumen nicht über eine beliebige Teilmenge von N quantifizieren können , da alle definierbaren Funktionen N → N berechenbar sein müssen.$\mathrm{HA}_\omega$$\mathrm{HA}$$\mathrm{PA}$$\mathrm{HA}$$\mathbb{N}$$\mathbb{N}\rightarrow \mathbb{N}$

Insbesondere glaube ich nicht , Sie Konsistenz beweisen kann , wenn Sie nur natürliche Zahlen zu MLTT ohne Universen hinzuzufügen. Ich glaube, das Hinzufügen von Universen oder "stärkeren" induktiven Typen (wie Ordinaltypen) gibt Ihnen zwar genug Leistung, aber ich fürchte, ich habe keine Referenz dafür. Bei Universen scheint das Argument jedoch recht einfach zu sein, da Sie genug Mengenlehre haben, um ein Modell von H A zu erstellen .$\mathrm{PA}$$\mathrm{HA}$

---

Zum Schluss noch ein paar Hinweise zur Proof-Theorie der Typensysteme: Ich glaube, hier gibt es wirklich eine Lücke in der Literatur, und ich würde mich über eine saubere Behandlung all dieser Themen freuen (tatsächlich träume ich davon, sie eines Tages selbst zu schreiben!). Inzwischen:

• Das Beweis-irrelevante Modell wird hier von Miquel und Werner erklärt, obwohl sie es für die Berechnung von Konstruktionen tun, was die Sache etwas komplizierter macht.

• Das Realisierbarkeitsargument ist in den klassischen Proofs und Types von Girard, Taylor und Lafont skizziert . Ich denke, sie skizzieren auch das Beweis-irrelevante Modell und eine Menge nützlicher Dinge. Es ist wahrscheinlich der erste zu lesende Verweis.

• Das Konservativitätsargument der Heyting-Arithmetik höherer Ordnung findet sich im schwer fassbaren zweiten Band des Konstruktivismus in der Mathematik von Troelstra & van Dalen (siehe hier ). Beide Bände sind äußerst informativ, aber für einen Anfänger, IMHO, ziemlich schwer zu lesen. Es werden auch "moderne" typentheoretische Fächer etwas vermieden, was angesichts des Alters der Bücher nicht verwunderlich ist.

---

Eine zusätzliche Frage in den Kommentaren betraf die genaue Konsistenzstärke / Normalisierungsstärke von MLTT + -Induktiven. Ich habe hier keine genaue Antwort, aber sicherlich hängt die Antwort von der Anzahl der Universen und der Art der erlaubten induktiven Familien ab. Rathjen untersucht diese Frage in dem hervorragenden Aufsatz Die Stärke einiger Martin-Lof-Typ-Theorien .

WRT Normalisierung, die Grundidee ist , dass , wenn, für 2 Theorien und U , haben wir P A ⊢ C o n ( T ) ⇒ C o n ( U$\cal{T}$$\cal{U}$

$$\mathrm{PA}\vdash\mathrm{Con}(\cal{T})\Rightarrow\mathrm{Con}(\cal{U})$$

dann im Allgemeinen

$$\mathrm{PA}\vdash \mbox{1-$\mathrm{Con}$}(\cal{T})\Rightarrow\mathrm{Norm}(\cal{U})$$

wobei 1- ist 1-Konsistenz und N o r m ist (schwach) Normalisierung.$\mathrm{Con}$$\mathrm{Norm}$

$\mathrm{HA}_\omega$

Was MLTT mit Induktion-Rekursion oder Induktion-Induktion betrifft, so weiß ich nicht, wie es ist, und AFAIK, das Problem der exakten Konsistenzfestigkeit ist immer noch offen.