Lógica: Cálculo Proposicional Clássico: Cálculo de Sequêntes

Fonte: Wikiversidade
Saltar para a navegação Saltar para a pesquisa



Introdução[editar | editar código-fonte]

Uma outra, e não menos importante, forma de se calcular a validade de argumentos em lógica proposicional clássica é o chamado cálculo de sequêntes. O cálculo de sequêntes foi proposto por Gentzen na década de trinta como uma tentativa (bem-sucedida) de demostrar a consistência da lógica proposicional clássica.

O estudo do cálculo de sequentes é especialmente importante para a melhor compreensão de algumas lógicas não-clássicas em especial as lógicas sub-estruturais.

Notação[editar | editar código-fonte]

Essa expressão deve ser interpretada da seguinte maneira: se forem todos verdadeiros então pelo menos um em deve ser verdadeiro.

Por exemplo o sequênte indica que de vazio provamos vazio, ou seja, que a contradição é um teorema e portanto a lógica não é consistente. Em outras palavras: para provar que o cálculo de sequentes é consistente temos que mostrar que o sequente não é válido.

Regras[editar | editar código-fonte]

O calculo de sequêntes, como em todos as outras faces da sintática de qualquer lógica, possui regras de manipulação. Essas regras são divididas em dois tipos: regras lógicas e regras estruturais. As regras lógicas nos mostram como introduzir conectivos lógicos a esquerda e a direita em um sequente enquanto as regras estruturais, como o próprio nome diz são estruturais.

Regras Lógicas[editar | editar código-fonte]

Cada conectivo possui uma regra de introdução a direita e uma a esquerda :

Regras Estruturais[editar | editar código-fonte]

A regra da associatividade é considerada implicitamente. As regras estruturais são idênticas a esquerda e a direita. Vamos mostrar só um dos lados para economizar espaço.

  • (axioma):
  • (comutatividade):
  • (monotonicidade):
  • (contração):
  • (corte):

Teoremas[editar | editar código-fonte]

Para provar a consistencia do cálculo de seqüêntes vamos primeiro enunciar um (meta)teorema importante no cálculo de seqüêntes:

Teorema da eliminação do corte: Tudo que pode ser provado pelo cálculo de seqüêntes pode ser provado sem usar a regra do corte.

As demais regras do cálculo de seqüêntes são chamadas de analíticas pois preservam os símbolos atômicos. Como a regra do corte não é necessária todos os símbolos atômicos são preservados de algum dos lados e portanto partindo de não conseguimos chegar em e portanto provamos o seguinte teorema:

Teorema da Consistencia: O cálculo de seqüêntes é consistênte