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.
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.
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.
Cada conectivo
possui uma regra de introdução a direita
e uma a esquerda
:
- (axioma):
![{\displaystyle {\frac {}{\varphi \vdash \varphi }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/738101946eeb9ea892d69c468a873bb13f01e4ad)
- (corte):
![{\displaystyle {\frac {\Gamma \vdash \Delta ,\varphi \ \qquad \Sigma ,\varphi \vdash \Psi }{\Gamma ,\Sigma \vdash \Delta ,\Psi }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5825462f712681ea478c67faaedcccc6cfa20ffe)
![{\displaystyle (\vdash \rightarrow ):{\frac {\Gamma ,\varphi \vdash \psi ,\Delta }{\Gamma \vdash \varphi \rightarrow \psi ,\Delta }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/069e3c3d75f2d94e619fba74e941ad5c10f210ba)
![{\displaystyle (\rightarrow \vdash ):{\frac {\Gamma \vdash \varphi ,\Delta \qquad \Sigma ,\psi \vdash \Pi }{\Gamma ,\Sigma ,\varphi \rightarrow \psi \vdash \Delta ,\Pi }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6de81f88890cc274a6a9b0a8f6c94b3c9fe40f1c)
![{\displaystyle (\vdash \land ):{\frac {\Gamma \vdash \varphi ,\Delta \qquad \Gamma \vdash \psi ,\Delta }{\Gamma \vdash \varphi \land \psi ,\Delta }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ca8b746e0832cae8a15a3caad8ff6c32f1188ce8)
![{\displaystyle (\land \vdash ):{\frac {\Gamma ,\varphi ,\psi \vdash \Delta }{\Gamma ,\varphi \land \psi \vdash \Delta }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/38c1e927a7f26f5966a055db1193133c0f93dfad)
![{\displaystyle (\vdash \lor ):{\frac {\Gamma \vdash \varphi ,\psi ,\Delta }{\Gamma \vdash \varphi \lor \psi ,\Delta }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/50ba202c19ff878e3956b2530ba639f63b4e9bb3)
![{\displaystyle (\lor \vdash ):{\frac {\Gamma ,\varphi \vdash \Delta \qquad \Gamma ,\psi \vdash \Delta }{\Gamma ,\varphi \lor \psi \vdash \Delta }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f8e26f076dde881473d49c2869a1daa74417da63)
![{\displaystyle (\vdash \neg ):{\frac {\Gamma ,\varphi \vdash \Delta }{\Gamma \vdash \neg \varphi ,\Delta }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/72fef505c6aae3cfffca8df082cf52d378f904f0)
![{\displaystyle (\vdash \neg ):{\frac {\Gamma \vdash \varphi ,\Delta }{\Gamma ,\neg \varphi \vdash \Delta }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b6267145f2bcc873bb32133522380a535ab31a4c)
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):
![{\displaystyle {\frac {\Gamma ,\varphi ,\psi ,\Sigma \vdash \Delta }{\Gamma ,\psi ,\varphi ,\Sigma \vdash \Delta }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b8e6fbf360f6cdbd3d4630bd41a25aa1222be5a8)
- (monotonicidade):
![{\displaystyle {\frac {\Gamma \vdash \Delta }{\Gamma ,\varphi \vdash \Delta }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/70871494c44d6aeef4d0bfac9963302ee78dcd72)
- (contração):
![{\displaystyle {\frac {\Gamma ,\varphi ,\varphi \vdash \Delta }{\Gamma ,\varphi \vdash \Delta }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1cc324c97647823e3dd533ae1b486767d6e498fe)
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
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.
|