| Autor(es) | F. William Lawvere (1937–2023); Myles Tierney (1937–2017); Joachim Lambek (1922–2014); Philip J. Scott |
| Fecha / periodo | 1963–1986 · Siglo XX · Estados Unidos y Canadá |
| Tipo | Formal |
| Deriva de | Lógica dialéctica (n.º 53) · Lógica intuicionista · Cálculo lambda · Deducción natural y cálculo de secuentes · Lógica de orden superior y teoría simple de tipos |
| Derivan de ella | Teoría homotópica de tipos y fundamentos univalentes |
| Tres leyes | Identidad: ✓ (flecha identidad \(1_A : A \to A\)) · No contradicción: ✓ (\(\neg(A \land \neg A)\) vale en toda álgebra de Heyting) · Tercio excluso: matizado (vale solo en los topos booleanos, como el de los conjuntos) |
La lógica categórica reformula la lógica en el lenguaje de la teoría de categorías, en el que lo primario no son los elementos sino las flechas entre objetos y sus propiedades universales. Tiene dos caras. En una, un sistema deductivo es una categoría: las fórmulas son objetos, las pruebas son flechas y la composición de flechas es el encadenamiento de pruebas (Lambek). En la otra, cada categoría suficientemente rica tiene una lógica interna, y los conectivos y cuantificadores se definen por adjunciones (Lawvere). El resultado más llamativo es el topos elemental de Lawvere y Tierney (1969–1970): un universo en el que se puede hacer matemática y cuya lógica interna es, en general, intuicionista. Así, la lógica deja de ser un marco previo a los objetos matemáticos y pasa a depender del universo en el que se trabaja.
Conectivos como propiedades universales. En un retículo de subobjetos \(\mathrm{Sub}(X)\):
Cuantificadores como adjuntos (Lawvere, «Adjointness in foundations», 1969). Para una proyección \(\pi : X \times Y \to X\), la sustitución (imagen inversa) \(\pi^* : \mathrm{Sub}(X) \to \mathrm{Sub}(X \times Y)\) tiene adjuntos a ambos lados: \(\exists_\pi \dashv \pi^* \dashv \forall_\pi\). Es decir:
Son exactamente las reglas de introducción y eliminación de Gentzen. La igualdad y el esquema de comprensión también se obtienen como adjuntos (Lawvere, 1970, «hiperdoctrinas»).
Topos elemental. Una categoría con límites finitos, exponenciales \(B^A\) y un clasificador de subobjetos \(\Omega\) con una flecha \(\top : 1 \to \Omega\) tal que cada subobjeto (monomorfismo) \(A \to X\) es la imagen inversa de \(\top\) por una única \(\chi_A : X \to \Omega\). Entonces:
Correspondencia de Lambek. Lambek («Deductive systems and categories» I–III, 1968–1972) mostró que:
Correspondencias entre fragmentos lógicos y tipos de categorías. Lógica regular (\(\land, \exists, =\)): categorías regulares. Lógica coherente (añade \(\lor\)): categorías coherentes. Lógica de primer orden intuicionista: categorías de Heyting. Lógica de orden superior intuicionista: topos (Lambek y Scott, 1986). Cada teoría tiene una categoría clasificante y sus modelos son funtores que preservan la estructura: es la «semántica funtorial» de la tesis de Lawvere (1963) para teorías algebraicas.
Ejemplo. En los haces sobre un espacio \(X\), una proposición es un abierto \(U\). La negación es el interior del complemento. Para \(U = X \setminus \{p\}\), \(U \cup \neg U = U \neq X\): el tercio excluso falla. El valor de verdad mide dónde es verdadera una proposición.
La lógica categórica recibe de la lógica intuicionista su lógica interna: la de un topos es intuicionista y la semántica de haces generaliza las de Kripke y Beth. Del cálculo lambda y de la deducción natural y el cálculo de secuentes toma el material que Lambek traduce a categorías: el cálculo lambda tipado a categorías cartesianas cerradas y los sistemas de Gentzen a categorías con estructura (1968–1972). Con la lógica de orden superior la une el trabajo de Lambek y Scott, que muestra que los topos son los modelos de la teoría intuicionista de tipos. La filiación con la lógica dialéctica pasa por Lawvere, que ya en «Adjointness in foundations» (1969) y «Quantifiers and sheaves» (1970) presenta la adjunción como forma matemática de la «unidad de opuestos», y que en textos de 1991 y 1994 formaliza con funtores adjuntos la «unidad e identidad de opuestos» de la Ciencia de la lógica de Hegel. Hacia adelante, la teoría homotópica de tipos usa modelos categóricos (grupoides, conjuntos simpliciales, \(\infty\)-topos) para interpretar los tipos identidad.
Surgió en los años sesenta, en paralelo a la geometría algebraica de Grothendieck, cuyos topos (1962–1963) generalizaban los espacios. Lawvere y Tierney extrajeron de ellos una noción puramente lógica. En los setenta y ochenta se convirtió en el lenguaje común de la teoría de la prueba, la teoría de tipos y la semántica de los lenguajes de programación. Para la pregunta «¿una lógica o muchas?», su aportación es decisiva: cada topos tiene su propia lógica interna, y la lógica clásica es la de un caso particular, el booleano. La lógica aparece ligada al universo de discurso. No se elige en abstracto, sino junto con los objetos sobre los que se razona.