Los topos como modelos de la matemática constructiva

Question

En esta pregunta se argumenta que la matemática constructiva no puede demostrar la existencia de una función real discontinua, porque hay un topos $\mathcal{E}$ donde todas las funciones reales son continuas. Sin embargo, no me queda claro por qué la mera existencia de este topos $\mathcal{E}$ afecta a marcos constructivos como Coq, Agda o la teoría de tipos de homotopía. Si conseguimos definir una función discontinua $f:\mathbb{R}\to\mathbb{R}$ en Coq, produciría una contradicción en $\mathcal{E}$ sólo si $\mathcal{E}$ puede interpretar $f$ y toda la maquinaria de Coq que se utilizó para definir $f$ .

Por ejemplo, el modelo de Coq que conozco en el topos de conjuntos necesita la suposición extra de que hay una infinidad contable de cardinales inaccesibles (para interpretar los universos de Coq). Y dudo que el topos $\mathcal{E}$ automáticamente tiene esos cardenales inaccesibles. Además, si añadimos el axioma del medio excluido en Coq definiremos fácilmente funciones reales discontinuas, y eso seguirá estando bien en $\mathcal{E}$ porque $\mathcal{E}$ no puede interpretar el medio excluido.

Así que me pregunto si topoi como $\mathcal{E}$ sólo dan pistas favorables, pero no pruebas, de que algunas proposiciones no se pueden demostrar constructivamente.

Answer 1

En primer lugar, está claro que una vez que añadimos la lógica clásica a Coq, ya no estamos haciendo matemáticas constructivas.

En segundo lugar, para el caso especial de Coq, está claro que Coq puede interpretarse en cualquier topos autológico (un topos en el que se satisface la colección + la separación) con un número contable de universos de Grothendieck. A la inversa, si Coq es consistente, entonces también lo es ZFC + $\omega$ -muchos universos de Grothendieck (lo que implica la consistencia de la teoría de un topos autológico con $\omega$ -muchos universos de Grothendieck -a saber, la categoría de conjuntos es un topos de este tipo) - véase esta respuesta para más detalles.

Ahora hay bastantes topos en los que todas las funciones $\mathbb{R} \to \mathbb{R}$ son continuos. En general, cuando se interpreta el intuicionismo brouweriano, la herramienta canónica que se utiliza es el segundo modelo de realizabilidad de Kleene. La versión topo-teórica de esto es el topos de realizabilidad sobre el segundo ACP de Kleene. Como se explica aquí Las topos de realizabilidad son automáticamente autológicas cuando la teoría de conjuntos del entorno satisface la colección y la separación.

Resulta que, como se explica aquí , si hay $\omega$ -muchos universos de Grothendieck en la teoría de conjuntos del entorno, entonces hay $\omega$ -muchos en un topos de realizabilidad.

Así, la construcción da como resultado un modelo de Coq en el que todas las funciones $\mathbb{R} \to \mathbb{R}$ son continuos. Así que es relativamente consistente con Coq que todas esas funciones son continuas.

También es posible derivar este principio pasando por un determinado topos de gavilla según Mac Land y Moerdijk. Los topos de gavilla también son automáticamente autológicos cuando la metateoría satisface colección + sustitución, y también heredan $\omega$ -muchos universos de Grothendieck de la teoría de conjuntos ambiental. Así que esta es otra forma de llegar al mismo resultado.

No sé cuál es la situación de HoTT o Agda. Estoy seguro de que las situaciones de Agda y Coq serán similares, pero no tengo experiencia en ese ámbito. Imagino que HoTT admitirá algún tipo de modelos tipo gavilla que nos permitirán paralelismos con las construcciones mencionadas anteriormente, pero no estoy seguro.