Lógica não comutativa - Noncommutative logic
A lógica não comutativa é uma extensão da lógica linear que combina os conectivos comutativos da lógica linear com os conectivos multiplicativos não comutativos do cálculo de Lambek . Seu cálculo sequente depende da estrutura de variedades de ordem (uma família de ordens cíclicas que podem ser vistas como uma espécie de estrutura ), e o critério de correção para suas redes de prova é dado em termos de permutações parciais . Ele também tem uma semântica denotacional na qual as fórmulas são interpretadas por módulos sobre algumas álgebras de Hopf específicas .
Não comutatividade na lógica
Por extensão, o termo lógica não comutativa também é usado por vários autores para se referir a uma família de lógicas subestruturais em que a regra de troca é inadmissível . O restante deste artigo é dedicado a uma apresentação dessa aceitação do termo.
A lógica não comutativa mais antiga é o cálculo de Lambek , que deu origem à classe de lógicas conhecida como gramáticas categóricas . Desde a publicação da lógica linear de Jean-Yves Girard , várias novas lógicas não comutativas foram propostas, a saber, a lógica linear cíclica de David Yetter, a lógica de pomets de Christian Retoré e as lógicas não comutativas BV e NEL .
A lógica não comutativa é algumas vezes chamada de lógica ordenada, uma vez que é possível com a maioria das lógicas não comutativas propostas impor uma ordem total ou parcial nas fórmulas em sequentes. No entanto, isso não é totalmente geral, pois algumas lógicas não comutativas não suportam tal ordem, como a lógica linear cíclica de Yetter. Embora a maioria das lógicas não comutativas não permita enfraquecimento ou contração junto com a não comutatividade, essa restrição não é necessária.
O cálculo de Lambek
Joachim Lambek propôs a primeira lógica não comutativa em seu artigo de 1958 Mathematics of Sentença Estrutura para modelar as possibilidades combinatórias da sintaxe das línguas naturais. Seu cálculo tornou-se, assim, um dos formalismos fundamentais da linguística computacional .
Lógica linear cíclica
David N. Yetter propôs uma regra estrutural mais fraca no lugar da regra de troca da lógica linear, gerando uma lógica linear cíclica. As sequências da lógica linear cíclica formam um anel e, portanto, são invariantes sob rotação, onde as regras de multipremise colam seus anéis nas fórmulas descritas nas regras. O cálculo suporta três modalidades estruturais, uma modalidade autodual que permite a troca, mas ainda linear, e os exponenciais usuais (? E!) Da lógica linear, permitindo que regras estruturais não lineares sejam usadas em conjunto com a troca.
Lógica Pomset
A lógica de Pomset foi proposta por Christian Retoré em um formalismo semântico com dois operadores sequenciais duais existindo junto com o produto tensorial usual e os operadores par da lógica linear, sendo que a primeira lógica proposta teria operadores comutativos e não comutativos. Um cálculo sequente para a lógica foi dado, mas faltou um teorema de eliminação de corte ; em vez disso, o sentido do cálculo foi estabelecido por meio de uma semântica denotacional.
BV e NEL
Alessio Guglielmi propôs uma variação do cálculo de Retoré, BV, na qual as duas operações não comutativas são colapsadas em um único operador autodual, e propôs um novo cálculo de prova, o cálculo de estruturas para acomodar o cálculo. A principal novidade do cálculo de estruturas era seu uso difundido de inferência profunda , que se argumentou ser necessária para cálculos combinando operadores comutativos e não comutativos; esta explicação concorda com a dificuldade de projetar sistemas sequentes para lógica de pomset que têm eliminação de corte.
Lutz Strassburger concebeu um sistema relacionado, NEL, também no cálculo de estruturas em que a lógica linear com a regra de mistura aparece como um subsistema.
Structads
Structads são uma abordagem à semântica da lógica que se baseia na generalização da noção de sequente ao longo das linhas das espécies combinatórias de Joyal , permitindo o tratamento de lógicas mais drasticamente não padronizadas do que aquelas descritas acima, onde, por exemplo, o ',' do o cálculo sequente não é associativo.
Veja também
Referências
links externos
- Lógica não comutativa I: o fragmento multiplicativo de V. Michele Abrusci e Paul Ruet, Annals of Pure and Applied Logic 101 (1), 2000.
- Aspectos lógicos da linguística computacional (PS) por Patrick Blackburn, Marc Dymetman, Alain Lecomte, Aarne Ranta, Christian Retoré e Eric Villemonte de la Clergerie.
- Artigos sobre Lógica Linear Comutativa / Não-comutativa no cálculo de estruturas : uma homepage de pesquisa na qual os artigos que propõem BV e NEL estão disponíveis.