Hispanopedia Wiki
Articulo de referencia

Lógica categórica

La lógica categórica es la rama de las matemáticas que aplica herramientas y conceptos de la teoría de categorías al estudio de la lógica matemática . También destaca por sus co...

Hispanopedia WikiContenido en espanolLectura gratuita

La lógica categórica es la rama de las matemáticas que aplica herramientas y conceptos de la teoría de categorías al estudio de la lógica matemática . También destaca 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 functor . El marco categórico proporciona un rico trasfondo conceptual para las construcciones lógicas y de teoría de tipos . Esta disciplina se conoce desde aproximadamente 1970.

Descripción general

En el enfoque categórico de la lógica existen tres temas importantes :

Semántica categórica
La lógica categórica introduce la noción de estructura valorada en una categoría C, donde la noción clásica de estructura propia de la teoría de modelos aparece en el caso particular en que C es la categoría de conjuntos y funciones . Esta noción ha demostrado ser útil cuando la noción de modelo propia de la teoría de conjuntos carece de generalidad o resulta inconveniente. La modelización que hace RAG Seely de diversas teorías impredicativas , como el Sistema F , es un ejemplo de la utilidad de la semántica categórica.
Se encontró que los conectores de la lógica precategórica se entendían más claramente utilizando el concepto de functor adjunto , y que los cuantificadores también se entendían mejor utilizando functores adjuntos. [ 2 ]
Lenguas internas
Esto puede verse como una formalización y generalización de la prueba por diagrama . 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 enunciados categóricos correspondientes. Esto ha tenido más éxito en la teoría de los 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 tenido éxito al tratar con topos que tienen "conjuntos" con propiedades incompatibles con la lógica clásica . Un ejemplo principal es el modelo de Dana Scott del cálculo lambda sin tipos en términos de objetos que se retraen en 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 de dicha lógica e instancias de un tipo de categoría apropiado. Un ejemplo clásico es la correspondencia entre teorías de la lógica ecuacional βη sobre el cálculo lambda simplemente tipado y categorías cartesianas cerradas . Las categorías que surgen de teorías mediante construcciones de modelos de términos generalmente pueden caracterizarse, salvo equivalencia , por una propiedad universal adecuada . Esto ha permitido demostrar propiedades metateóricas de algunas lógicas mediante un álgebra categórica apropiada . Por ejemplo, Freyd demostró de esta manera las propiedades de disyunción y existencia de la lógica intuicionista .

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 se relaciona con la categoría de teorías en esa lógica mediante una adjunción, donde los dos functores de la adjunción proporcionan, por un lado, el lenguaje interno de una categoría estructurada y, por otro, el modelo de términos de una teoría.

Véase también

Notas

  1. ↑ Goguen, Joseph; Mossakowski, Till; de Paiva, Valeria; Rabe, Florian; Schröder, Lutz (2007). "Una visión institucional de la lógica categórica" ​​(PDF) . 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). Lógica y métodos 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. North-Holland. ISBN 978-0-444-51621-3.
  • Kent, Allen; Williams, James G. (1990). Enciclopedia de Ciencias de la Computación y Tecnología . Marcel Dekker. ISBN 0-8247-2272-8.
  • Barr, M.; Wells , C. (1996). Teoría de categorías para la informática (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 fundamentales

  • 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 .   

Lecturas adicionales

  • 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 en matemáticas avanzadas. Vol.  7. Cambridge University Press. ISBN 978-0-521-35653-4.Introducción bastante accesible, aunque algo anticuada. El enfoque categórico de las 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 en lógica y fundamentos de las matemáticas. Vol.  141. North Holland, Elsevier. ISBN 0-444-50170-3.Una monografía exhaustiva escrita por un informático; abarca tanto la lógica de primer orden como la de orden superior, así como los tipos polimórficos y dependientes. Se centra en la categoría fibrada como herramienta universal en la lógica categórica, necesaria para abordar los 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. pp. 279–361 . ISBN  978-1-4020-3091-8.Versión disponible en línea en la página web 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" . Apuntes de clase .
  • Lurie, Jacob . "Lógica categórica (278x)" . Apuntes de clase .