Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte I

Introdução

Até agora nós temos dois métodos que sempre determinam a validade de argumentos e fórmulas no CPC(Cálculo Proposicional Clássico): as tabelas de verdade e os tableaux semânticos. Claro que também podemos determinar a validade de uma fórmula mostrando que esta se trata de uma instância de outra fórmula válida, ou por interdefinibilidade de operadores mostrar que ela é equivalente a uma outra fórmula válida, mas estes métodos não são aplicáveis em quaisquer circunstâncias. Agora aprenderemos um terceiro método que sempre determina a validade de fórmulas e argumentos no CPC, além de consistir em um método de derivação, a Dedução Natural.

Tomemos o seguinte argumento:

$A\to \neg \neg B$

$A$

$\therefore B\lor \left(\neg \neg C\lor D\right)$

As tabelas de verdade não parecem muito práticas neste caso. Afinal, temos quatro fórmulas atômicas, o que requer uma tabela de 16 linhas. Sem falar que teríamos muitas colunas também, dada a quantidade de sub-fórmulas.

A alternativa é provar a validade do argumento por tableaux. Contudo, repare que intuitivamente este argumento não passa da simples combinação de vários argumentos válidos, simples e que nós já conhecemos.

Temos o Modus Ponens:

$A\to \neg \neg B$

$A$

$\therefore \neg \neg B$

A eliminação da dupla negação:

$\neg \neg B$

$\therefore B$

Também sabemos que se uma fórmula $\varphi$ é verdadeira, então entre $\varphi$ e uma fórmula arbitrária $\psi$, ao menos uma é verdadeira. Ou seja:

$\varphi$

$\therefore \varphi \lor \psi$

Esse argumento é chamado de "Expansão". Ora, o seguinte argumento é obviamente uma instância da expansão:

$B$

$\therefore B\lor \left(\neg \neg C\lor D\right)$

Se sabemos de tudo isso, então porque usar o método de tableaux semânticos se estes nos obrigam a considerar o valor de proposições arbitrárias como $\left(\neg \neg C\lor D\right)$, assim como lidar com os valores de $\neg \neg B$ e de $\neg B$, quando sabemos que a primeira é equivalente a $B$?

É justamente isto que a Dedução Natural permite: por meio de um pequeno número de regras de inferência, demonstrar a validade de uma infinidade de fórmulas e argumentos sem a necesidade de considerar os valores que cada fórmula ou subfórmula recebe. Ou seja, não estamos mais lidando com a semântica, mas com a sintaxe.

Agora incrementaremos nossa notação e terminologia. Até agora usamos o martelo semântico, "$\vDash$". Agora usaremos o martelo sintático, "$\vdash$".

A leitura que fazemos de cada:

$\Gamma \vDash \alpha$

$\alpha$ é conseqüência semântica de $\Gamma$, ou $\Gamma$ implica semanticamente em $\alpha$.

$\Gamma \vdash \alpha$

$\alpha$ é conseqüência sintática de $\Gamma$, ou a partir de $\Gamma$ prova-se $\alpha$.

$\vDash \alpha$

$\alpha$ é uma fórmula válida (tautologia no caso do CPC).

$\vdash \alpha$

$\alpha$ é um teorema.

É dito de um sistema lógico que ele é correto se ele verifica a seguinte propriedade:

$\Gamma \vdash \alpha \Longrightarrow \Gamma \vDash \alpha$

Ou seja, que todos os argumentos sintaticamente válidos também são semanticamente válidos.

É dito de um sistema lógico que ele é completo se ele verifica a seguinte propriedade:

$\Gamma \vDash \alpha \Longrightarrow \Gamma \vdash \alpha$

Ou seja, que todos os argumentos semanticamente válidos também são sintaticamente válidos.

O CPC verifica ambas propriedades, ou seja, o CPC verifica que:

$\Gamma \vdash \alpha \iff \Gamma \vDash \alpha$

Obviamente, isto também é verificado na instância em que $\Gamma =\varnothing$. Portanto:

$\vdash \alpha \iff \vDash \alpha$

Ou seja, todo teorema é tautologia e toda tautologia é teorema.

Regras de Inferência Diretas

Nas disciplinas matemáticas como a lógica, a geometria, a aritmética etc., é preferível demonstrar o máximo (de teoremas, construções... válidos, obviamente) por meio do mínimo (de conceitos primitivos, axiomas, regras de inferência etc.).

