Regra estrutural
 | Este artigo não cita fontes confiáveis. Ajude a inserir referências. Conteúdo não verificável pode ser removido.—Encontre fontes: ABW • CAPES • Google (N • L • A) (Junho de 2017) |
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 Γ ⊢ Σ Γ , A ⊢ Σ {\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma ,A\vdash \Sigma }}} do lado esquerdo da catraca, e Γ ⊢ Σ Γ ⊢ A , Σ {\displaystyle {\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: Γ , A , A ⊢ Σ Γ , A ⊢ Σ {\displaystyle {\frac {\Gamma ,A,A\vdash \Sigma }{\Gamma ,A\vdash \Sigma }}} e Γ ⊢ A , A , Σ Γ ⊢ A , Σ {\displaystyle {\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: Γ 1 , A , Γ 2 , B , Γ 3 ⊢ Σ Γ 1 , B , Γ 2 , A , Γ 3 ⊢ Σ {\displaystyle {\frac {\Gamma _{1},A,\Gamma _{2},B,\Gamma _{3}\vdash \Sigma }{\Gamma _{1},B,\Gamma _{2},A,\Gamma _{3}\vdash \Sigma }}} e Γ ⊢ Σ 1 , A , Σ 2 , B , Σ 3 Γ ⊢ Σ 1 , B , Σ 2 , A , Σ 3 {\displaystyle {\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).
do lado esquerdo da 
do lado direito dela.
e
Γ
⊢
A
,
A
,
Σ
Γ
⊢
A
,
Σ
{\displaystyle {\frac {\Gamma \vdash A,A,\Sigma }{\Gamma \vdash A,\Sigma }}}
. Também conhecida como fatoramento em sistemas de 
e
Γ
⊢
Σ
1
,
A
,
Σ
2
,
B
,
Σ
3
Γ
⊢
Σ
1
,
B
,
Σ
2
,
A
,
Σ
3
{\displaystyle {\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.