Quiero saber si la capacidad de decisión de igualdad de dos pruebas decidibles de la misma proposición puede demostrarse sin ningún axioma adicional en el cálculo de construcciones inductivas.
Específicamente, quiero saber si esto es cierto sin ningún axioma adicional en Coq.
¡Gracias!
Editado para corregir el error: Editar 2 para hacer Prop
más explícito
Respuestas:
Como señala Neel si trabajas bajo "las proposiciones son tipos", entonces puedes encontrar fácilmente un tipo cuya igualdad no se puede mostrar como decidible (pero, por supuesto, es consistente asumir que todos los tipos tienen igualdad decidible), como .N→N
Si entendemos "proposición" como un tipo de tipo más restringido, entonces la respuesta depende de lo que queremos decir exactamente. Si está trabajando en el cálculo de construcciones con unN→N
Prop
tipo, entonces todavía no puede demostrar que las proposiciones decidibles tienen igualdad decidible. Esto es así porque es consistente en el cálculo de las construcciones de equipararProp
con un universo de tipo de prueba relevante, por lo que para todo lo que sabeProp
fuerzas contiene algo así como . Esto también implica que no puede probar su teorema para la noción de Coq .Prop
Pero, en cualquier caso, la mejor respuesta proviene de la teoría del tipo de homotopía. Hay una proposición de tipo que satisface ∀ x , y : PP
Es decir, una proposición tiene como máximo un elemento (como debería ser si se entiende como un valor de verdad irrelevante para la prueba). En este caso, la respuesta es, por supuesto, positiva porque la definición de proposición implica inmediatamente que su igualdad es decidible.
Tengo curiosidad por saber qué quieres decir con "proposición".
fuente
Prop