Na Dedução Natural trabalhamos apenas com regras de inferência. Para que a correção do sistema seja verificada, as regras escolhidas devem ser reconhecidas como válidas. A completude é um pouco mais complicada. Digamos que para verificar a completude o ideal seria ter duas regras para cada operador usado: uma que o insira e outra que o remova.

Trabalharemos primeiramente com as regras de infererência diretas. Como o nome sugere, estas regras regulam quais fórmulas podemos inferir diretamente de outras fórmulas.

Agora vejamos como construir uma dedução usando as regras de inferência diretas. Vamos provar aquele argumento da introdução:

$\left\{A\to \neg \neg B,A\right\}\vdash B\lor \left(\neg \neg C\lor D\right)$

O primeiro passo é colocar cada premissa em uma linha enumerada:

1.   $A\to \neg \neg B$   Premissa 2.   $A$   Premissa

Agora, aplicamos as regras de inferência que julgarmos úteis para chegar ao resultado esperado. Para cada nova fórmula inferida, inserimos uma linha enumerada, indicando à direita as linhas que contém as fórmulas a partir das quais foi efetuada a inferência, assim como a regra aplicada.

Por exemplo, vamos aplicar nas linhas 1 e 2 o Modus Ponens (MP):

1.   $A\to \neg \neg B$   Premissa 2.   $A$   Premissa 3.   $\neg \neg B$   1,2 MP

Agora aplicaremos a regra de Dupla Negação (DN) na linha 3 a fim de derivar $B$. Então aplicaremos a Expansão (E) a fim de obter $B\lor \left(\neg \neg C\lor D\right)$.

1.   $A\to \neg \neg B$   Premissa 2.   $A$   Premissa 3.   $\neg \neg B$   1,2 MP 4.   $B$   3 DN 5.   $B\lor \left(\neg \neg C\lor D\right)$   4 E

Ou seja, sob o conjunto de premissas $\left\{A\to \neg \neg B,A\right\}$, derivamos, por meio de inferências reconhecidas como válidas, $B\lor \left(\neg \neg C\lor D\right)$. Portanto, $\left\{A\to \neg \neg B,A\right\}\vdash B\lor \left(\neg \neg C\lor D\right)$.

Repare também que na linha 3 provamos que $\left\{A\to \neg \neg B,A\right\}\vdash \neg \neg B$ , e na linha 4, $\left\{A\to \neg \neg B,A\right\}\vdash B$.

Façamos mais uma derivação a fim de aplicar outras regras. Vamos provar que $\left\{A\leftrightarrow B,B\land C\right\}\vdash A\land B$.

1.   $A\leftrightarrow B$   Premissa 2.   $B\land C$   Premissa 3.   $B\to A$   1 BC 4.   $B$   2 S 5.   $A$   3,4 MP 6.   $A\land B$   5,4 C

Nas linhas 1 e 2 temos as premissas $A\leftrightarrow B$ e $B\land C$, respectivamente. Aplicamos Bi-condicionais para Condicionais (BC) na linha 1 e derivamos $B\to A$ na linha 3. Então aplicamos Separação (S) na linha 2 a fim de derivar $B$ na linha 4. Aplicamos Modus Ponens nas linhas 3 e 4 a fim de derivar $A$ na linha 5. Então aplicamos Conjunção (C) nas linhas 5 e 4 a fim de derivar $A\land B$. Q.e.d

Exercícios

Prove por dedução natural que:

1. $\left\{A\leftrightarrow \left(B\lor C\right),\neg \neg B\right\}\vdash A\land B$
2. $\left\{A\lor B,B\to C,\neg A\land D\right\}\vdash C$
3. $\left\{A\to C,C\to A,\left(A\leftrightarrow C\right)\to B\right\}\vdash B$

Resolução dos Exercícios

Trabalhando com Hipóteses

Você deve ter reparado que faltou uma regra para inserir a negação, assim como uma regra para inserir a implicação independentemente da bi-implicação. Para tal, fazemos uso das regras hipotéticas, ou seja, regras que nos permitem trabalhar com hipóteses.

