¿Dónde está la prueba de que Coq + Excluded Middle es consistente

21

He visto (y he oído) que afirmaba que es seguro agregar el axioma clásico del medio excluido a Coq, pero parece que no puedo encontrar un documento que respalde esta afirmación. Los documentos que veo enumerados en el wiki de Coq sobre el medio excluido muestran inconsistencia con el conjunto impredecible.

De hecho, parece que Coquand afirma que agregar Excluded Middle (un habitante de ) es inconsistente para CoC en la sección 4.5.3 de su descripción (PDF) de la metateoría de CoC. Sin embargo, esta sección es un poco absurda para mí, por lo que muy bien podría estar interpretándolo mal.A+¬A

Mark Reitblatt
fuente
66
Este tipo de cosas se deben preguntar en la lista de correo de coq.
Andrej Bauer
1
Duh Por alguna razón, este lugar obvio se me olvidó. Cuando tienes un martillo ...
Mark Reitblatt
99
me alegra que la gente piense en publicar aquí primero, incluso para preguntas de teoría B que no reciben suficiente atención :)
Suresh Venkat

Respuestas:

11

En realidad, en la sección 4.5.3, no dice que la impredicatividad EM + sea inconsistente. Él dice que cuando lo asumes, el modelo debe volverse degeneradamente irrelevante a prueba (la interpretación de todos los tipos que no sean Prop puede tener como máximo un elemento). Andy Pitts describe un fenómeno similar "Los tipos de poder no triviales no pueden ser subtipos de tipos polimórficos" .

Para las versiones predicativas de la teoría de tipos, probablemente sea más fácil hacer la prueba de consistencia que Google: la estratificación del universo le brinda todo lo que necesita para el modelo de tipos de teoría simple de conjuntos (es decir, los tipos son conjuntos, los términos son mapas) para hacer ejercicio. Solo observe que los conjuntos están cerrados bajo sumas y productos indexados, y póngase cómodo con el axioma de reemplazo al interpretar universos. Esta es una mala práctica académica, por supuesto, pero la prueba aún vale la pena.

Neel Krishnaswami
fuente
Gracias. ¿Y para una propuesta impredicativa?
Mark Reitblatt
2
2