Métodos de prova

Cinco rotas para o mesmo destino — e por que a escolha importa.

Dois alunos recebem o mesmo enunciado: demonstrar que se $n^2$ é par, então $n$ é par. O primeiro diz: "Vou assumir que $n^2$ é par e que $n$ é ímpar, e chegar a uma contradição." O segundo diz: "Vou assumir que $n$ é ímpar e mostrar que $n^2$ é ímpar." Ambos chegam a uma prova correta — mas por rotas formalmente distintas. A diferença não é estilística. Uma tem um alvo específico desde a primeira linha; a outra, não.

Cada rota tem um nome, uma condição de uso, e uma mesma raiz: todas são instâncias das regras de inferência sobre os conectivos $\rightarrow$, $\vee$ e $\neg$.

§1. O que é uma prova

Uma prova é uma derivação: uma sequência de proposições onde cada linha segue das anteriores por uma regra de inferência, ou é uma hipótese assumida explicitamente e identificada como tal. Aristóteles formalizou o silogismo; os estoicos enumeraram cinco regras básicas. Em 1934, Gentzen e — independentemente — Jaśkowski sistematizaram o que hoje chamamos dedução natural.

Na dedução natural, cada conectivo tem um par de regras:

• Regra de introdução — como construir uma proposição com esse conectivo.
• Regra de eliminação — como usar uma proposição com esse conectivo.

Prova condicional, contrapositiva, redução ao absurdo e análise de casos são instâncias dessas regras aplicadas a $\rightarrow$, $\vee$, e $\neg$.

§2. Prova condicional

A regra mais usada em toda a matemática. Para provar $P \rightarrow Q$:

Assuma $P$. Derive $Q$. A condicional está demonstrada.

Em dedução natural, essa é a regra $\rightarrow$-Introdução. A hipótese $P$ fica disponível dentro do bloco de prova e é descarregada na conclusão: ela deixa de ser um pressuposto solto e passa a ser o antecedente da condicional provada.

Exemplo. Se $n$ é par, então $n^2$ é par.

Assuma $n$ par. Por definição, $n = 2k$ para algum inteiro $k$. Então:

$n^2 = (2k)^2 = 4k^2 = 2(2k^2)$

Logo $n^2$ é par. $\square$

O símbolo $\square$ — o tombstone de Paul Halmos (1973) — marca o fim de uma prova. Substitui o latino Q.E.D. (quod erat demonstrandum).

A estrutura é direta: a hipótese entra, a conclusão sai. No registro computacional, isso é uma função — e não coincidentemente. Uma prova de $P \rightarrow Q$ é exatamente uma função que, dado um termo do tipo $P$, retorna um termo do tipo $Q$:

def prova_par_implica_quadrado_par(n: int) -> int:
    # hipótese: n é par, i.e., n = 2k para algum k
    k = n // 2
    return 4 * k * k  # n² = 2(2k²), logo par

Erro frequente. Assumir o que se quer provar. "Assuma que $n^2$ é par. Então $n$ é par. Logo $n^2$ par implica $n$ par." Isso é petição de princípio — a conclusão foi usada como hipótese disfarçada.

§3. Análise de casos

Quando a informação disponível tem a forma $P \vee Q$, a única rota é tratar cada alternativa em separado. A regra $\vee$-Eliminação:

Se $P \vee Q$, e $R$ segue de $P$, e $R$ segue de $Q$, então $R$.

Os dois ramos precisam convergir para a mesma conclusão $R$. Não é possível concluir coisas diferentes em cada caso — a disjunção não revela qual alternativa é verdadeira, apenas que pelo menos uma é.

Exemplo. Para todo inteiro $n$, $n^2 \geq 0$.

Todo inteiro é não-negativo ou negativo: $n \geq 0$ ou $n < 0$.

• Caso 1: $n \geq 0$. Então $n^2 = n \cdot n \geq 0$.
• Caso 2: $n < 0$. Então $-n > 0$, e $n^2 = (-n)^2 > 0$.

Em ambos os casos, $n^2 \geq 0$. $\square$

A disjunção usada não precisa estar na hipótese original. É possível introduzir o terceiro excluído $P \vee \neg P$ a qualquer momento — ele é uma tautologia — e dividir a prova nos dois casos. Essa técnica aparece em provas que tratam $n$ par e $n$ ímpar como casos separados sem que o enunciado mencione paridade.

No registro computacional, $\vee$-Eliminação é um match sobre um tipo soma:

from typing import Union
 
def prova_usando_P_ou_Q(hipotese: Union[P, Q]) -> R:
    match hipotese:
        case P():
            return prova_R_de_P(hipotese)
        case Q():
            return prova_R_de_Q(hipotese)

Erro frequente. Verificar apenas um dos casos. Se $n^2 \geq 0$ fosse demonstrado somente para $n \geq 0$, a prova estaria incompleta — o caso $n < 0$ permaneceria aberto.

§4. Contrapositiva

$P \rightarrow Q$ é logicamente equivalente a $\neg Q \rightarrow \neg P$. Isso é uma tautologia:

Quando provar a direção original é difícil, pode ser mais fácil provar a contrapositiva. O método tem um alvo específico: assuma $\neg Q$, derive $\neg P$.

Exemplo. Se $n^2$ é par, então $n$ é par.

Prove a contrapositiva equivalente: se $n$ é ímpar, então $n^2$ é ímpar.

Assuma $n$ ímpar. Então $n = 2k + 1$ para algum inteiro $k$. Assim:

$n^2 = (2k+1)^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1$

Logo $n^2$ é ímpar. $\square$

A prova pela contrapositiva é estruturalmente uma prova condicional — assume a hipótese $\neg Q$ e deriva $\neg P$ diretamente. O que muda é apenas qual condicional escolhemos provar.

§5. Redução ao absurdo

Para provar $P$:

Assuma $\neg P$. Derive uma contradição. Conclua $P$.

Uma contradição é um par de proposições $B$ e $\neg B$ simultaneamente deriváveis. O símbolo $\bot$ — bottom, lido falso ou absurdo — é a proposição falsa em todo caso: o piso abaixo de todas as proposições, oposto da tautologia $\top$. Formalmente, $\bot$ não tem regra de introdução — nada o constrói diretamente. Tem apenas uma regra de eliminação:

É por isso que uma contradição destrói a prova: dela, tudo e o contrário de tudo são deriváveis.

Exemplo. Não existe inteiro maior que todos os outros inteiros.

Suponha, para contradição, que existe tal inteiro $M$. Considere $M + 1$. Por definição de adição em $\mathbb{Z}$, $M + 1 > M$. Mas $M$ era, por hipótese, maior que todo inteiro — inclusive $M + 1$. Contradição. Logo não existe tal $M$. $\square$

O alvo é não-específico. Ao assumir $\neg P$, não sabemos de antemão qual contradição vai aparecer. Qualquer $B$ e $\neg B$ servem. Isso dá liberdade — mas também menos direção do que a contrapositiva. Quando a prova começa com "suponha que $n^2$ é par e $n$ é ímpar", não está claro imediatamente onde a contradição vai surgir.

Diferença com a contrapositiva — em resumo. Para provar $P \rightarrow Q$:

• Contrapositiva: assuma $\neg Q$; derive $\neg P$. Alvo fixo.
• Redução ao absurdo: assuma $P \wedge \neg Q$; derive qualquer $\bot$. Alvo livre.

A contrapositiva é sempre uma prova direta na direção invertida. A redução ao absurdo é uma prova indireta: não construímos $P$ — eliminamos $\neg P$.

Nota sobre a lógica clássica. Na forma plena — assumir $\neg P$, derivar $\bot$, concluir $P$ — a redução ao absurdo é uma regra clássica, equivalente ao terceiro excluído e à dupla negação. A lógica intuicionista admite introdução de negação (assumir $P$, derivar $\bot$, concluir $\neg P$) mas rejeita a versão que elimina uma negação. Ver lógicas não-clássicas.

§6. A escolha do método depende da forma do problema

A escolha do método depende da forma da proposição a provar e da informação disponível:

• Se a conclusão é uma condicional e a rota direta é clara: prova condicional.
• Se negar a conclusão fornece informação útil que facilita a derivação: contrapositiva.
• Se não há rota direta visível e assumir o contrário produz tensão com o que já se sabe: redução ao absurdo.
• Se a hipótese disponível é uma disjunção, ou a prova exige separar casos: análise de casos.

Esses métodos se compõem. A prova da irracionalidade de $\sqrt{2}$ usa redução ao absurdo como moldura e prova condicional internamente. Uma prova de paridade usa análise de casos para separar pares e ímpares e prova condicional dentro de cada ramo.

§7. Registro computacional

O isomorfismo de Curry-Howard, já visto em lógica proposicional e lógica de predicados, vale aqui apenas para a lógica intuicionista. A redução ao absurdo clássica não tem análogo direto.

from typing import Never
 
# ex falso quodlibet: de ⊥, qualquer coisa
def ex_falso(absurdo: Never) -> object:
    raise AssertionError("nunca alcançado")
 
# análise de casos sobre P | Q
def por_casos(hipotese: P | Q) -> R:
    match hipotese:
        case P():
            return prova_de_P(hipotese)
        case Q():
            return prova_de_Q(hipotese)

A lógica intuicionista é a lógica da computação: cada prova é um programa, cada proposição um tipo, cada derivação um termo que pode ser executado. A lógica clássica estende isso com um operador de controle — mas o preço é perder a correspondência direta entre provar e computar.

Esses quatro métodos — prova condicional, análise de casos, contrapositiva, redução ao absurdo — são os instrumentos com que toda a matemática que segue é construída. O próximo passo é ver esses instrumentos em ação nos módulos de conjuntos e funções, onde as provas deixam de ser exercícios e passam a ser o tecido das definições.