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


Introdução editar

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

 

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

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

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


  • (axioma):  


  • (corte):  


  •  


  •  


  •  


  •  


  •  


  •  


  •  


  •  

Regras Estruturais editar

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

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

 

 
 

 

 
 
 
 

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  

 

 
  
 
 


 

 
 


 

 
 
 
 


 

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