Las conexiones entre la teoría de las categorías y la lógica son múltiples y profundas. Sin embargo, no suelen girar directamente en torno a los fundamentos. La mayoría (¿todos?) los intentos de fundamentos categóricos no llegaron a ninguna parte, lo que no quiere decir que no produjeran nada. La mayor parte del interés en los fundamentos categóricos se ha centrado en topos fundamentos teóricos. El trabajo de Lambek en el topos gratuitos es un ejemplo. Para ser claros, la mayoría de los categoristas, como la mayoría de los matemáticos, no tienen un interés especial en los fundamentos, incluso los categoristas que se centran en la teoría de los topos que surgió de la geometría algebraica. La página de nLab sobre fundamentos de las matemáticas da una idea del sentimiento que tienen los categóricos hacia las fundaciones.
Volveré a los fundamentos dentro de un rato, pero me alejaré hacia las aplicaciones de la teoría de categorías. El libro de Jacobs Lógica categórica y teoría de tipos discute la maquinaria necesaria para conectar las categorías con la lógica. Correspondencia modular entre teorías de tipos dependientes y categorías que incluyen pretopoi y topoi sirve de referencia práctica para saber cómo explícitamente el lenguaje interno y lógica interna trabajo en varios ejemplos importantes. Esta página de nLab ofrece una visión rápida de alto nivel. La clave es que estas descripciones son bastante "modulares", lo que significa que en gran medida podemos mezclar y combinar las características lógicas que deseemos. Haces en Geometría y Lógica es un buen libro que introduce la teoría de los topos y cómo se conecta con (¡sorpresa!) la geometría y la lógica. Asume que tienes los fundamentos de la teoría de categorías, por ejemplo, como se obtiene del libro de Awodey.
Volviendo a los fundamentos, mientras que la teoría de las categorías sugiere algunos puntos de vista conceptuales/filosóficos como el principio de equivalencia que puede presentar las presentaciones habituales, al menos, de la teoría de conjuntos de forma negativa, en mi opinión, una de las formas más valiosas en que la teoría de categorías es útil para pensando en fundaciones es la plétora de modelos que ofrece. ¿Quiere explorar cómo es el mundo de las matemáticas si es finitista o predicativo o predicativo-finitista? Entonces tengo una pretopos para ti. O mejor, el lenguaje interno de una clase adecuada de pretopos. En una dirección diferente, Paul Cohen introdujo la técnica de forzando en su demostración de la independencia de la Hipótesis del Continuo. Categóricamente, el forzamiento corresponde a la construcción de categorías de láminas que pueden servir como modelos de ZFC. Esto se describe en el capítulo VI de Sheaves in Geometry and Logic. Los numerosos modelos de la teoría clásica de conjuntos que pueden producirse de este modo hicieron que Cohen cambiara su postura filosófica sobre las matemáticas.
La mayoría de estos modelos se presentan como modelos dentro de una potente teoría de conjuntos de fondo, por ejemplo Teoría de conjuntos Tarksi-Grothendieck Aunque esta teoría de conjuntos no suele articularse, sino que simplemente se asume que hay suficiente teoría de conjuntos para realizar las construcciones categóricas. Estos modelos suelen formularse como teorías de primer orden como la teoría de conjuntos ZFC o, alternativamente, pueden formularse directamente sistemas deductivos para los lenguajes internos, pero normalmente los categoristas se limitan a estudiar tipos de categorías y no intentan proponer un sistema fundacional.
1 votos
Podrías mirar la teoría de tipos de homotopía. Si tienes algún conocimiento de la teoría de la homotopía es una base alternativa interesante que también toma prestada mucha intuición de la teoría de categorías