Regra estrutural

Predefinição:Sem-fontes Na teoria da prova, uma regra estrutural é uma regra de inferência que não se refere a qualquer conectivo lógico, mas em vez disso, atua na sentença ou nos sequentes diretamente. Regras estruturais frequentemente imitam propriedades meta-teóricas da lógica. Lógicas que negam uma ou mais regras estruturais são classificados como lógicas subestruturais.

Regras estruturais comuns

Três regras estruturais comuns são:

• Enfraquecimento, onde as hipóteses ou a conclusão de um sequente podem ser aumentadas com sequentes adicionais. De forma simbólica, as regras de enfraquecimento podem ser escritas desta forma $\frac{\mathrm{\Gamma }⊢\mathrm{\Sigma }}{\mathrm{\Gamma },A⊢\mathrm{\Sigma }}$ do lado esquerdo da catraca, e $\frac{\mathrm{\Gamma }⊢\mathrm{\Sigma }}{\mathrm{\Gamma }⊢A,\mathrm{\Sigma }}$ do lado direito dela.
• Contração, onde dois sequentes iguais (ou unificáveis) do mesmo lado da catraca podem ser repostos por um único sequente (ou instância comum). Simbolicamente: $\frac{\mathrm{\Gamma },A,A⊢\mathrm{\Sigma }}{\mathrm{\Gamma },A⊢\mathrm{\Sigma }}$ e $\frac{\mathrm{\Gamma }⊢A,A,\mathrm{\Sigma }}{\mathrm{\Gamma }⊢A,\mathrm{\Sigma }}$. Também conhecida como fatoramento em sistemas de prova automática de teoremas usando a resolução. Também conhecida como consequência lógica da idempotência na lógica clássica. 
• Permutação, onde dois sequentes do mesmo lado da catraca podem ser permutados. Simbolicamente: $\frac{{\mathrm{\Gamma }}_1,A,{\mathrm{\Gamma }}_2,B,{\mathrm{\Gamma }}_3⊢\mathrm{\Sigma }}{{\mathrm{\Gamma }}_1,B,{\mathrm{\Gamma }}_2,A,{\mathrm{\Gamma }}_3⊢\mathrm{\Sigma }}$ e $\frac{\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_1,A,{\mathrm{\Sigma }}_2,B,{\mathrm{\Sigma }}_3}{\mathrm{\Gamma }⊢{\mathrm{\Sigma }}_1,B,{\mathrm{\Sigma }}_2,A,{\mathrm{\Sigma }}_3}$. (Esta regra também é conhecida como regra da permutação).

Uma lógica sem qualquer uma das regras estruturais acima interpretaria os lados esquerdo ou direito como puras sequências; com a permutação, eles são multiconjuntos; e tanto com a contração como com a contração, eles são conjuntos.

Estes não são as únicas regras estruturais possíveis. Uma regra estrutural famosa é conhecida como corte. Um esforço considerável é despendido por teóricos da prova mostrando que as regras de corte são supérfluas em várias lógicas. Mais precisamente, o que se mostra é que o corte é apenas (em um certo sentido), uma ferramenta para abreviar provas, e não contribui com os teoremas que podem ser provados. O sucesso da "remoção" das regras de corte, conhecidas como eliminação do corte, está diretamente relacionada com a filosofia da computação conhecida como normalização (ver isomorfismo de Curry-Howard); ela frequentemente dá uma boa indicação da complexidade de decidir sobre uma determinada lógica.

Ver também

• Lógica Afim
• Lógica Linear
• Lógica Ordenada
• Lógica Estrita
• Lógica de Separação