¿Qué puede expresarse y demostrarse con la lógica interna de un topos?

Question

El título de este post expresa lo que realmente quiero, que es aprender a manejar la lógica interna de un topos de forma más eficaz. Sin embargo, para poner los pies en la tierra, voy a hacer algunas preguntas básicas sobre el topos $\mathcal{Grph}$ de grafos dirigidos, cuya categoría subyacente es $$\mathcal{Grph}:={\bf Set}^{\mathcal{G}}.$$ Aquí $\mathcal{G}$ es la categoría de indexación para grafos, con dos objetos $A$ y $V$ y con dos morfismos $src,tgt\colon A\to V\ $ .

¿Qué puedo expresar en la lógica interna del topos $\mathcal{Grph}$ Digamos que usando el lenguaje Mitchell-Benabou o la semántica Joyal-Kripke, o lo que sea. ¿Cómo puedo utilizar esta lógica para demostrar cosas? ¿Qué tipo de cosas no se pueden decir o demostrar de este modo?

A continuación figuran algunas preguntas concretas. En cada caso, cuando pregunto "¿Puedo...?", quiero decir "¿Hasta qué punto puedo utilizar el lenguaje interno y la lógica de...? $\mathcal{Grph}$ a...".

1. ¿Puedo expresar que un gráfico $X$ es finito, (respectivamente completo, discreto)?
2. ¿Puedo hacer un gráfico $X$ y producir el gráfico de rutas $Paths(X)\ $ cuyo vértices son los de $X$ pero cuyo flechas son todas caminos de longitud finita en $X$ ?
3. ¿Puedo expresar que $Paths$ es una mónada, es decir, produce algún morfismo $X\to Paths(X)\ $ y otro $Paths(Paths(X))\to Paths(X)\ $ con algunas propiedades?
4. ¿Puedo hacer un gráfico $X$ y producir el subgrafo $L\subseteq X$ formado por todos los vértices y flechas que intervienen en un bucle? (Es decir, una flecha $a\in X(A)$ está en $L$ si existe un camino $P$ de longitud $n$ en $X$ tal que $a\in P$ y $P$ es un bucle: $P(0)=P(n)\ $ . Un vértice $v\in X(V)$ está en $L$ si es el origen de una flecha en $L$ .)
5. ¿Puedo demostrar que si un grafo no tiene bucles y tiene un número finito de vértices, entonces tiene un número finito de caminos?
6. ¿Puedo hacer algo más en $\mathcal{Grph}$ que podría ser divertido e informativo?

Quizá este post refleje un malentendido básico sobre cómo pensar en la lógica interna de un topos. Si es así, por favor, acláremelo. Además, estaría bien una pregunta tipo test del tipo "a ver si puedes expresar/probar esto en $\mathcal{Grph}$ : _ _ ."

Answer 1

En general, el lenguaje interno de un topos sólo puede expresar aquellas afirmaciones que tienen sentido en cada topos. En esencia, esto te limita a algo parecido a la teoría de conjuntos de Zermelo acotada, sin pertenencia global.

La forma correcta de utilizar el lenguaje interno de un particular topos, como su topos de grafos dirigidos, es enriquecer el lenguaje interno general de los topos con nuevos tipos primitivos y nuevos axiomas. Si tiene suerte, podrá añadir sólo el axioma y definir los nuevos tipos (es decir, los nuevos tipos pueden caracterizarse en el lenguaje interno). Veamos cuáles pueden ser en el caso del topos de grafos dirigidos.

Dado que estamos tratando con un topos presheaf podemos decir de antemano que la incrustación (covariante) de Yoneda $y : \mathcal{G} \to \mathbf{Set}^\mathcal{G}$ nos dará algo importante. Así es, $y(V)$ es el gráfico con un vértice y sin flechas, mientras que $y(A)$ es el grafo con dos vértices y una flecha entre ellos. Permíteme escribir $V$ y $A$ en lugar de $y(V)$ y $y(A)$ respectivamente. Podríamos llamar $V$ "el vértice" y $A$ "la flecha". Obviamente, llamamos "grafos" a los objetos de nuestro topos.

Cálculos sencillos revelan que, para un gráfico dado $G$ :

