Lógica categórica

La lógica categórica es la rama de las matemáticas en la que se aplican herramientas y conceptos de la teoría de categorías al estudio de la lógica matemática . También es notable por sus conexiones con la informática teórica . ^[1] En términos generales, la lógica categórica representa tanto la sintaxis como la semántica mediante una categoría y una interpretación mediante un funtor . El marco categórico proporciona un rico trasfondo conceptual para las construcciones lógicas y de teoría de tipos . El tema ha sido reconocible en estos términos desde aproximadamente 1970.

Descripción general

Hay tres temas importantes en el enfoque categórico de la lógica:

Semántica categórica

La lógica categórica introduce la noción de estructura valorada en una categoría C con la noción clásica de teoría de modelos de una estructura que aparece en el caso particular donde C es la categoría de conjuntos y funciones . Esta noción ha demostrado ser útil cuando la noción de teoría de conjuntos de un modelo carece de generalidad y/o es inconveniente. El modelado de RAG Seely de varias teorías impredicativas , como el Sistema F , es un ejemplo de la utilidad de la semántica categórica.

Se encontró que los conectivos de la lógica precategórica se entendían más claramente usando el concepto de functor adjunto , y que los cuantificadores también se entendían mejor usando functores adjuntos. ^[2]

Idiomas internos

Esto puede verse como una formalización y generalización de la prueba mediante la búsqueda de diagramas . Se define un lenguaje interno adecuado que nombra los constituyentes relevantes de una categoría y luego se aplica la semántica categórica para convertir las afirmaciones en una lógica sobre el lenguaje interno en declaraciones categóricas correspondientes. Esto ha sido más exitoso en la teoría de topos , donde el lenguaje interno de un topos junto con la semántica de la lógica intuicionista de orden superior en un topos permite razonar sobre los objetos y morfismos de un topos como si fueran conjuntos y funciones. ^[3] Esto ha sido exitoso al tratar con topos que tienen "conjuntos" con propiedades incompatibles con la lógica clásica . Un excelente ejemplo es el modelo de cálculo lambda no tipificado de Dana Scott en términos de objetos que se retraen sobre su propio espacio de funciones . Otro es el modelo de Moggi -Hyland del sistema F por una subcategoría completa interna del topos efectivo de Martin Hyland .

Construcciones de modelos de términos

En muchos casos, la semántica categórica de una lógica proporciona una base para establecer una correspondencia entre teorías en la lógica e instancias de un tipo apropiado de categoría. Un ejemplo clásico es la correspondencia entre teorías de la lógica ecuacional βη sobre el cálculo lambda de tipos simples y las categorías cerradas cartesianas . Las categorías que surgen de las teorías a través de construcciones de modelos de términos generalmente se pueden caracterizar hasta la equivalencia por una propiedad universal adecuada . Esto ha permitido pruebas de propiedades metateóricas de algunas lógicas por medio de un álgebra categórica apropiada . Por ejemplo, Freyd proporcionó una prueba de las propiedades de disyunción y existencia de la lógica intuicionista de esta manera.

Estos tres temas están relacionados. La semántica categórica de una lógica consiste en describir una categoría de categorías estructuradas que está relacionada con la categoría de teorías en esa lógica mediante una adjunción, donde los dos funtores en la adjunción dan el lenguaje interno de una categoría estructurada por un lado, y el modelo de término de una teoría por el otro.

Véase también

• Historia de la teoría de topos
• Topografía coherente

• Portal de matemáticas

Notas

1. Goguen, Joseph; Mossakowski, Till; de Paiva, Valeria; Rabe, Florian; Schroder, Lutz (2007). "Una visión institucional sobre la lógica categórica". Revista internacional de software e informática . 1 (1): 129–152. CiteSeerX 10.1.1.126.2361 . 
2. Lawvere 1971, Cuantificadores y haces
3. Aluffi 2009

Referencias

Libros

