Regra estrutural

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 {\Gamma \vdash \Sigma }{\Gamma ,A\vdash \Sigma }}$ do lado esquerdo da catraca, e ${\frac {\Gamma \vdash \Sigma }{\Gamma \vdash A,\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 {\Gamma ,A,A\vdash \Sigma }{\Gamma ,A\vdash \Sigma }}$ e ${\frac {\Gamma \vdash A,A,\Sigma }{\Gamma \vdash A,\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 {\Gamma _{1},A,\Gamma _{2},B,\Gamma _{3}\vdash \Sigma }{\Gamma _{1},B,\Gamma _{2},A,\Gamma _{3}\vdash \Sigma }}$ e ${\frac {\Gamma \vdash \Sigma _{1},A,\Sigma _{2},B,\Sigma _{3}}{\Gamma \vdash \Sigma _{1},B,\Sigma _{2},A,\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.