Gdzie jest dowód, że Coq + Wykluczone Środek jest spójny

Widziałem (i słyszałem), że twierdził, że można bezpiecznie dodać klasyczny aksjomat wykluczonego środka do Coq, ale nie mogę znaleźć dokumentu potwierdzającego to twierdzenie. Artykuły, które widzę na liście na wiki Coq o wykluczonym środku, wykazują niespójność z impredykatywnym Setem.

Rzeczywiście wydaje się, że Coquand stwierdza, że ​​dodanie Wykluczonego Środka (mieszkańca ) jest niespójne dla CoC w sekcji 4.5.3 jego opisu (PDF) metateorii CoC. Jednak ta sekcja jest dla mnie trochę zawiła, więc mogę bardzo źle go odczytać.$A+\neg A$

Właściwie w sekcji 4.5.3 nie do końca mówi, że impredykatywność EM + jest niespójna. Mówi, że kiedy to założysz, model musi stać się degeneracyjnie nieistotny dla dowodu (interpretacja wszystkich typów innych niż Prop może mieć co najwyżej jeden element). Andy Pitts opisuje podobne zjawisko: „Nietrywialne typy mocy nie mogą być podtypami typów polimorficznych” .

W przypadku predykcyjnych wersji teorii typów prawdopodobnie łatwiej jest po prostu zrobić dowód spójności niż w przypadku Google - rozwarstwienie wszechświata zapewnia wszystko, czego potrzebujesz do prostego modelu teoretycznego zestawu typów (tzn. Typy są zbiorami, terminy są mapy) do wypracowania. Zauważ tylko, że zbiory są zamknięte pod indeksowanymi sumami i produktami, i przytul się aksjomatem zastępowania przy interpretacji wszechświatów. Jest to oczywiście zła praktyka akademicka, ale dowód nadal warto samemu wykonać.