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

Origem: Wikilivros, livros abertos por um mundo aberto.

< Lógica | Cálculo Proposicional Clássico(Redireccionado de Lógica: Cálculo Proposicional Clássico: Cálculo de Sequêntes)

Ir para: navegação, pesquisa

acima: Voltar para o índice de Cálculo Proposicional Clássico
anterior: Axiomática |

Índice

1 Introdução
2 Notação
3 Regras
- 3.1 Regras Lógicas
- 3.2 Regras Estruturais
4 Metateoremas
5 Teoremas e Inferências

[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 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.

[editar] Notação

$A1, ..., An \vdash B1, ..., Bm$

Essa expressão deve ser interpretada da seguinte maneira: se $A 1,..., A n$ forem todos verdadeiros então pelo menos um $B i$ em $B 1,..., B n$ deve ser verdadeiro.

Por exemplo o sequênte $\vdash$ 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 $\vdash$ 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 $(\vdash \#)$ e uma a esquerda $(\# \vdash)$ :

(axioma): $\frac{}{\varphi \vdash \varphi}$

(corte): $\frac{\Gamma \vdash \Delta, \varphi\ \qquad \Sigma, \varphi \vdash \Psi}{\Gamma, \Sigma \vdash \Delta, \Psi}$

$(\vdash \rightarrow): \frac{\Gamma, \varphi \vdash \psi, \Delta}{\Gamma \vdash \varphi \rightarrow \psi, \Delta}$

$(\rightarrow \vdash): \frac{\Gamma \vdash \varphi, \Delta \qquad \Sigma, \psi \vdash \Pi}{\Gamma,\Sigma, \varphi \rightarrow \psi \vdash \Delta, \Pi}$

$(\vdash \land): \frac{\Gamma \vdash \varphi, \Delta \qquad \Gamma \vdash \psi, \Delta}{\Gamma \vdash \varphi \land \psi, \Delta}$

$(\land \vdash): \frac{\Gamma, \varphi, \psi \vdash \Delta}{\Gamma, \varphi \land \psi \vdash \Delta}$

$(\vdash \lor): \frac{\Gamma \vdash \varphi , \psi,\Delta}{\Gamma \vdash \varphi \lor \psi, \Delta}$

$(\lor \vdash): \frac{\Gamma, \varphi \vdash \Delta \qquad \Gamma, \psi\vdash \Delta}{\Gamma, \phi \lor \psi \vdash \Delta}$

$(\vdash \neg): \frac{\Gamma, \varphi \vdash \Delta}{\Gamma \vdash \neg \varphi, \Delta}$

$(\vdash \neg): \frac{\Gamma \vdash \varphi, \Delta}{\Gamma, \neg \varphi \vdash \Delta}$

[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.

(comutatividade): $\frac{\Gamma, \varphi, \psi, \Sigma \vdash \Delta}{\Gamma, \psi, \varphi, \Sigma \vdash \Delta}$

(monotonicidade): $\frac{\Gamma \vdash \Delta}{\Gamma, \varphi \vdash \Delta}$

(contração): $\frac{\Gamma, \varphi, \varphi \vdash \Delta}{\Gamma, \varphi \vdash \Delta}$

[editar] Metateoremas

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 $A \vdash A$ não conseguimos chegar em $\vdash$ e portanto provamos o seguinte teorema: