| Autor(es) | Joachim Lambek (1922–2014); Kosta Došen (1954–2017); Peter Schroeder-Heister (n. 1953) |
| Fecha / periodo | 1958–1993 · Siglo XX · Canadá y Europa |
| Tipo | Formal |
| Deriva de | Sistemas de Leśniewski · Deducción natural y cálculo de secuentes · Lógica relevante |
| Derivan de ella | Lógica natural y lógica de términos · Lógica de la separación y lógica BI |
| Tres leyes | Identidad: ✓ (el axioma \(A \Rightarrow A\) se conserva en todas) · No contradicción: no tematizado en el cálculo de Lambek, sin negación; en las demás varía (la explosión requiere debilitamiento) · Tercio excluso: no tematizado en Lambek; varía según las reglas estructurales y el tipo de negación |
En el cálculo de secuentes de Gentzen hay dos clases de reglas: las lógicas, que introducen conectivas, y las estructurales, que manipulan las premisas sin mirar su forma. Estas últimas dicen que el orden de las premisas no importa (intercambio), que una premisa puede usarse varias veces (contracción) y que se pueden añadir premisas ociosas (debilitamiento). Las lógicas subestructurales suprimen o restringen alguna de ellas. El gesto distintivo es tratar las reglas estructurales como parámetros: se dejan fijas las reglas de las conectivas y se varían las estructurales, y cada elección da una lógica. Las premisas pasan a ser algo más fino que un conjunto: una secuencia, un multiconjunto o una estructura con agrupaciones.
Reglas estructurales (para secuentes \(\Gamma \Rightarrow C\)):
Cálculo de Lambek L («The Mathematics of Sentence Structure», 1958). Tipos construidos a partir de tipos básicos (\(s\), oración; \(n\) o \(np\), nombre) con tres conectivas:
Reglas (con \(\Gamma\) no vacío):
L no tiene ninguna regla estructural, ni siquiera el intercambio, por eso distingue dos implicaciones, \(/\) y \(\backslash\). Lambek probó la eliminación del corte, de lo que se sigue la decidibilidad.
Ejemplo. «Juan ama a María»: \(np, (np \backslash s)/np, np \Rightarrow s\). Se deriva aplicando dos veces las reglas izquierdas: el verbo toma el objeto a la derecha y después el sujeto a la izquierda. La elevación de tipo \(np \Rightarrow s / (np \backslash s)\) es derivable: un nombre puede funcionar como algo que busca un predicado.
Resultados. Pentus (1993) probó que las gramáticas de Lambek generan exactamente los lenguajes independientes del contexto, lo que confirmaba una conjetura de Chomsky (1963). Pentus (2006) probó que la derivabilidad en L es NP-completa.
El mapa subestructural. Añadiendo reglas estructurales al cálculo de Lambek se obtiene una jerarquía:
Consecuencias de la supresión.
Semántica algebraica. Retículos residuados: un monoide con un orden y operaciones \(/\) y \(\backslash\) tales que \(a \bullet b \leq c\) si y solo si \(a \leq c / b\) si y solo si \(b \leq a \backslash c\). Las reglas estructurales corresponden a condiciones sobre el monoide: conmutatividad, idempotencia, integralidad.
Lambek formuló su cálculo para dar forma deductiva a la gramática categorial de Ajdukiewicz (1935), que a su vez procedía de las categorías semánticas de Leśniewski; y lo formuló en el marco del cálculo de secuentes de Gentzen, cuyo teorema de eliminación del corte reprodujo para un sistema sin reglas estructurales. La lógica relevante entró en el campo cuando se la reinterpretó como lógica sin debilitamiento. Las tres líneas (Lambek, relevancia, BCK) se desarrollaron con independencia; lo que las unifica es la perspectiva estructural que Došen formuló en el congreso de Tubinga de 1990 y que el volumen de 1993 consolidó.
Del marco subestructural derivan desarrollos concretos. Sánchez Valencia construyó su marcación de monotonía para la lógica natural sobre la gramática de Lambek. La lógica BI de O’Hearn y Pym es una lógica subestructural de recursos, base de la lógica de la separación. La relación con la lógica lineal es de afinidad reconocida después: el cálculo de Lambek es un fragmento no conmutativo de la lógica lineal, pero eso se vio tras la aparición de esta en 1987.
La idea de que las reglas estructurales son parámetros cambió la manera de comparar lógicas. Clásica, intuicionista, relevante, lineal y de Lambek dejaron de ser rivales sin relación y pasaron a ser puntos de un mismo mapa. Las aplicaciones van de la lingüística computacional a la gestión de recursos en informática y a las teorías de la verdad sin contracción. Para la pregunta «¿una lógica o muchas?», este es quizá el argumento más fuerte a favor de la pluralidad: las reglas de las conectivas pueden mantenerse fijas y, aun así, la noción de consecuencia varía según cómo se traten las premisas. La pregunta pasa a ser qué estructura tienen las premisas en cada dominio: conjuntos de hipótesis, recursos que se consumen, palabras en orden.