• $G \times V$ es el grafo discreto asociado en los vértices de $G$ .
• $G^V$ es el grafo completo asociado en los vértices de $G$ .
• $G \times A$ es el siguiente gráfico: para cada vértice $g$ en $G$ obtenemos dos vértices $(g,s)$ y $(g,y)$ en $G \times A$ (piense en ellos como " $g$ como fuente" y " $g$ como objetivo"), y para cada flecha $a : g \to g'$ en $G$ obtenemos una flecha $a : (g,s) \to (g',t)$ en $G \times A$ . Esto probablemente signifique algo para los teóricos del grafismo, no me sorprendería que tuvieran un nombre para ello.
• $G^A$ es el "grafo de flechas" asociado: los vértices de $G^A$ son pares de vértices $(g,g')$ de $G$ y para cada flecha $a : g \to h$ obtenemos una flecha $a : (g,g') \to (h',h)$ en $G^A$ . Esto tiene más sentido una vez que se calculan los puntos globales de $G^A$ corresponden exactamente a las flechas de $G$ . Además, es útil pensar en los vértices de $G^A$ como "flechas potenciales de $G$ ".

Ya podemos responder a algunas de sus preguntas:

• Un gráfico $G$ es discreta cuando la proyección $G \times V \to G$ está dentro.
• Un gráfico $G$ es completo cuando el mapa canónico $G \to G^V$ está dentro.

Te gustaría tener el gráfico de caminos $\mathsf{Path}(G)$ de un gráfico dado $G$ . Creo que has descrito el gadget equivocado, es decir, lo que deberías buscar es un gráfico cuyo puntos globales son las trayectorias en $G$ pero habrá muchas otras cosas "potenciales" flotando por ahí. Hasta ahora no hemos utilizado el hecho de que hay dos morfismos $s, t : A \to V$ . Esto nos permite formar "caminos genéricos de longitud $n$ " $P_n$ como pullbacks: $P_1 = A$ , $P_2 = A \times_V A$ es el pullback de $s : A \to V$ y $t : A \to V$ etc. Con un poco de cuidado deberíamos ser capaces de formar el objeto de "caminos genéricos" $P$ equipado con una operación de concatenación que lo convierte en un monoide. Voy a suponer ingenuamente que los vértices de $P$ son pares de números naturales $(k,n)$ con $k < n$ y que las flechas son de la forma $(k,n) \to (k+1,n)$ . Pero esto hay que comprobarlo, y en cualquier caso debería ser posible definir lo "correcto" $P$ internamente. El gráfico $\mathsf{Path}(G)$ que busca debe ser la suma dependiente $\sum_{p : P} G^p$ (y esto se parece mucho a un functor polinómico). La estructura monoide de $P$ debería darte una mónada.

En cuanto a los caminos cíclicos (tú los llamas bucles): si no me equivoco los grafos internamente proyectivos son aquellos grafos cuyos grados de entrada y salida son todos 1, es decir, los ciclos y el camino infinito que se extiende en ambas direcciones. Esto debería ayudar a entender los caminos cíclicos. Que un grafo $G$ es internamente proyectiva puede expresarse en el lenguaje interno como "cada $G$ -la familia indexada de grafos habitados tiene una función de elección", es decir, se trata de los objetos que satisfacen el axioma de elección, internamente.

El vértice $V$ es un subobjeto del objeto terminal $1$ que es el grafo con un único vértice y una única flecha. Por lo tanto, existe un valor de verdad correspondiente $v \in \Omega$ que es una especie de valor de verdad "intermedio". Podemos definir un operador de cierre $j : \Omega \to \Omega$ (una modalidad) por $j(p) = (v \Rightarrow p)$ . Esta modalidad debería denominarse "de vértice". En efecto, si $H \hookrightarrow G$ es un subgrafo de $G$ entonces su $j$ -cierre $\bar{H} \hookrightarrow G$ es el subgrafo de $G$ inducida por los vértices de $H$ . Ah, pero esto es entonces lo mismo que el complemento del complemento de $H$ por lo que vemos que $j$ es sólo el cierre de la doble negación. (Espero estar haciéndolo bien, hablo de memoria). Si estoy en lo cierto, entonces podemos definir $V$ en el lenguaje interno, utilizando un axioma:

Axioma: existe un valor de verdad $v \in \Omega$ tal que $(v \Rightarrow p) = \lnot\lnot p$ para todos $p \in \Omega$ .

Entonces $V = \lbrace * \in 1 \mid v \rbrace$ . Todavía tenemos que hacer algo $A$ Sin embargo.

En cualquier caso, mi experiencia con los lenguajes internos es que merece la pena utilizarlos. Sin embargo, hay que esforzarse un poco para encontrar la mejor manera de configurar el lenguaje interno de un topos concreto. La idea general es introducir el menor número posible de tipos nuevos, caracterizarlos con axiomas adecuadamente elegidos y averiguar qué otros axiomas útiles son válidos en tu topos.

Answer 2

Una pregunta preciosa; ¡gracias!

Primero, también puedes coger Set y ver si su lógica booleana de dos valores ayuda de alguna manera a distinguir un conjunto finito (las definiciones varían) de uno infinito (las definiciones varían). No ayuda.

En Grph el clasificador de subobjetos es bastante sencillo, consta de dos vértices (T y F) y cinco flechas (dos triviales, una de T a F, una de F a T, y una de T a F, suplantando a aquellas flechas que se originan y terminan en un subgrafo, pero no pertenecen a él).

¿Qué puedes hacer con él? Casi nada. Hay exactamente cuatro topologías Grothendick en este topos, y eso es todo.