Quero saber se a decidibilidade da igualdade de duas provas decidíveis da mesma proposição pode ser comprovada sem axiomas adicionais em Cálculo de construções indutivas.
Especificamente, quero saber se isso é verdade sem axiomas adicionais no Coq.
Obrigado!
Editado para corrigir o erro: Edite 2 para tornar Prop
mais explícito
Respostas:
Como Neel aponta, se você trabalha sob as "proposições são tipos", pode facilmente criar um tipo cuja igualdade não possa ser mostrada decidível (mas é claro que é consistente assumir que todos os tipos têm igualdade decidível), como .N→N
Se entendermos "proposição" como um tipo de tipo mais restrito, a resposta dependerá do que exatamente queremos dizer. Se você está trabalhando no cálculo de construções de umN→N
Prop
tipo, ainda não pode mostrar que proposições decidíveis têm igualdade decidível. Isso ocorre porque, no cálculo das construções, é consistente equiparar-seProp
a um universo de tipo relevante para prova, portanto, pelo que você sabe,Prop
pode conter algo como . Isso também implica que você não pode provar seu teorema para a noção de Coq de .Prop
Mas, em qualquer caso, a melhor resposta vem da teoria dos tipos de homotopia. Uma proposição é um tipo que satisfaz Ou seja, uma proposição tem no máximo um elemento (como deveria se fosse para ser entendido como um valor de verdade irrelevante para a prova). Nesse caso, a resposta é obviamente positiva, porque a definição de proposição implica imediatamente que sua igualdade é decidível.∀ x , y : PP
Estou curioso para saber o que você quer dizer com "proposição".
fonte
Prop