Em Dedução Natural, hipóteses são quaisquer fórmulas bem construídas que inserimos na derivação sem derivá-las de quaisquer outras fórmulas. Com as regras hipotéticas, nosso sistema fica completo. Vejamos então um esquema geral para trabalhar com as hipóteses.

1.   $\varphi$   Premissa   2.     $\psi$   Hipótese

Inserimos uma hipótese $\psi$ na linha 2. Isto nos obriga a inserir uma linha vertical. Esta linha permanecerá aí até aplicarmos uma regra hipotética que remova-a. Até então, tudo o que derivarmos por meio das regras diretas estará à direita da linha de hipótese:

1.   $\varphi$   Premissa   2.     $\psi$   Hipótese 3.     $\psi \lor \chi$   2 E 4.     $\varphi \land \psi$   1,2 C 5.     $\varphi \lor \chi$   1 E 6.     $\left(\varphi \lor \chi \right)\land \left(\psi \lor \chi \right)$   5,3 C 7.   $\xi$   alguma regra hipotética

Também podemos levantar hipóteses dentro de hipóteses, inserindo novas linhas verticais:

1.   $\varphi$   Premissa   2.     $\psi$   Hipótese 3.     $\psi \lor \chi$   2 E 4.       $\xi$   Hipótese 5.       $\xi \land \left(\psi \lor \chi \right)$   4,3 C 6.     $\zeta$   alguma regra hipotética 7.   $\delta$   alguma regra hipotética

Antes de apresentarmos as regras hipotéticas, lembre-se de sempre respeitar as seguintes prescrições:

1. Introduzir uma linha vertical para cada nova hipótese.
2. Uma vez que uma linha é descartada, não usar mais qualquer fórmula que esteja a sua direita.
3. As hipóteses devem ser descartadas na ordem inversa nas quais são levantadas.
4. Uma dedução não está terminada enquanto não forem descartadas todas as hipóteses.

Redução ao Absurdo (RAA)

Se a partir de uma hipótese $\varphi$ derivarmos uma contradição, então descartamos a hipótese e introduzimos $\neg \varphi$ na derivação.

Um exemplo:

1.   $\alpha$   Premissa   2.     $\neg \alpha$   Hipótese 3.     $\alpha \land \neg \alpha$   1,2 C 4.   $\neg \neg \alpha$       2,3 RAA

Na linha 1 temos $\alpha$ como premissa. Na linha 2 levantamos a hipótese $\neg \alpha$. Na linha 3 aplicamos a conjunção em $\alpha$ e $\neg \alpha$, obtendo a contradição $\alpha \land \neg \alpha$. Como a partir da hipótese derivamos uma contradição, a descartamos e deduzimos sua negação, $\neg \neg \alpha$.

Portanto, $\alpha \vdash \neg \neg \alpha$

Regra de Prova Condicional (RPC)

Se ao levantarmos uma hipótese $\varphi$ inferimos $\psi$, então podemos descartar a hipótese e inserir $\varphi \to \psi$ na derivação.

Por exemplo:

1.   $\alpha \to \beta$   Premissa 2.   $\beta \to \gamma$   Premissa   3.     $\alpha$   Hipótese 4.     $\beta$   1,3 MP 5.     $\gamma$   2,4 MP 6.   $\alpha \to \gamma$   3,5 RPC

Aqui temos as premissas $\alpha \to \beta$ e $\beta \to \gamma$ nas linhas 1 e 2, respectivamente. Na linha 3 levantamos a hipótese $\alpha$. Aplicando Modus Ponens nas linhas 1 e 3, inferimos $\beta$ na linha 4. Aplicando Modus Ponens nas linhas 2 e 4, inferimos $\gamma$ na linha 5. Dado que apartir de $\alpha$ inferimos $\gamma$, descartamos a hipótese e inserimos $\alpha \to \gamma$ na dedução.

Portanto, $\left\{\alpha \to \beta ,\beta \to \gamma \right\}\vdash \alpha \to \gamma$

Exercícios

Fazendo uso das regras hipotéticas, demonstre que:

1. $P\to Q\vdash P\to \left(Q\lor C\right)$
2. $P\to \neg P\vdash \neg P$
3. $A\lor B\vdash \neg A\to B$
4. $A\to B\vdash \neg \left(A\land \neg B\right)$
5. $\left\{\neg \left(A\land B\right),A\right\}\vdash \neg B$

Resolução dos Exercícios