Wo ist der Beweis, dass Coq + Excluded Middle konsistent ist?

21

Ich habe gesehen (und gehört), dass behauptet wird, dass es sicher ist, das klassische Axiom der ausgeschlossenen Mitte zu Coq hinzuzufügen, aber ich kann anscheinend kein Papier finden, das diese Behauptung stützt. Die Papiere, die ich im Coq-Wiki über ausgeschlossene Mitten sehe, weisen Inkonsistenzen mit Impredicative Set auf.

Tatsächlich scheint Coquand in Abschnitt 4.5.3 seiner Beschreibung (PDF) der CoC-Metatheorie zu behaupten, dass das Hinzufügen von Excluded Middle (ein Einwohner von ) für CoC inkonsistent ist . Allerdings ist dieser Abschnitt für mich etwas abstrus, sodass ich ihn möglicherweise falsch interpretiere.A+¬A

Mark Reitblatt
quelle
6
So etwas muss auf der CoQ-Mailingliste angefragt werden.
Andrej Bauer
1
Duh. Aus irgendeinem Grund ist mir dieser offensichtliche Ort durch den Kopf gegangen. Wenn Sie einen Hammer haben ...
Mark Reitblatt
9
macht mich glücklich, dass die Leute darüber nachdenken, zuerst hier zu posten, auch bei Fragen zu Theorie B, die nicht genug Beachtung finden :)
Suresh Venkat

Antworten:

11

Tatsächlich sagt er in Abschnitt 4.5.3 nicht ganz, dass EM + Impredicativity inkonsistent ist. Er sagt, dass das Modell, wenn Sie es annehmen, entartet Beweis-irrelevant werden muss (die Interpretation aller Typen außer Prop kann höchstens ein Element haben). Andy Pitts beschreibt ein ähnliches Phänomen "Nicht-triviale Potenztypen können keine Subtypen polymorpher Typen sein" .

Für prädikative Versionen der Typentheorie ist es wahrscheinlich einfacher, nur den Konsistenznachweis zu erbringen, als für Google. Die Universumsschichtung bietet Ihnen alles, was Sie für das einfältige satztheoretische Modell von Typen benötigen (dh Typen sind Mengen, Begriffe sind) Karten) zu erarbeiten. Beobachten Sie einfach, dass Mengen unter indizierten Summen und Produkten geschlossen sind, und lernen Sie den Grundsatz des Ersetzens bei der Interpretation von Universen kennen. Dies ist natürlich eine schlechte akademische Praxis, aber der Beweis ist es trotzdem wert, für sich selbst erbracht zu werden.

Neel Krishnaswami
quelle
Vielen Dank. Und für Verbesserungsvorschläge?
Mark Reitblatt
2
2