Aprender dedução natural

Uma prova parte das premissas e chega à conclusão por passos pequenos, cada um justificado por uma regra. Em notação de Fitch, cada linha diz a fórmula, a regra que a permite e as linhas em que essa regra se apoia. Se todas as linhas estiverem certas, a conclusão segue das premissas.

O que queres provar escreve-se como um sequente, por exemplo a ∧ b, a → c ⊢ c ∧ b. À esquerda de ⊢ ficam as premissas, separadas por vírgulas, e à direita a conclusão. Sem nada à esquerda, como em ⊢ a → a, a fórmula tem de sair só das regras, e diz-se um teorema.

Para poupar parênteses, ¬ liga mais do que tudo, ∧ e ∨ ligam mais do que →, uma cadeia de ∧ agrupa à esquerda e uma de → agrupa à direita. Assim, a → b ∧ c é a → (b ∧ c), a ∧ b ∧ c é (a ∧ b) ∧ c e a → b → c é a → (b → c). O site mostra sempre a forma curta.

Avança pela prova abaixo, linha a linha, e repara no que cada justificação cita.

Nenhuma destas linhas pede que saibas o que a, b ou c querem dizer. Uma regra aplica-se se as fórmulas citadas tiverem a forma que ela exige, seja qual for o assunto. É por isso que uma prova se confere à mão ou por programa, sem discutir o significado de nada.

Cada conectivo traz dois tipos de regra. A de introdução, marcada com I, diz como chegar a uma fórmula com esse conectivo. A de eliminação, marcada com E, diz o que podes tirar de uma fórmula que já o tem. Nas secções seguintes vês, para cada regra, o esquema, em que φ e ψ valem por quaisquer fórmulas, um exemplo e o engano mais frequente.

A conjunção é o melhor sítio para começar: φ ∧ ψ afirma as duas fórmulas, por isso há uma regra para as juntar e outra para as separar.

A regra de eliminação olha só para o conectivo principal da linha citada. Em a ∧ b ∧ c, que é (a ∧ b) ∧ c, os dois lados são a ∧ b e c. Cada ∧E retira uma camada, e o exemplo acima gasta uma linha por camada.

Uma implicação φ → ψ é uma promessa: sempre que tiveres φ, tens ψ. Usá-la é uma troca direta. Arranjas φ e recebes ψ, sem mais nada a fazer.

Uma implicação não afirma φ nem afirma ψ. Só exclui o caso em que φ é verdadeira e ψ é falsa. Por isso, ter φ → ψ numa linha não te dá nenhuma das duas fórmulas, e é preciso obter φ por outro caminho antes de aplicar a regra.

Falta saber como se chega a uma implicação. Isso pede uma ferramenta nova, a subdedução, que é o tema da secção seguinte.

Para provar φ → ψ, não precisas de saber se φ é verdadeira. Supões φ, só para ver no que dá, e mostras que daí se chega a ψ. A suposição abre uma subdedução: uma prova dentro da prova, com barra própria e com a hipótese na primeira linha.

Uma subdedução cita-se como intervalo, da hipótese até à última linha, por exemplo 3–6. Se tiver uma só linha, o intervalo começa e acaba nela, como 1–1 em ⊢ a → a, onde a hipótese a é logo a última linha.

Tudo o que escreves dentro de uma subdedução pode depender da hipótese, por isso só vale enquanto ela estiver em vigor. Quando a subdedução fecha, a hipótese deixa de contar, e as linhas de dentro já não se podem citar uma a uma. Resta o intervalo completo, que é o que a regra →I usa.

No sentido contrário não há problema: de dentro de uma subdedução podes citar diretamente as linhas exteriores que estão acima, sem as repetir. A prova só termina numa linha fora de todas as subdeduções.

As subdeduções também podem ficar umas dentro das outras. A mais recente é a primeira a fechar. Segue esta prova, em que cada →I fecha uma hipótese, a de dentro antes da de fora.

Sobra um caso. A subdedução tem de acabar na fórmula que queres, e essa fórmula pode já estar escrita lá fora. Citá-la não basta, porque ela tem de aparecer como última linha. É para isso que serve R: repete uma fórmula numa linha nova.

Para chegar a φ ∨ ψ basta uma das fórmulas. Usar uma disjunção dá mais trabalho: não sabes qual delas é verdadeira, por isso tratas os dois casos.

A fórmula que acrescentas com ∨I pode ser qualquer uma, até uma que não apareça em mais lado nenhum. O preço é perder informação: de a passas a saber só que a ou b é verdadeira. Por isso, ∨I costuma ser o último passo, quando já sabes qual dos lados consegues provar.

Em ∨E, cada caso é uma subdedução separada, e o que escreves num não se pode citar no outro. A conclusão pode nem falar de φ nem de ψ. Só tem de ser a mesma fórmula na última linha dos dois casos, e é essa que passa para fora.

Negar φ é mostrar que φ leva a uma contradição, que se escreve F. É aqui que entram ¬I, ¬E, FI e FE.

F é uma fórmula como as outras, mas nunca é verdadeira. Noutros textos aparece como ⊥, e aqui também a podes escrever assim, embora o site mostre sempre F. A maneira habitual de lá chegar é a regra FI.

