El lenguaje de Mitchell y Bénabou

En esta sección veremos cómo se interpretan los símbolos de un lenguaje de primer orden en un topos arbitrario \(\mathcal{E}\).

La primera observación es que el lenguaje no es como en lo cursos de lógica donde sólo hay un tipo de variable que se interpreta como un elemento en un conjunto. Nuestro lenguaje se parece al de los espacios vectoriales, en este hay dos tipos de variable, una para hablar de vectores y otra para hablar de escalares. Con esto debe haber dos conjuntos deferentes para interpretar cada tipo de variable.

En un topos \(\mathcal{E}\) cada objeto \(E\) servirá como un tipo de variable. Más precisamente, el lenguaje que estamos haciendo tiene tantos tipos de variable como objetos tenga el topos y la interpretación de una variable será una flecha con codominio adecuado.

Para cada objeto \(X\in\mathcal{E}\) tenemos una cantidad numerable de variables de tipo \(X\), que denotamos \(x_1,x_2,\ldots\). Cada una de ellas se interpreta como la flecha identidad \(id_X\colon X\to X\). La razón por la cual toda se interpretan como la identidad es que, cuando formemos el término \(f(x)\) de tipo \(Y\) para una flecha \(f\colon X\to Y\), si \(x\) no se interpretara como la identidad, entonces la composición \(X\to X\to Y\) no terminaría en \(f(x)\) (pensar esto en conjuntos, con funciones y elementos).

Luego, si tenemos variables \(x_i\) de tipo \(X_i\) y \(f\colon X_1\times\cdots\times X_n\to Y\) es una flecha en \(\mathcal{E}\), entonces tenemos el término \(f(x_1,\ldots,x_n)\) de tipo \(Y\) cuya interpretación es \(f\). Aquí hay que recordar que las variables se interpretan como la identidad. Si ahora tenemos términos \(\sigma_i\) de tipo \(X_i\), entonces también podemos formar el término \(f(\sigma_1,\ldots,\sigma_n)\). Este término se interpreta como la composición \[S_1\times\cdots\times S_n\xrightarrow{\sigma_1\times\cdots\times\sigma_n}X_1\times\cdots\times X_n \xrightarrow{f}Y\]

En general, los tipos de las variables libres de un término forman al dominio de la interpretación. Por lo tanto, un término de tipo \(X\) sin variables libres, como una constante, se interpreta como una flecha \(1\to X\).

Como un topos es una categoría cartesiana cerrada, entonces hay una biyección entre flechas de la forma \(X\times Y\to Z\) y de la forma \(Y\to Z^X\). Esta biyección nos permite formalizar la abstracción \(\lambda\) en un topos. Esto es, dado un término \(\sigma\colon X\times Y\to Z\) de tipo \(Z\) (con dos variables libres) podemos inducir un término \(\lambda x\sigma\colon Y\to Z^X\) de tipo \(Z^X\) (con una variable libre).

Otros términos especiales son aquellos de tipo \(\Omega\). Este tipo de términos recibirán el nombre de fórmulas. Antes hemos visto algunas fórmulas especiales en un topos. Por ejemplo, la delta de Kronecker \(\delta_X\colon X\times X\to\Omega\) es la fórmula que dice cuando dos términos de tipos \(X\) son iguales. Así, hay una igualdad para cada tipo de variable y no una igualdad global. El tercer axioma de un topos da la fórmula de pertenencia \(\in_X\colon X\times PX\to\Omega\).

La estructura de álgebra de Heyting interna del clasificador de subobjetos permite aplicar conectivos a fórmulas. Por ejemplo, si \(\varphi(x),\psi(x)\colon X\to\Omega\), entonces la conjunción de estas fórmulas es la composición \[X\xrightarrow{(\varphi(x),\psi(x))}\Omega\times\Omega\xrightarrow{\land}\Omega\]

El resto de los conectivos se obtiene de forma análoga.

Sabemos que si \(f\colon A\to B\) es una flecha en \(\mathcal{E}\) entonces la imagen inversa \(f^{-1}\colon Sub(B)\to Sub(A)\) tiene adjuntos derecho e izquierdo, denotados \(\forall_f\) y \(\exists_f\), respectivamente. Luego, ya vimos que estos adjuntos se pueden internalizar de forma que \(Pf\colon PB\to PA\) tiene adjuntos derecho e izquierdo, con la misma notación que antes. Si en particular tomamos la única flecha \(X\to 1\) y recordamos que \(P1=\Omega\), entonces \(P!\colon\Omega\to PX\) tiene adjuntos derecho \(\forall\colon PX\to\Omega\) e izquierdo \(\exists\colon PX\to\Omega\).

Sea \(\varphi(x,y)\colon X\times Y\to\Omega\) una fórmula con dos variables libres. La interpretación de la fórmula \(\forall x\varphi(x,y)\) es la composición \[Y\xrightarrow{\lambda x\varphi(x,y)}\Omega^X=PX\xrightarrow{\forall}\Omega\]

El cuantificador existencial es análogo a lo que hemos hecho.

Ahora ya hemos interpretado todo el lenguaje de primer orden en un topos. Además, también tenemos la interpretación de la igualdad y la pertenencia. Por lo tanto, podemos desarrollar una teoría de conjuntos interna a un topos arbitrario. Es claro que no obtendremos algo igual a ZFC ya que en un topos, en general, la lógica interna es intuicionista.

Como ahora tenemos una teoría de conjuntos interna es posible imaginar que los objetos tienen elementos y denotar con \(\{x\mid\varphi(x)\}\) al producto fibrado de \(v\colon 1\to\Omega\) a lo largo de \(\varphi(x)\colon X\to\Omega\).