Lógica categórica

Lógica categórica es la rama de las matemáticas en la que las herramientas y conceptos de la teoría de categorías se aplican al estudio de la lógica matemática. También se destaca por sus conexiones con la informática teórica. 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 construcciones lógicas y de teoría de tipos. El tema ha sido reconocible en estos términos desde alrededor de 1970.

Descripción general

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

Semántica cagorística

La lógica cateórica introduce la noción de estructura valorada en una categoría C con la noción teórica modelo clásico de una estructura que aparece en el caso particular donde C es la categoría de conjuntos y funciones. Esta noción ha resultado útil cuando la noción teórica de un modelo carece de generalidad y/o es inconveniente. R.A.G. El modelado 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 conectores de la lógica pre-categorical se entendían más claramente utilizando el concepto de functor adjunto, y que los cuantificadores también se entendían mejor usando functores adjuntos.

Idiomas internos

Esto se puede ver como una formalización y generalización de la prueba por el persiguiendo diagramas. Uno define un lenguaje interno adecuado que nombra a los constituyentes pertinentes de una categoría, y luego aplica semántica categórica para convertir las afirmaciones en una lógica sobre el lenguaje interno en las correspondientes declaraciones categóricas. Esto ha sido más exitoso en la teoría de los topos, donde el lenguaje interno de un topos junto con la semántica de la lógica de orden superior intuitionista en un topos permite razonar sobre los objetos y morfismos de un topos "como si fueran conjuntos y funciones". Esto ha tenido éxito en tratar con topos que tienen "sets" con propiedades incompatibles con la lógica clásica. Un ejemplo principal es el modelo de Dana Scott de cálculo de lambda sin tipo en términos de objetos que retraen a su propio espacio de función. Otro es el modelo Moggi-Hyland del sistema F por una subcategoría completa interna de los topos efectivos de Martin Hyland.

Construcciones Term-model

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 y casos de un tipo adecuado de categoría. Un ejemplo clásico es la correspondencia entre las teorías de la lógica ecuatoriana de la beta y las categorías cerradas cartesianas. Categorías que surgen de teorías a través de construcciones a plazo pueden caracterizarse normalmente hasta la equivalencia por una propiedad universal adecuada. Esto ha permitido pruebas de propiedades meta-teóricas de algunas lógicas por medio de un álgebra categórica apropiada. Por ejemplo, Freyd dio una prueba de las propiedades de disyunción y existencia de la lógica intuitionista de esta manera.