Desde un punto de vista formal es posible estudiar la teoría de las categorías dentro de la teoría de las categorías, utilizando la noción de topos . La teoría de los topos hace muchas cosas, pero una de ellas es un fundamento alternativo de la teoría de las categorías para las matemáticas.
Aumentando la teoría de los topos con suficientes axiomas adicionales, es teóricamente posible reconstruir toda la ZFC dentro de la teoría de los topos. Así, si alguien puede estudiar la teoría de categorías en ZFC, puede hacer lo mismo estudiando la teoría de categorías dentro de ZFC dentro de la teoría de topos. O puede estudiar la teoría de las categorías utilizando la teoría de los topos sin utilizar ZFC como paso intermedio. Un reto práctico para hacer esto es que los axiomas para un topos son posiblemente más complicado que el axiomas para ZFC que, aparte de la sustitución, pueden justificarse en términos de propiedades relativamente básicas de los conjuntos.
Otra forma de analizar algunas cuestiones planteadas en este hilo es considerar la noción de tipo . Hay una bonita analogía para la diferencia entre ZFC y algunos fundamentos categóricos: es como la diferencia entre un lenguaje de programación no tipado (como Esquema ) y un lenguaje fuertemente tipado (como Java o C++).
En Scheme y otros lenguajes no tipados, no hay separación entre el código y los datos: dados dos objetos cualesquiera, podemos tratar el primero como una función y el segundo como una entrada, e (intentar) calcular la salida correspondiente. Así, por ejemplo, podríamos definir los números naturales utilizando Números de la Iglesia , tratar " $5$ " como una función, y calcular su valor en el par ordenado $(0,17)$ . Por supuesto, nadie hace esto en serio en la práctica. Del mismo modo, en ZFC, podemos preguntarnos si el $\pi$ es un miembro del par ordenado $(8, \mathbb{R})$ Aunque en la práctica nadie lo hace en serio.
En Java y C++, existen definiciones estrictas de cada tipo de datos. Por ejemplo, si tengo un objeto "número natural" y quiero un objeto "número real", tengo que convertir ("cast") el objeto original para que tenga el tipo apropiado. Por lo tanto, no puedo añadir directamente $1_\mathbb{N}$ y $\pi_\mathbb{R}$ . Esto es similar a la forma en que algunas fundaciones categóricas manejan las cosas. En lugar de hablar de "reparto", estas fundaciones se centran en el "mapa de inclusión natural" de $\mathbb{N}$ a $\mathbb{R}$ etc.
Conviene saber que existen muchas otras teorías de tipos, además de las inspiradas en la teoría de los topos. Hay teoría de tipos intuicionista que es muy potente, y clásico aritmética de segundo orden que es mucho más débil pero que sigue siendo capaz de formalizar casi toda la matemática de grado.
Creo, al igual que muchos que trabajan en los fundamentos de las matemáticas, que la matemática informal ingenua que se encuentra en la práctica se realiza en algún tipo de teoría de tipos complicada (e informal). Esto hace que los fundamentos de la teoría de tipos sean mucho más naturales para muchos matemáticos -muchas de las objeciones presentadas a ZFC se basan en la falta de tipificación en la teoría de conjuntos. Los fundamentos teóricos de tipos simples serían posiblemente un sistema formal más natural que ZFC para muchos propósitos prácticos, al igual que Java es un lenguaje más práctico que Scheme para muchos propósitos.
Por otro lado, la falta de tipado en ZFC, al igual que la falta de tipado en Scheme, es útil para muchos propósitos teóricos, por lo que es bueno para los matemáticos ser conscientes de los sistemas no tipados también. Por ejemplo, para hacer un modelo de ZFC sólo necesitamos definir una relación indefinida, $\in$ . Para hacer un modelo de la teoría de tipos tenemos que diseñar el sistema de tipos, luego diseñar un dominio para cada tipo, y también diseñar todos los mapas entre tipos y operaciones en cada tipo individual. Esto es mucho más complicado. De forma análoga, es un ejercicio común en las clases de informática pedir a los estudiantes que escriban un intérprete de Scheme, o incluso que escriban un compilador de Scheme en lenguaje ensamblador, pero no es común pedir a los estudiantes que escriban un intérprete completo de Java en Java, y mucho menos en lenguaje ensamblador.
12 votos
Lo que Mac Lane intenta decir, en un lenguaje más técnico, es que las (meta)categorías son modelos de una determinada teoría de primer orden. Sin embargo, a continuación dice que trabajará principalmente con categorías que existen realmente dentro del universo de la teoría de conjuntos.
4 votos
ZFC es una teoría de árboles bien fundados, enraizados y rígidos; hay mucha estructura interna en los conjuntos ZFC que no necesariamente queremos.
2 votos
La paradoja de Russell también ocurre en la TC. Y, de forma independiente, se puede tomar la TC como formalización de base e incrustar en ella la teoría de conjuntos (de forma similar a la situación inversa habitual para que la gente entienda la teoría de categorías, empezando por enunciar la TC en términos de establece de objetos, morfismo, etc.)
2 votos
Estimado @DVD: el comentario sobre las incrustaciones en $R^3$ parece no entender el sentido de la pregunta. Este PO es sobre una preocupación seria por formalización desde la base . Entonces su sugerencia de tomar subconjuntos de $R^3$ como las 'primitivas' no es una opción, ya que la construcción de ' $R$ ', que supuestamente debe significar 'los' números reales, es en sí mismo problemático. Y si su sugerencia es basarse en algún "espacio subjetivamente [...] real", entonces esto no es 'matemáticas' como se suele interpretar hoy en día, aunque sólo sea por el hecho empírico de que las opiniones están divididas sobre si el espacio euclidiano es 'el' espacio 'real'.