lógica subestrutural

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