La lógica no conmutativa es una extensión de la lógica lineal que combina los conectivos conmutativos de la lógica lineal con los conectivos multiplicativos no conmutativos del cálculo de Lambek . Su cálculo secuencial se basa en la estructura de variedades de orden (una familia de órdenes cíclicos que pueden considerarse como una especie de estructura ), y el criterio de corrección para sus redes de prueba se da en términos de permutaciones parciales . También tiene una semántica denotacional en la que las fórmulas se interpretan mediante módulos sobre algunas álgebras de Hopf específicas .
Por extensión, el término lógica no conmutativa también es utilizado por varios autores para referirse a una familia de lógicas subestructurales en las que la regla de intercambio es inadmisible . El resto de este artículo está dedicado a una presentación de esta aceptación del término.
La lógica no conmutativa más antigua es el cálculo de Lambek , que dio origen a la clase de lógicas conocidas como gramáticas categoriales . Desde la publicación de la lógica lineal de Jean-Yves Girard se han propuesto varias lógicas no conmutativas nuevas, a saber, la lógica lineal cíclica de David Yetter, la lógica pomset de Christian Retoré y las lógicas no conmutativas BV y NEL.
La lógica no conmutativa se denomina a veces lógica ordenada, ya que es posible con la mayoría de las lógicas no conmutativas propuestas imponer un orden total o parcial a las fórmulas en las secuencias. Sin embargo, esto no es totalmente general, ya que algunas lógicas no conmutativas no admiten dicho orden, como la lógica lineal cíclica de Yetter. Aunque la mayoría de las lógicas no conmutativas no permiten el debilitamiento o la contracción junto con la no conmutatividad, esta restricción no es necesaria.
Joachim Lambek propuso la primera lógica no conmutativa en su artículo de 1958 Matemáticas de la estructura de la oración para modelar las posibilidades combinatorias de la sintaxis de los lenguajes naturales . [1] Su cálculo se ha convertido así en uno de los formalismos fundamentales de la lingüística computacional .
David N. Yetter propuso una regla estructural más débil en lugar de la regla de intercambio de la lógica lineal, lo que dio como resultado la lógica lineal cíclica. [2] Las secuencias de la lógica lineal cíclica forman un ciclo y, por lo tanto, son invariantes bajo rotación, donde las reglas multipremisas unen sus ciclos en las fórmulas descritas en las reglas. El cálculo admite tres modalidades estructurales, una modalidad autodual que permite el intercambio, pero sigue siendo lineal, y las exponenciales habituales (? y !) de la lógica lineal, lo que permite que las reglas estructurales no lineales se utilicen junto con el intercambio.
La lógica de Pomset fue propuesta por Christian Retoré en un formalismo semántico con dos operadores secuenciales duales que existían junto con el producto tensorial habitual y los operadores par de la lógica lineal, la primera lógica propuesta para tener operadores conmutativos y no conmutativos. [3] Se dio un cálculo secuencial para la lógica, pero carecía de un teorema de eliminación de corte ; en cambio, el sentido del cálculo se estableció a través de una semántica denotacional.
Alessio Guglielmi propuso una variación del cálculo de Retoré, BV, en la que las dos operaciones no conmutativas se colapsan en un único operador autodual, y propuso un nuevo cálculo de demostración, el cálculo de estructuras , para dar cabida al cálculo. La principal novedad del cálculo de estructuras fue su uso generalizado de la inferencia profunda , que se argumentó que es necesaria para los cálculos que combinan operadores conmutativos y no conmutativos; esta explicación coincide con la dificultad de diseñar sistemas secuentes para la lógica de pomsets que tienen eliminación de cortes.
Lutz Straßburger ideó un sistema relacionado, NEL, también en el cálculo de estructuras en el que la lógica lineal con la regla de mezcla aparece como un subsistema.
Las estructuras son un enfoque de la semántica de la lógica que se basa en la generalización de la noción de secuente siguiendo las líneas de las especies combinatorias de Joyal , lo que permite el tratamiento de lógicas drásticamente no estándar que las descritas anteriormente, donde, por ejemplo, el "," del cálculo secuente no es asociativo .