| Autor(es) | Jean-Yves Girard (n. 1947) |
| Fecha / periodo | 1987 · Siglo XX · Francia |
| Tipo | Formal |
| Deriva de | Lógica intuicionista · Deducción natural y cálculo de secuentes |
| Derivan de ella | Lógica de la separación y lógica BI |
| Tres leyes | Identidad: ✓ (\(A \multimap A\); axioma \(\vdash A^\perp, A\)) · No contradicción: matizado (\(A \otimes A^\perp \multimap \bot\) vale; \(A \mathbin{\&} A^\perp\) no implica cualquier cosa) · Tercio excluso: matizado (vale el multiplicativo \(A \wp A^\perp\), no el aditivo \(A \oplus A^\perp\)) |
La lógica lineal nace de una observación sobre el cálculo de secuentes: las reglas estructurales de debilitamiento (añadir hipótesis que no se usan) y contracción (usar una hipótesis varias veces) son las que convierten las fórmulas en verdades eternas y reutilizables. Si se suprimen, las fórmulas se comportan como recursos: una hipótesis se consume exactamente una vez. Girard llegó a esta idea al analizar la semántica del Sistema F mediante espacios de coherencia, donde la implicación intuicionista se descompone en dos pasos: un operador que permite duplicar (\(!\)) y una implicación lineal (\(\multimap\)). El gesto distintivo es que, sin las reglas estructurales, cada conectiva clásica se desdobla en dos versiones, y el uso ilimitado vuelve a introducirse de forma controlada mediante modalidades. El resultado es una lógica que conserva la simetría de la clásica (negación involutiva, dualidades) y a la vez el contenido constructivo de la intuicionista.
Conectivas (Girard, «Linear logic», Theoretical Computer Science, 1987). Negación lineal \(A^\perp\). El «par» se escribe aquí \(\wp\).
Dualidades de De Morgan. \(A^{\perp\perp} = A\); \((A \otimes B)^\perp = A^\perp \wp B^\perp\); \((A \mathbin{\&} B)^\perp = A^\perp \oplus B^\perp\); \((!A)^\perp = ?A^\perp\); \(1^\perp = \bot\); \(\top^\perp = 0\).
Cálculo de secuentes unilateral (secuentes \(\vdash \Gamma\); solo vale el intercambio):
Debilitamiento y contracción solo se permiten sobre fórmulas marcadas con \(?\).
Traducción de Girard. La lógica intuicionista se incrusta fielmente: \((A \to B)^* = !A^* \multimap B^*\), \((A \land B)^* = A^* \mathbin{\&} B^*\), \((A \lor B)^* = !A^* \oplus !B^*\). La lógica clásica se incrusta también, con otras traducciones.
Qué se pierde. No valen \(A \multimap A \otimes A\) (no se duplica), \(A \otimes B \multimap A\) (no se descarta), ni \(A \otimes A^\perp \multimap B\) con \(B\) arbitrario. \(A \oplus A^\perp\) no es teorema.
Ejemplo (Girard). Con un euro (\(E\)) puedo comprar un café (\(C\)) o un té (\(T\)): \(E \multimap C \mathbin{\&} T\), y elijo yo. Si la máquina decide, \(E \multimap C \oplus T\). Con dos euros obtengo café y té: \(E \otimes E \multimap C \otimes T\). De \(E\) no se sigue \(E \otimes E\).
Metateoría.
La lógica lineal procede de la lógica intuicionista a través de la teoría de tipos: su origen está en la semántica del Sistema F, el cálculo lambda polimórfico de Girard (1972), que por la correspondencia de Curry y Howard corresponde a la lógica intuicionista de segundo orden. En los espacios de coherencia la función estable \(A \to B\) se factoriza como \(!A \multimap B\), y la lógica lineal hace explícita esa descomposición. Del cálculo de secuentes de Gentzen toma el marco: parte de LK, suprime el debilitamiento y la contracción y observa cómo se desdoblan las reglas de las conectivas según los contextos se compartan o se separen. De la lógica lineal procede la conjunción multiplicativa que la lógica BI de O’Hearn y Pym toma como conjunción separadora.
Las afinidades son más tardías. Con la lógica relevante comparte la restricción de reglas estructurales (la relevante suprime el debilitamiento pero conserva la contracción), y Arnon Avron («The semantics and proof theory of linear logic», 1988) estudió la relación. El cálculo de Lambek (1958) resultó ser un fragmento no conmutativo de la lógica lineal, relación reconocida después de 1987. Andreas Blass (1992) le dio una semántica de juegos en la tradición dialógica de Lorenzen.
La lógica lineal apareció en un momento en que la teoría de la demostración y la informática teórica convergían. Su lectura de las fórmulas como recursos la hizo útil para la concurrencia, los sistemas de tipos lineales y afines de los lenguajes de programación, la planificación y la lingüística computacional. Girard la presentó como una lógica «de la acción» más fina que la clásica y la intuicionista, no como una rival: ambas se incrustan en ella. Para la pregunta «¿una lógica o muchas?» es un caso central. Muestra que lógicas aparentemente incompatibles pueden ser fragmentos o traducciones de un marco más fino, y que las reglas estructurales, que la tradición daba por supuestas, son opciones con consecuencias. El pluralismo aparece aquí como pluralismo de reglas estructurales.