¿Implica el teorema de Diaconescu que la teoría de tipos cúbicos no es constructiva?

Question

Según este La teoría de tipos de Martin-Löf tiene como teorema el axioma de elección (bajo la noción de "proposiciones como tipos"). Es decir, teoría de tipos cúbicos puede demostrar el axioma de elección (es una extensión de la teoría de tipos de Martin-Löf).

Martin-Löf no se ve afectado por Teorema de Diaconescu ya que no puede demostrar la intensionalidad (si para todo x, f x = g x entonces f = g). Pero la teoría de tipos cúbicos puede demostrar la intensionalidad . Esto no me parece correcto, ¿debo estar entendiendo algo mal o algo está roto? La teoría de tipos cúbicos está diseñada para que los fundamentos univalentes (es decir, la teoría de tipos de homotopía) no hagan que los teoremas sean computacionalmente atascado . Normalmente, en la teoría de Martin-Löf se toma la univalencia como sus axiomas (digamos, postularla en Coq o Agda) pero esto hace que todos sus teoremas sean computacionalmente atascado . En cambio, la teoría de los tipos cúbicos evita este problema. Pero parece que el teorema de Diaconescu implica que la teoría de tipos cúbicos puede demostrar la ley del medio excluido y, por tanto, no es constructiva. Ahora bien, si la teoría de los tipos cúbicos no es constructiva, entonces Correspondencia Curry-Howard no se sostiene. ¿Qué está pasando aquí, qué me estoy perdiendo? ¿Es la teoría del tipo cúbico realmente no constructiva?

Answer 1

En primer lugar, donde dice "intensionalidad", quiere decir "extensionalidad" y específicamente "extensionalidad de la función".

La página de Wikipedia sobre Teorema de Diaconescu utiliza el axioma de extensionalidad para los conjuntos que establece que para los conjuntos $S$ y $T$ , $S=T\iff(\forall x\in S.x\in T)\land(\forall x\in T.x\in S)$ . También menciona (sin citarlo claramente) que la razón por la que el teorema de Diaconescu no se aplica a las teorías de tipo constructivo es porque no tienen un análogo del axioma de separación .

Las teorías de tipos constructivos no tienen necesariamente un clasificador de subobjetos. A veces, por ejemplo, en el Cálculo de Construcciones, hay un tipo $\mathsf{Prop}$ que está estrechamente relacionado con un clasificador de subobjetos. En HoTT, como se describe en sección 3.5 del libro HoTT podemos definir un tipo $\mathsf{Prop}_{\mathcal U}$ a través de $\sum_{A:\mathcal U}\mathsf{isProp}(A)$ . Si asumimos un axioma de redimensionamiento proposicional, podemos definir $\Omega\equiv\mathsf{Prop}_{\mathcal{U}_0}$ que será del tipo $\mathcal{U}$ para cualquier $\mathcal U$ que es un universo más grande que $\mathcal{U}_0$ . Esto se comporta más como un clasificador de subobjetos. En este punto, el libro HoTT hace referencia a sección 10.1.4 que se pregunta si la categoría de conjuntos (es decir $0$ -tipos en $\mathcal U$ ) definida en el capítulo 9 es un topos elemental, es decir, si tiene un clasificador de subobjetos. $\mathsf{Prop}_{\mathcal U}$ casi funcionaría si no fuera porque es "demasiado grande" para ser del tipo $\mathcal U$ pero el redimensionamiento propositivo nos permitiría utilizar $\Omega$ que es de tipo $\mathcal U$ . La siguiente sección presenta el teorema de Diaconescu en este contexto. Se basa en la presentación del axioma de elección en sección 3.8 .

El axioma de elección de la sección 3.8 es diferente del "axioma" teórico de elección demostrable descrito anteriormente en el libro en sección 1.6 . Una forma de pensar en la diferencia entre la lógica clásica y la constructiva es que la lógica constructiva introduce nuevas conectivas lógicas: la disyunción constructiva y el existencial constructivo. (Edward Nelson lo describe así También es evidente en semántica categórica para la lógica clásica y también es explícito en el fin de la sección 3.7 donde $P\lor Q$ y $\exists x:X.P(x)$ se definen como $||P+Q||$ y $||\sum_{x:X}P(x)||$ respectivamente). Por lo tanto, la cuestión de qué noción de existencial utilizar al formular el axioma de elección es significativa. Si utilizamos el "existencial constructivo", es decir, la suma dependiente, entonces obtenemos el "axioma" de elección de la teoría de tipos. Si utilizamos el "existencial clásico", es decir, el truncamiento proposicional de la suma dependiente (de una familia de meras proposiciones), obtenemos algo que se comporta como el axioma tradicional de elección (y que no es demostrable), incluso dando lugar al teorema de Diaconescu. Lo que usó Diaconescu es la formulación habitual en la teoría de las categorías, es decir, que todos los epimorfismos se dividen. Se podría imaginar la formalización de esto como $\prod_{A,B:\mathcal U}\prod_{f:A\to B}(\prod_{b:B}\sum_{a:A}f(a)=b)\to\sum_{g:B\to A}\prod_{a:A}f(g(a))=a$ pero esta es una afirmación interna y "todos los epimorfismos se dividen" es una afirmación externa y no hay razón para esperar que la afirmación interna refleje la externa (y, de nuevo, tendríamos que decidir si queremos $\Sigma$ o $\exists$ ).

Así que, dicho todo esto, el "axioma" teórico del tipo de elección no es obviamente la formulación interna apropiada del axioma de elección (de hecho, creo que la mayoría diría que obviamente no es la formulación interna apropiada), Diaconescu no está utilizando una formulación interna de todos modos, y además Diaconescu estaba hablando de la formulación elemental ( $1$ -)topos mientras que los modelos previstos de HoTT son $(\infty,1)$ -topos. En particular, los subobjetos parecen mucho menos informativos sobre la estructura categórica superior y, de hecho, en el libro de HoTT el Axioma de Elección se limita a tipos con bajo nivel h y sólo habla del teorema de Diaconescu con respecto a estos tipos de bajo nivel h.

Como nota final, existen correspondencias de estilo Curry-Howard con los sistemas de prueba clásicos, en particular el $\lambda\mu$ -Cálculo de Parigot que recibe una semántica categórica en el documento que mencioné anteriormente .