Lógica subestrutural

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Text document with red question mark.svg
Este artigo ou secção contém fontes no fim do texto, mas que não são citadas no corpo do artigo, o que compromete a confiabilidade das informações. (desde abril de 2013)
Por favor, melhore este artigo inserindo fontes no corpo do texto quando necessário.

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

.

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

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

de

.

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

nós podemos deduzir

.

Também a partir de

se pode deduzir, para qualquer B ,

.

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).

Composição de premissas[editar | editar código-fonte]

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.

História[editar | editar código-fonte]

É 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.

Veja também[editar | editar código-fonte]

Referências[editar | editar código-fonte]

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

Outras leituras[editar | editar código-fonte]

  • 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.

Links externos[editar | editar código-fonte]

Predefinição:Logic