Где доказательство того, что Coq + исключенное среднее непротиворечиво

21

Я видел (и слышал), что он утверждал, что безопасно добавить классическую аксиому исключенного среднего к Coq, но я не могу найти документ, подтверждающий это утверждение. Статьи, которые я вижу в списке в вики Coq о исключенной середине, показывают несоответствие с нечетким множеством.

Действительно, кажется, что Кокванд заявляет, что добавление Исключенного Среднего (житель ) несовместимо с CoC в разделе 4.5.3 его описания (PDF) метатеории CoC. Тем не менее, этот раздел немного заумный для меня, поэтому я вполне могу неправильно его прочитать.A+¬A

Марк Рейтблатт
источник
6
Такого рода вещи нужно спросить в списке рассылки coq.
Андрей Бауэр
1
Duh. По какой-то причине это очевидное место ускользнуло от меня. Когда у тебя есть молоток ...
Марк Рейтблатт
9
меня радует, что люди думают о том, чтобы публиковать здесь в первую очередь, даже для вопросов теории B, которые не получают достаточного внимания :)
Суреш Венкат

Ответы:

11

На самом деле, в разделе 4.5.3 он не совсем говорит, что непредсказуемость EM + противоречива. Он говорит, что когда вы предполагаете это, модель должна вырожденно не иметь отношения к доказательству (интерпретация всех типов, кроме Prop, может содержать не более одного элемента). Энди Питтс описывает похожее явление: «Нетривиальные типы степеней не могут быть подтипами полиморфных типов» .

Для предикативных версий теории типов, вероятно, проще сделать доказательство непротиворечивости, чем для Google - стратификация вселенной дает вам все, что нужно для простодушной теоретико-множественной модели типов (т. Е. Типы - это наборы, термины - это карты), чтобы выработать. Просто обратите внимание, что наборы закрыты под индексированными суммами и продуктами, и при интерпретации вселенных освоитесь с аксиомой замены. Конечно, это плохая учебная практика, но доказательство все же стоит сделать для себя.

Нил Кришнасвами
источник
Спасибо. А за неимоверную опору?
Марк Рейтблатт
2
2