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

Origem: Wikilivros, livros abertos por um mundo aberto.
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 demonstrar 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 :


  • (axioma):


  • (corte):









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.

  • (comutatividade):


  • (monotonicidade):


  • (contração):


Metateoremas[editar | editar código-fonte]

Para provar a consistência 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 Consistência: O cálculo de seqüêntes é consistente

Teoremas e Inferências[editar | editar código-fonte]







Observação: A partir deste ponto, por questões de economia, omitiremos o uso da regra de comutatividade.




Exercício: Prove





Exercício: Prove




Exercício: Prove


 











Nuvola apps edu mathematics-p.svg

Esta página é um esboço de matemática. Ampliando-a você ajudará a melhorar o Wikilivros.