Igualdade de provas decidíveis?

9

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.

P:Prop,P¬P(p1:P,p2:P,{p1=p2}{p1p2})

Obrigado!

Editado para corrigir o erro: Edite 2 para tornar Propmais explícito

Adam Barak
fonte
11
O que você escreveu não faz sentido. Se é uma proposição, então é uma prova e você não pode formar . Você quis dizer que sua hipótese é vez de , ou seja, " é decidível"? Pp:Pp¬pP¬Pp¬pP
Andrej Bauer
Desculpe, eu quis dizer a hipótese " é decidível", ou seja,PP¬P
Adam Barak
2
Considere como , e a declaração é falsa, pois você pode habitar facilmente com , e a equivalência de funções é obviamente indecidível. Existem outras condições em você tem em mente? PNN(NN)¬(NN)inl(λx.x)P
Neel Krishnaswami
P deve ser uma proposição. (Na verdade, no meu desenvolvimento, eu já uso a extensionalidade funcional, de modo que a declaração ainda pode ser válida para mim, mas vamos ignorar a extensionalidade funcional / proposicional por enquanto).
11134 Adam Barak
A extensionalidade da função não implica que a equivalência da função seja decidível ... E a resposta de Neel resolve o caso geral: se P é um tipo infinito (habitado) (que inclui alguns tipos de proposições se nenhum axioma extra for incluído), a implicação falhará a espera por . PP
C4:

Respostas:

5

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 .NN

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 um Proptipo, 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-se Propa um universo de tipo relevante para prova, portanto, pelo que você sabe, Proppode conter algo como . Isso também implica que você não pode provar seu teorema para a noção de Coq de .NNProp

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

x,y:P.x=y.

Estou curioso para saber o que você quer dizer com "proposição".

Andrej Bauer
fonte
Como você teria dentro ? Obrigado! NNProp
Adam Barak
Não há nada no cálculo da construção que impeça , existe? Prop=Type
Andrej Bauer
A confusão aqui é sobre o que se entende por "sistema coq". Se for "o cálculo das construções", então . Se o "Cálculo de construções indutivas com 1 universo impredicativo" mais preciso, então não sentido sem as anotações no nível do universo. Até onde eu sei, é um axioma consistente (embora inconsistente com o EM por motivos sutis). T y p e T y p e 1 = P r o pProp=Set=TypeTypeType1=Prop
Cody
Claro, temos que um índice em . O ponto para @AdamBarak entender é o seguinte: como não leva a nenhuma contradição no Coq, podemos mostrar que algo não pode ser feito no Coq, mostrando que isso levaria a uma contradição se também tivéssemos . P r o p = T y p e 1 P r o p = T y p e 1TypeProp=Type1Prop=Type1
Andrej Bauer
11
Ainda não está certo, porque em Coq não podemos mostrar que a equivalência funcional é indecidível. A afirmação "igualdade em é decidível" é o que Martin Escardo chama de tabu construtivo: não pode ser provado nem refutado no Coq. Portanto, o argumento correto é: se então é uma proposição e a declaração "igualdade em é decidível "não é comprovável. (Considerando que você disse: e a declaração "igualdade em é decidível" é falsa). NNProp=Type1NNNNNN
Andrej Bauer 12/12