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

De Wikiversidade

Índice 1 Introdução 2 Notação 3 Regras 3.1 Regras Lógicas 3.2 Regras Estruturais 4 Teoremas

[editar] Introdução

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.

[editar] Notação

Essa expressão deve ser interpretada da seguinte maneira: se A1,...,An forem todos verdadeiros então pelo menos um Bi em B1,...,Bn 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.

[editar] Regras

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.

[editar] Regras Lógicas

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

• 
• 
• 
• 
• 
• 
• 
• 

[editar] Regras Estruturais

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):

[editar] Teoremas

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