Com F já se pode negar. A regra ¬I segue a ideia da abertura: supões φ, chegas a F e concluis que φ não pode ser verdadeira.

A eliminação faz muito pouco: tira duas negações seguidas, e mais nada. Não há regra que te dê φ a partir de ¬φ, porque as duas fórmulas dizem o contrário uma da outra.

Falta FE. De uma contradição podes escrever qualquer fórmula. Parece estranho, mas uma linha com F só aparece numa situação impossível, onde já nada há a distinguir. É sobretudo útil em ∨E: um caso que contradiz o resto acaba em F, e FE faz com que dê a fórmula a que o outro caso chega.

Algumas provas repetem sempre o mesmo padrão. As regras derivadas dão-lhe um nome, e cada uma delas pode ser substituída por uma prova só com regras base.

Uma regra derivada não te deixa provar nada de novo. Encurta o que já consegues provar. Cada figura traz o esquema, o momento certo para a usar e uma prova só com regras base. Essas provas estão escritas com p, q e r, mas valem para quaisquer fórmulas no lugar de φ, ψ e θ: basta trocar as letras.

Numa prova, uma derivada usa-se como qualquer outra regra: escreves a sigla e citas as linhas. Com MT, esta prova faz em duas linhas o que, só com regras base, pediria duas subdeduções.

A forma da conclusão e das premissas costuma dizer qual é o passo seguinte. Estas são as perguntas a fazer quando não sabes por onde continuar.

Começa pela conclusão. A forma dela diz como a prova costuma acabar, e isso dá-te um objetivo mais pequeno:

• Se é φ ∧ ψ, prova cada lado e junta-os com ∧I.
• Se é φ → ψ, supõe φ e procura ψ. No fim, fecha com →I.
• Se é ¬φ, supõe φ e procura F. No fim, fecha com ¬I.
• Se é φ ∨ ψ, vê se consegues provar um dos lados e acaba com ∨I. Às vezes nenhum lado sai sozinho, e aí a resposta está nas premissas.

Repete a pergunta para cada objetivo novo. Reproduz a prova abaixo, ou avança à mão, e lê a razão de cada linha.

Depois de cada estratégia há um laboratório, com um sequente para provares aqui mesmo. Abre no modo guiado: tocas nas linhas que queres citar e escolhes a regra. Se preferires escrever, muda de modo no topo do editor.

Quando a conclusão já não ajuda, olha para o que tens. Cada linha acessível oferece alguma coisa:

• De φ ∧ ψ, tira os dois lados com ∧E. Não custa nada e dá-te mais linhas para citar.
• De φ → ψ, tenta obter φ, porque depois tens ψ com →E.
• De φ ∨ ψ, abre os dois casos com ∨E e procura o mesmo objetivo em ambos. Faz isto cedo: dentro de cada caso tens mais uma linha para usar.
• Com ¬φ, procura φ. Se o conseguires, FI dá-te F.

Se nada disto chegar, resta a redução ao absurdo. Supõe a negação do objetivo e procura F. Ganhas uma linha para usar, e a contradição costuma sair de uma premissa negada. Fica para o fim porque a prova sai mais longa e menos direta.

Se continuares preso, pode acontecer que a prova não exista. A secção seguinte explica como o mostrar.

Fica a pergunta de fundo: o que consegues provar coincide com o que é verdadeiro em todas as valorações? A solidez e a completude dizem que sim.

Até aqui, tudo foi sintaxe: ⊢ quer dizer que há uma prova. A outra noção vem das tabelas de verdade. Uma valoração dá verdadeiro ou falso a cada variável, e escreve-se ⊨ quando todas as valorações que tornam as premissas verdadeiras também tornam a conclusão verdadeira.

A solidez diz que, se há prova, o sequente é válido: de ⊢ segue ⊨. A razão está nas regras, porque cada uma preserva a verdade. Se o que ela cita é verdadeiro, o que ela escreve também é. Dentro de uma subdedução vale o mesmo, para as valorações que tornam as hipóteses abertas verdadeiras. Como uma prova é uma cadeia destes passos, a verdade das premissas chega à conclusão.

Isto dá-te uma forma de mostrar que não há prova, sem as experimentar todas. Basta uma valoração com as premissas verdadeiras e a conclusão falsa, a que se chama contraexemplo.

A completude é o sentido contrário: se o sequente é válido, há prova. De ⊨ segue ⊢. É a parte difícil, porque diz que as regras não deixam nada de fora. A demonstração sai do âmbito desta lição, mas a ideia é esta: quando uma conclusão não se prova, consegue construir-se uma valoração que serve de contraexemplo.

Nenhuma das duas é automática, porque dependem das regras escolhidas. Se tirares ¬E às regras base, por exemplo, a ∨ ¬a continua verdadeira em todas as valorações e deixa de ter prova.

Juntas, as duas dizem que ⊢ e ⊨ coincidem. Cada sequente tem uma prova ou um contraexemplo, nunca os dois. A completude diz só que a prova existe, não que seja curta nem fácil de encontrar, e é para isso que servem as estratégias.