Lógica não comutativa

A lógica não comutativa é uma extensão da lógica linear , que combina a conectivos comutativos da lógica linear com os conectivos não multiplicativos do cálculo de Lambek. Seu cálculo de sequentes baseia-se na estrutura de variedades de ordem (uma família de ordens cíclicas que pode ser vista como uma espécie de estrutura), e o critério para a correção de suas redes de prova é dado em termos de permutações parciais. Ela também tem uma semântica denotacional em que as fórmulas são interpretados por módulos através de 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 alguns autores para referir-se 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 da aceitação do termo.

A lógica não-comutativa mais antiga é o cálculo de Lambek, que deu origem à classe de lógicas conhecidas como gramáticas categóricas. Desde a publicação da lógica linear de Jean-Yves Girard houve várias lógicas não-comutativas propostas, isto é, a lógica linear cíclica de Davi Yetter, lógica pomset de Christian Retoré, e as lógicas não-comutativas BV e NEL estudadas no cálculo de estruturas.

A lógica não comutativa é às vezes chamado de ordenar lógica, uma vez que é possível com a maioria das lógicas não-comutativas propostas impor ordem total ou parcial nas fórmulas de sequentes. No entanto, este não é totalmente geral, já que algumas lógicas não-comutativas não suportam tal ordem, tal como a lógica linear cíclica de Yetter. Observe também que, enquanto a maioria das lógicas não-comutativas não permitem o enfraquecimento ou a contração juntamente com 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 científico (1958) Matemática da Estrutura de Sentença para o modelo possibilidades combinatórias da sintaxe das línguas naturais. O seu cálculo tornou-se, assim, um dos principais formalismos de 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, produzindo lógica linear cíclica. Os sequents da lógica linear cíclica formam um anel, e por isso são invariantes sob uma rotação, onde regras de multipremissas associam os anéis às fórmulas descritas nas regras. O cálculo suporta três modalidades estruturais, uma modalidade auto-dupla permitindo troca, mas ainda linear, e os exponenciais de costume (? e !) da lógica linear, permitindo regras subestruturais não lineares para serem usadas em conjunto com a troca.

Lógica pomset

A lógica pomset foi proposta por Christian Retoré em uma formalismo semântico com dois operadores sequenciais existindo juntamente com os habituais produto e o par de operadores de lógica linear, a primeira lógica proposta para que ambos operadores comutativos e não-comutativos. Um cálculo de sequente para a lógica foi dado, mas faltava-lhe um teorema da eliminação do corte; em vez disso, o sentido do cálculo foi estabelecido através de uma semântica denotacional.

BV e NEL

Alessio Guglielmi propôs uma variação do cálculo de Retoré, BV, em que os duas operações não-comutativas são recolhidas em um único, auto-duplo, operador e propôs uma nova prova, o cálculo de estruturas para acomodar o cálculo. A principal novidade do cálculo de estruturas foi seu difundido uso de inferência profunda, que foi argumentado é necessário para cálculos combinando operadores comutativos e não comutativos; esta explicação concorda com a dificuldade de conceber sistemas de sequentes para lógica pomset de que tem a eliminação de corte.

Lutz Strassburger desenvolveu um sistema relacionado, NEL, também para o cálculo de estruturas em que a lógica linear com a regra da mistura aparecem como um subsistema.

Structads

Structads são uma abordagem das semânticas da lógica que são baseadas em generalizar a noção de sequente ao longo das linhas de Joyal da espécies combinatoriais, permitindo o tratamento de lógicas mais drasticamente fora do padrão do que as descritas acima, onde, por exemplo, ',' do cálculo sequente não é associativo.

Ligações externas

1. Non-commutative logic I: the multiplicative fragment by V. Michele Abrusci and Paul Ruet, Annals of Pure and Applied Logic 101(1), 2000. Logical aspects of computational linguistics (PS) by Patrick Blackburn, Marc Dymetman, Alain Lecomte, Aarne Ranta, Christian Retoré and Eric Villemonte de la Clergerie. Papers on Commutative/Non-commutative Linear Logic in the calculus of structures: a research homepage from which the papers proposing BV and NEL are available.