Eu já vi (e ouvi) afirmar que é seguro acrescentar o axioma clássico do meio excluído ao Coq, mas não consigo encontrar um documento que apoie essa afirmação. Os artigos que vejo listados no wiki da Coq sobre o meio excluído estão mostrando inconsistência com o conjunto impredicativo.
De fato, parece que Coquand afirma que adicionar Meio Excluído (um habitante de ) é inconsistente para o CoC na seção 4.5.3 de sua descrição (PDF) da metateoria do CoC. No entanto, esta seção é um pouco obscura para mim, então eu posso muito bem interpretá-lo mal.
reference-request
lo.logic
coq
Mark Reitblatt
fonte
fonte
Respostas:
Na verdade, na seção 4.5.3, ele não diz exatamente que a impredicatividade do EM + é inconsistente. Ele diz que, quando você assume, o modelo deve se tornar degeneradamente irrelevante (a interpretação de todos os tipos, exceto Prop, pode ter no máximo um elemento). Andy Pitts descreve um fenômeno semelhante "Tipos de energia não triviais não podem ser subtipos de tipos polimórficos" .
Para versões predicativas da teoria dos tipos, provavelmente é mais fácil fazer apenas a prova de consistência do que procurar no Google - a estratificação do universo fornece tudo o que você precisa para o modelo teórico de conjunto de tipos simples (ou seja, tipos são conjuntos, termos são mapas) para dar certo. Apenas observe que os conjuntos são fechados com somas e produtos indexados e se familiarizam com o axioma da substituição ao interpretar universos. É uma prática acadêmica ruim, é claro, mas ainda vale a pena fazer a prova por si mesmo.
fonte