• Abramsky, Samson; Gabbay, Dov (2001). Métodos lógicos y algebraicos . Manual de lógica en informática. Vol. 5. Oxford University Press. ISBN 0-19-853781-6.
• Aluffi, Paolo (2009). Álgebra: Capítulo 0 (1.ª ed.). American Mathematical Society. pp. 18–20. ISBN 978-1-4704-1168-8.
• Gabbay, DM; Kanamori, A.; Woods, J., eds. (2012). Conjuntos y extensiones en el siglo XX. Manual de historia de la lógica. Vol. 6. Holanda Septentrional. ISBN 978-0-444-51621-3.

• Kent, Allen; Williams, James G. (1990). Enciclopedia de informática y tecnología . Marcel Dekker. ISBN 0-8247-2272-8.
• Barr, M. y Wells, C. (1996). Teoría de categorías para la ciencia de la computación (2.ª ed.). Prentice Hall. ISBN 978-0-13-323809-9.
• Lambek, J. ; Scott, PJ (1988). Introducción a la lógica categórica de orden superior. Estudios de Cambridge en matemáticas avanzadas. Vol. 7. Cambridge University Press. ISBN 978-0-521-35653-4.
• Lawvere, FW ; Rosebrugh, R. (2003). Conjuntos para matemáticas. Cambridge University Press. ISBN 978-0-521-01060-3.
• Lawvere, FW; Schanuel, SH (2009). Matemáticas conceptuales: una primera introducción a las categorías (2.ª ed.). Cambridge University Press. ISBN 978-1-139-64396-2.

Artículos seminales

• Lawvere, FW (noviembre de 1963). "Semántica funcional de las teorías algebraicas". Actas de la Academia Nacional de Ciencias . 50 (5): 869–872. Bibcode :1963PNAS...50..869L. doi : 10.1073/pnas.50.5.869 . JSTOR  71935. PMC  221940 . PMID  16591125.
• — (Diciembre de 1964). "Teoría elemental de la categoría de conjuntos". Actas de la Academia Nacional de Ciencias . 52 (6): 1506–11. Bibcode :1964PNAS...52.1506L. doi : 10.1073/pnas.52.6.1506 . JSTOR  72513. PMC  300477 . PMID  16591243.
• — (1971). "Cuantificadores y gavillas". Actes: Du Congres International Des Mathematiciens Niza 1-10 de septiembre de 1970. Pub. Sous La Direction Du Comité D'organization Du Congres . Gauthier-Villars. págs. 1506–11. OCLC  217031451. Zbl  0261.18010.

Lectura adicional

• Makkai, Michael ; Reyes, Gonzalo E. (1977). Lógica categórica de primer orden. Lecture Notes in Mathematics. Vol. 611. Springer. doi :10.1007/BFb0066201. ISBN 978-3-540-08439-6.
• Lambek, J.; Scott, PJ (1988). Introducción a la lógica categórica de orden superior. Estudios de Cambridge sobre matemáticas avanzadas. Vol. 7. Cambridge University Press. ISBN 978-0-521-35653-4.Introducción bastante accesible, pero algo anticuada. El enfoque categórico para lógicas de orden superior sobre tipos polimórficos y dependientes se desarrolló en gran medida después de la publicación de este libro.
• Jacobs, Bart (1999). Lógica categórica y teoría de tipos. Estudios de lógica y fundamentos de las matemáticas. Vol. 141. North Holland, Elsevier. ISBN 0-444-50170-3.Una monografía completa escrita por un científico informático; cubre tanto la lógica de primer orden como la de orden superior, y también los tipos polimórficos y dependientes. El enfoque se centra en la categoría fibrosa como herramienta universal en lógica categórica, que es necesaria para tratar con tipos polimórficos y dependientes.
• Bell, John Lane (2001). "El desarrollo de la lógica categórica". En Gabbay, DM; Guenthner, Franz (eds.). Manual de lógica filosófica . Vol. 12 (2.ª ed.). Springer. págs. 279–361. ISBN. 978-1-4020-3091-8.Versión disponible en línea en la página de inicio de John Bell.
• Marqués, Jean-Pierre; Reyes, Gonzalo E. "La Historia de la Lógica Categórica 1963-1977". Gabbay, Kanamori y Woods 2012 . págs. 689–800.
  Una versión preliminar.
• Awodey, Steve (12 de julio de 2024). "Lógica categórica". notas de clase .
• Lurie, Jacob . "Lógica categórica (278x)". notas de clase .