¿Igualdad de pruebas decidibles?

9

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.

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

¡Gracias!

Editado para corregir el error: Editar 2 para hacer Propmás explícito

Adam Barak
fuente
1
Lo que escribiste no tiene sentido. Si es una proposición, entonces p : P es una prueba, y no puede formar p ¬ p . ¿Quiso decir que su hipótesis era P ¬ P en lugar de p ¬ p , es decir, " P es decidible"? Pp:Pp¬pP¬Pp¬pP
Andrej Bauer
Lo siento, quise decir la hipótesis " es decidible", es decir, P ¬ PPP¬P
Adam Barak
2
Tome como NN , y la afirmación es falsa, ya que puede habitar fácilmente ( NN ) ¬ ( NN ) con i n l ( λ x .PNN(NN)¬(NN) , y la equivalencia de funciones es obviamente indecidible. ¿Hay otras condiciones sobre P que tenga en mente? inl(λx.x)P
Neel Krishnaswami
P debería ser una propuesta. (En realidad, en mi desarrollo, ya utilizo la extensionalidad funcional, por lo que la declaración aún puede ser válida para mí, pero ignoremos la extensionalidad funcional / proposicional por ahora).
Adam Barak
La extensionalidad de la función no implica que la equivalencia de la función sea decidible ... Y la respuesta de Neel resuelve el caso general: si P es un tipo infinito (habitado) (que incluye algunos tipos de proposiciones si no se incluyen axiomas adicionales), entonces la implicación falla para el asimiento para . PP
cody

Respuestas:

5

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

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 un Proptipo, 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 equiparar Propcon un universo de tipo de prueba relevante, por lo que para todo lo que sabe Propfuerzas contiene algo así como . Esto también implica que no puede probar su teorema para la noción de Coq .NNProp

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.

x,y:P.x=y.

Tengo curiosidad por saber qué quieres decir con "proposición".

Andrej Bauer
fuente
¿Cómo tendrías adentro ? ¡Gracias! NNProp
Adam Barak
No hay nada en el cálculo de la construcción que impida , ¿verdad? Prop=Type
Andrej Bauer
La confusión aquí es sobre lo que se entiende por "el sistema coq". Si es "el cálculo de las construcciones", entonces . Si el "Cálculo de construcciones inductivas con 1 universo impredecible" más preciso, entonces T y p e no tiene sentido sin anotaciones a nivel de universo. Hasta donde yo sé, T y p e 1 = P r o p es un axioma consistente (aunque inconsistente con EM por razones sutiles). Prop=Set=TypeTypeType1=Prop
cody
Claro, tenemos que agregar un índice en . El punto que debe entender @AdamBarak es el siguiente: debido a que P r o p = T y p e 1 no genera ninguna contradicción en Coq, podemos demostrar que no se puede hacer algo en Coq al mostrar que conduciría a una contradicción si también tuvimos P r o p = T y p e 1 . TypeProp=Type1Prop=Type1
Andrej Bauer
1
Todavía no está del todo bien, porque en Coq no podemos mostrar que la equivalencia funcional sea indecidible. La afirmación "la igualdad en es decidible" es lo que Martin Escardo llama un tabú constructivo: no se puede probar ni refutar en Coq. Entonces el argumento correcto es: si P r o p = T y p e 1 entonces NN es una proposición, y la afirmación "la igualdad en NN es decidible" no es demostrable. (Mientras que usted dijo: y la afirmación "la igualdad en NN es decidible" es falsa). NNProp=Type1NNNNNN
Andrej Bauer