Lógica subestrutural
De Wikipedia, a enciclopédia encyclopedia
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.
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. (Abril de 2013) |
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).