Quatro técnicas de dedução

As ferramentas de partida

Na aula sobre sistemas dedutivos formais, fixou-se o sistema de Łukasiewicz. Sua linguagem é a língua de círculos e discos, escrita com as abreviaturas oficiais da aula sobre a linguagem da lógica proposicional; seus axiomas são todas as instâncias dos três esquemas seguintes, em que $\varphi$, $\psi$ e $\chi$ são fórmulas quaisquer, e sua única regra é o modus ponens.

• A1: $(\varphi \rightarrow (\psi \rightarrow \varphi))$.
• A2: $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$.
• A3: $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$.
• MP: de $\varphi$ e $(\varphi \rightarrow \psi)$ deduz-se $\psi$.

Uma dedução de $\varphi$ a partir de um conjunto $\Gamma$ de fórmulas é uma sequência finita de fórmulas que termina em $\varphi$ e na qual cada fórmula é um axioma, um elemento de $\Gamma$ ou o resultado de aplicar o modus ponens a duas fórmulas anteriores; se ela existe, escreve-se $\Gamma \vdash \varphi$, e, se $\Gamma$ é vazio, $\vdash \varphi$, e diz-se que $\varphi$ é um teorema. Nessa mesma aula foram demonstrados os metateoremas que usaremos aqui: a reflexividade (Refl: se $\varphi \in \Gamma$, então $\Gamma \vdash \varphi$), a monotonicidade (Mon: se $\Gamma \subseteq \Delta$ e $\Gamma \vdash \varphi$, então $\Delta \vdash \varphi$), o modus ponens entre deduções (se $\Gamma \vdash \varphi$ e $\Gamma \vdash (\varphi \rightarrow \psi)$, então $\Gamma \vdash \psi$), o corte (Corte: se $\Gamma \vdash \varphi_{i}$ para cada $i$ de $1$ a $n$ e $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, então $\Gamma \vdash \psi$), a finitude (se $\Gamma \vdash \varphi$, algum subconjunto finito de $\Gamma$ basta), o teorema da dedução (TD: se $\Gamma \cup \{\varphi\} \vdash \psi$, então $\Gamma \vdash (\varphi \rightarrow \psi)$) e sua recíproca (RTD), e o teorema $\vdash (\varphi \rightarrow \varphi)$, que nas justificações abreviaremos Id. Por último, $\varphi \dashv\vdash \psi$ (equivalência demonstrável) significa que $\{\varphi\} \vdash \psi$ e $\{\psi\} \vdash \varphi$.

Convém lembrar que $\neg$ e $\rightarrow$ não são símbolos da língua base, mas abreviaturas: $\neg\varphi$ é a cadeia $(\varphi \downarrow \varphi)$, e $(\varphi \rightarrow \psi)$ é $(\neg\varphi \vee \psi)$, isto é, $\neg(\neg\varphi \downarrow \psi)$. Os três axiomas falam apenas de negações e de implicações, e a mesma aula mostrou, com uma marca de valores $0$ e $1$ que eles e o modus ponens conservam, o limite que daí decorre: no sistema de Łukasiewicz, a partir de $(v_{1} \downarrow v_{2})$ não se deduz $(\neg\neg v_{1} \downarrow v_{2})$, e a negação conjunta fica em parte fora de seu alcance. Esta aula procede, portanto, em dois tempos. Até a dupla negação inclusive, $\vdash$ refere-se ao sistema de Łukasiewicz, e nada do que se demonstra depende de desdobrar as abreviaturas. Demonstrada a dupla negação, acrescenta-se ao sistema uma segunda regra primitiva, a substituição da dupla negação, que atua sobre a cadeia desdobrada; a partir desse ponto, $\vdash$ refere-se ao sistema do curso, o de Łukasiewicz mais essa regra. Como toda dedução do primeiro é também dedução do segundo, nada do que foi demonstrado antes se perde.

Dois estilos de dedução

Há duas maneiras de escrever uma dedução, e ambas serão usadas. A primeira é a dedução propriamente dita, uma sequência de fórmulas na qual cada linha é um axioma, uma premissa ou o resultado do modus ponens; cada linha é justificada com A1, A2, A3, Premissa ou MP$(i, j)$, em que a linha $i$ é o antecedente e a linha $j$ é a implicação cujo antecedente é exatamente a linha $i$ (e, desde que se introduza a regra nova, SDN$(i)$). A segunda é a dedução sobre deduções, cujas linhas não são fórmulas, mas afirmações da forma $\Gamma \vdash \varphi$; cada uma é justificada com um metateorema já demonstrado, e a sequência inteira é um raciocínio da metalinguagem que garante que existe uma dedução do primeiro estilo, embora não a escreva. As justificações deste segundo estilo leem-se como segue.

• Refl: a fórmula da direita pertence ao conjunto da esquerda.
• A1, A2, A3: a fórmula da direita é uma instância do esquema; uma instância de um axioma deduz-se a partir de qualquer $\Gamma$ com uma dedução de uma só linha.
• MP$(i, j)$: o modus ponens entre deduções, aplicado à linha $i$, $\Gamma \vdash \varphi$, e à linha $j$, $\Gamma \vdash (\varphi \rightarrow \psi)$, com o mesmo $\Gamma$.
• TD$(i)$ e RTD$(i)$: o teorema da dedução ou sua recíproca, aplicado à linha $i$.
• O nome de um teorema já demonstrado, como Id ou DN: a fórmula da direita é uma instância desse teorema, e deduz-se a partir de qualquer $\Gamma$ por monotonicidade, porque o conjunto vazio está contido em $\Gamma$.
• Premissa, em uma dedução sobre deduções: a linha é uma das hipóteses da regra que se está demonstrando.

Todo resultado desta aula é enunciado com metavariáveis e vale, portanto, para fórmulas quaisquer: sua demonstração é um esquema, e, ao trocar nela cada metavariável por uma fórmula, obtém-se outra demonstração, porque as instâncias de um esquema de axioma continuam sendo instâncias dele e cada modus ponens continua sendo um modus ponens (o mesmo valerá para cada aplicação da regra nova). Assim, de $\vdash (\varphi \rightarrow \varphi)$ segue-se $\vdash (\neg\psi \rightarrow \neg\psi)$, com $\neg\psi$ em lugar de $\varphi$. Este recurso, aplicar um resultado a uma fórmula mais complexa que a do enunciado, é o que mais rende no que segue.

Do resultado à regra

As técnicas desta aula são demonstradas a partir de premissas fixas, como $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$; mas são usadas no meio de deduções com outras premissas, nas quais $(\varphi \rightarrow \psi)$ e $(\psi \rightarrow \chi)$ não são premissas, mas fórmulas já deduzidas. O lema seguinte, consequência direta da monotonicidade e do corte, autoriza esse uso de uma vez por todas.

Daí decorre que cada técnica demonstrada a partir de premissas tem três apresentações: o próprio resultado, o teorema que se obtém descarregando suas premissas e a regra que se aplica sob qualquer $\Gamma$. Em uma dedução sobre deduções, a regra é invocada com o nome da técnica e os números das linhas às quais se aplica, como SH$(3, 4)$, e o lema garante que o passo é legítimo.