Semántica categorial explicó – ¿qué es interpretación?

Question

He sido realmente tener un tiempo difícil tratando de entender la semántica categórica. De hecho, estoy confundido hasta el punto de que tengo miedo de no saber cómo hacer esta pregunta!

He estado leyendo los libros de texto como Makkai y Reyes' libro de Jacobs Categórica de la lógica y de la teoría tipo (1992) o Categórica Lógica por Andrew Pitts, pero yo simplemente no puede obtener la sensación de ¿qué están tratando de hacer. Esta entrada y esta uno en la nlab no parecen ser muy útil para mi entendimiento. De hecho, parece que cuanto más leo más confundido que me pasa.

Puede que esas preguntas sean contestadas de cristal con claridad?

• Cómo se define una categoría de interpretación?

• Si es un functor, ¿cuál es su dominio? Es decir, en el modelo de la teoría, podemos interpretar lenguas. ¿Qué estamos interpretación de aquí, los idiomas o las teorías .. o algo más?

Permítanme un ejemplo: lo sé, muy informalmente, que intuitionistic lógica proposicional (IPL) corresponden a bicartesian categorías cerradas (BCC).

• Pero, ¿cómo hacer esta declaración matemáticamente exacta? ¿Cómo podemos definir como una interpretación?

Si es de hecho un functor, ¿cuál es su dominio? La categoría de intuitionistic proposicional de la lógica o de la categoría de intuitionistic proposicional idiomas? O incluso un particular intuitionistic lógica proposicional entendida como un categry (posiblemente dado por la categoría de pruebas)?

Realmente agradecería cualquier respuesta que podría arrojar algo de luz, no sólo en este ejemplo, pero también en el panorama de ti.

Antecedentes: creo tener todos los antecedentes en la categoría de teoría (UPs, natural de transformaciones, equivalencias, adjoints etc.) y el tipo de teoría (polimorfismo, dependiente de tipos, etc.), después de haber asistido a cursos en ambas disciplinas.

Answer 1

Hay (al menos) dos diferentes tipo de cosas que usted puede hacer, más o menos correspondiente a la sintaxis y la semántica.

---

Usted puede estudiar la lógica interna de una categoría, que permite el uso de una lógica del lenguaje como una práctica herramienta para hacer cálculos en una categoría. por ejemplo, los objetos son los tipos, las proposiciones son subobjetos, et cetera.

Por el contrario, dado un lenguaje adecuado, podemos construir su categoría sintáctica que consiste de todos los tipos que se pueden construir en el lenguaje y las funciones que se pueden definir entre ellos, y satisfacer todas las relaciones que pueden probar que tienen entre ellos. Y así podemos categoría de uso de la teoría para ayudarnos a pensar de tipo de teorías.

---

En la semántica lado podemos pensar en una categoría $T$ (posiblemente con extra de la estructura; por ejemplo, un boceto) como una teoría. A continuación, los modelos de esta teoría en una categoría $C$ será functors $F : T \to C$ de un cierto tipo.

---

Por supuesto, estos no son ajenos; si tenemos la teoría de un grupo, que se podría construir $T$ a su categoría sintáctica, y requieren de la functors la definición de modelos de $T$ a ser de las que se conserva la lógica que se utiliza.

Por el contrario, si estamos en el hábito de estudiar functors de alguna categoría $T$, puede ser vale la pena considerar la teoría dada por el lenguaje interno de $T$ y ver functors como modelos de la teoría.

Un tipo común de esta construcción es uno que podemos hacer con el álgebra universal (por ejemplo, la teoría de grupos, como las operaciones y ecuaciones). Si tenemos un poco de variedad de álgebra universal, podemos tomar $T$ a ser el opuesto de la categoría de finitely presentado álgebras y, a continuación, los modelos serán functors de $T$ que preservar límites finitos.