As simetrias dos conectivos

O que se usa e o que é preciso demonstrar

A aula sobre os sistemas dedutivos formais fixou o sistema de Łukasiewicz: os axiomas A1, A2 e A3 e o modus ponens. Estabeleceu além disso a reflexividade (Refl: se $\varphi \in \Gamma$, então $\Gamma \vdash \varphi$), a monotonicidade (Mon), o corte (Corte: se $\Gamma \vdash \varphi_{i}$ para cada $i$ e $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, então $\Gamma \vdash \psi$), o teorema da dedução (TD) e sua recíproca (RTD) e a equivalência demonstrável, $\varphi \dashv\vdash \psi$, que significa que $\{\varphi\} \vdash \psi$ e $\{\psi\} \vdash \varphi$; e mostrou, com uma marca que os axiomas e o modus ponens conservam, que esse sistema não deduz certas fórmulas sobre a negação conjunta. A aula sobre as quatro técnicas de dedução acrescentou o silogismo hipotético (SH: $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$), o intercâmbio de premissas (IP), a dupla negação (DN: $\varphi \dashv\vdash \neg\neg\varphi$, com seus dois teoremas $\vdash (\neg\neg\varphi \rightarrow \varphi)$ e $\vdash (\varphi \rightarrow \neg\neg\varphi)$) e a contraposição (CP) em suas três formas:

Demonstrada a dupla negação, essa mesma aula completou o sistema do curso com uma segunda regra primitiva, a substituição da dupla negação (SDN): se $\chi'$ resulta de $\chi$ ao substituir uma ocorrência de uma subfórmula $\theta$ por $\neg\neg\theta$, ou uma ocorrência de uma subfórmula $\neg\neg\theta$ por $\theta$, então de $\chi$ se infere $\chi'$. A linha obtida assim da linha $i$ se justifica com SDN$(i)$. A partir desse ponto, $\vdash$ se refere ao sistema do curso (A1 a A3, o modus ponens e SDN), no qual continuam valendo Refl, Mon, Corte, TD e RTD. A regra atua sobre a cadeia da língua base, de modo que alcança também as ocorrências que uma abreviatura oculta, e em qualquer um dos dois argumentos de uma negação conjunta; entre suas consequências imediatas estão

e, em geral, $\chi \dashv\vdash \chi'$ sempre que $\chi'$ resulte de $\chi$ por SDN. Uma linha de equivalência dessa forma se justifica com “SDN”, sem número de linha, do mesmo modo que uma linha “DN” ou “CP” cita uma equivalência já demonstrada. Como lá, um teorema já demonstrado pode ser escrito como linha de uma dedução, porque sua própria dedução pode ser intercalada nesse lugar; e, pelo lema “do resultado à regra” daquela aula, cada técnica se aplica também como regra sob qualquer conjunto $\Gamma$ de premissas, citada com os números das linhas às quais se aplica, como CP$(i)$ ou SH$(i, j)$. Nas deduções sobre deduções, “Premissa” designa uma hipótese da regra que se demonstra.

As abreviaturas oficiais, fixadas na aula sobre a linguagem da lógica proposicional, são as únicas definições dos conectivos:

Uma linha justificada com “Def” não deduz nada: escreve a mesma fórmula com outro nome, e a anotação diz qual abreviatura se desdobra ou se recolhe (“Def $\rightarrow$”, “Def $\vee$”). Convém lembrar o fenômeno observado na aula sobre a formalização da linguagem natural: uma mesma fórmula admite vários nomes, de modo que uma conjunção é também, como cadeia, uma disjunção. Por exemplo, desdobrando a implicação com $\neg\varphi$ no lugar de $\varphi$, obtém-se

e a dupla negação que aparece diante de $\varphi$, oculta pela abreviatura, é a razão pela qual a regra SDN intervirá em tudo o que se segue.

A equivalência demonstrável como igualdade

As demonstrações desta aula são, quase todas, cadeias de equivalências: $\varphi_{1} \dashv\vdash \varphi_{2}$, $\varphi_{2} \dashv\vdash \varphi_{3}$, e assim sucessivamente. Para que de uma cadeia se conclua $\varphi_{1} \dashv\vdash \varphi_{n}$, a equivalência demonstrável deve comportar-se como uma igualdade, e é isso o que estabeleceu a proposição sobre as propriedades da equivalência demonstrável da aula sobre os sistemas dedutivos formais: a relação é reflexiva ($\varphi \dashv\vdash \varphi$), simétrica (se $\varphi \dashv\vdash \psi$, então $\psi \dashv\vdash \varphi$) e transitiva (se $\varphi \dashv\vdash \psi$ e $\psi \dashv\vdash \chi$, então $\varphi \dashv\vdash \chi$), e duas fórmulas demonstravelmente equivalentes são intercambiáveis como conclusões (se $\Gamma \vdash \varphi$ e $\varphi \dashv\vdash \varphi'$, então $\Gamma \vdash \varphi'$, para todo conjunto $\Gamma$ de fórmulas). Convém lembrar como se demonstraram as duas últimas, porque toda a aula repousa nelas: de $\{\varphi\} \vdash \varphi'$ passa-se, por monotonicidade, a $\Gamma \cup \{\varphi\} \vdash \varphi'$, e desta e de $\Gamma \vdash \varphi$, por corte, a $\Gamma \vdash \varphi'$; a transitividade resulta de aplicar isso com $\Gamma = \{\varphi\}$ num sentido e com $\Gamma = \{\chi\}$ no outro.

Daqui em diante, o passo que reúne uma cadeia de equivalências numa só se justifica com “Corte”, que é o instrumento dessa proposição. Ora, cada elo $\varphi_{i} \dashv\vdash \varphi_{i+1}$ contém as duas deduções, a de ida e a de volta; donde uma cadeia de equivalências demonstra ao mesmo tempo os dois sentidos de sua conclusão, e nada fica “como exercício”.