Regra estrutural

Origem: Wikipédia, a enciclopédia livre.
Saltar para a navegação Saltar para a pesquisa
Question book.svg
Esta página ou secção não cita fontes confiáveis e independentes, o que compromete sua credibilidade (desde junho de 2017). Por favor, adicione referências e insira-as corretamente no texto ou no rodapé. Conteúdo sem fontes poderá ser removido.
Encontre fontes: Google (notícias, livros e acadêmico)

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[editar | editar código-fonte]

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  do lado esquerdo da catraca, e  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:  e . 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:  e . (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[editar | editar código-fonte]

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