Lógica subestrutural

Este artigo ou secção contém uma lista de referências no fim do texto, mas as suas fontes não são claras porque não são citadas no corpo do artigo, o que compromete a confiabilidade das informações. Ajude a melhorar este artigo inserindo citações no corpo do artigo. (Abril de 2013)

Em lógica, uma subestrutura lógica é uma falta lógica das regras estruturais usuais (p.e. da lógica clássica e intuicionista), tal como enfraquecimento, contração ou associatividade. Duas das lógicas subestruturais mais significativas são lógica de relevância e lógica linear.

No cálculo de sequentes, se escreve cada linha de uma prova como

${\displaystyle \Gamma \vdash \Sigma }$.

Aqui as regras são regras estruturais para reescrever os LDE Γ de um sequente, inicialmente concebido como um string de proposições. A interpretação padrão desta string é como conjunção: nós devemos ler

${\displaystyle {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {C}}}$

como a notação sequente para

(A e B) implica C.

Aqui nós estamos tomando os LDE Σ para ser uma simples proposição C (que é o intuicionista estilo de sequente); mas tudo o que se aplica igualmente ao caso geral, uma vez que todas as manipulações estão indo para a esquerda do símbolo de sequente.

Desde que a conjunção é uma operação comutativa e associativa , a criação formal da teoria de sequentes normalmente inclui regras estruturais para reescrever o sequente Γ adequadamente - por exemplo para deduzir

${\displaystyle {\mathcal {B}},{\mathcal {A}}\vdash {\mathcal {C}}}$

de

${\displaystyle {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {C}}}$.

Existem mais regras estruturais correspondentes a Idempotência e monotônica propriedades de conjunção: de

${\displaystyle \Gamma ,{\mathcal {A}},{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$

nós podemos deduzir

${\displaystyle \Gamma ,{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$.

Também a partir de

${\displaystyle \Gamma ,{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$

se pode deduzir, para qualquer B ,

${\displaystyle \Gamma ,{\mathcal {A}},{\mathcal {B}},\Delta \vdash {\mathcal {C}}}$.

Lógica linear, em que hipóteses duplicadas 'contam' de forma diferente a partir de ocorrências individuais, deixa de fora essas duas regras, enquanto a lógica relevante simplesmente deixa de fora a última regra, pelo fato do B ser claramente relevante para a conclusão.

Estes são exemplos básicos de regras estruturais. Não que essas regras sejam controversas, quando aplicado no cálculo proposicional convencional. Elas ocorrem naturalmente na teoria da prova, tendo sido notado pela primeira vez lá(antes de receber um nome).

Existem inúmeras formas de compor premissas (e no caso de conclusões múltiplas, as conclusões também).Uma maneira é para reuni-lás em um conjunto. Mas desde que p.e. {a,a} = {a} temos contrações livres se as premissas são conjuntos. Nós também temos associatividade e permutação (ou comutatividade) para serem livres também, entre outras propriedades. Em lógica subestrutural, tipicamente premissas não são compostas em conjuntos, mas elas são compostas em estruturas mais refinadas, tal como árvores ou multisets (conjuntos que distinguem múltiplas ocorrências de elementos) ou sequências de fórmulas. Por exemplo, na lógica linear, desde que as contrações falhem, as premissas devem ser compostas em algo pelo menos tão refinado quanto os multisets.

É um campo relativamente novo. A primeira conferência sobre o tema foi realizada em outubro de 1990 em Tübingen, como “Logics with Restricted Structural Rules”. Durante a conferência, Kosta Došen propôs o termo “substructural logics”, que é agora usado atualmente.

• Sistema subestrutural (em inglês)
• Entrelaçamento (em inglês)
• Consequência lógica

• F. Paoli (2002), Substructural Logics: A Primer, Kluwer.

• Galatos, Nikolaos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono (2007), Residuated Lattices. An Algebraic Glimpse at Substructural Logics, Elsevier, ISBN 978-0-444-52141-5.

• Predefinição:Sep entry

Predefinição:Logic