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.
reference-request
lo.logic
coq
Mark Reitblatt
fuente
fuente
Respuestas:
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.
fuente