Provas em lógica proposicional

Uma tabela mostra que uma conclusão é consequência das premissas. Uma dedução mostra como chegar à conclusão com regras de inferência. Escrevemos $\Gamma\vdash\varphi$ quando existe uma dedução de $\varphi$ a partir das premissas $\Gamma$.

Na dedução natural, DN, podemos abrir hipóteses temporárias. Cada hipótese só sai através da regra que fecha a sua caixa; ao fechar, a conclusão deixa de depender dela. Esta gestão das hipóteses é tão necessária como escolher a conetiva certa.

Eliminação da implicação

De $p\to q$ e $p$, obtemos $q$ por eliminação da implicação, $\to E$:

1  p → q       premissa
2  p           premissa
3  q           →E, 1, 2

Se $p$ significa «há autorização» e $q$ significa «a porta abre», a regra usa a autorização e a condição que a liga à abertura. Só ter $p\to q$ não permite concluir $q$: falta garantir o antecedente.

Quando abres uma hipótese, anota o que queres obter antes de a fechar. Uma caixa fechada deixa de estar acessível; duas caixas abertas lado a lado são irmãs e não partilham linhas entre si.

Regras básicas

Cada conetiva tem regras de introdução, para a construir, e de eliminação, para a usar.

Regra	O que permite
$\land I$	De $\varphi$ e $\psi$, obter $\varphi\land\psi$.
$\land E$	De $\varphi\land\psi$, obter qualquer um dos membros.
$\lor I$	De $\varphi$, obter $\varphi\lor\psi$ ou $\psi\lor\varphi$.
$\lor E$	De $\varphi\lor\psi$ e duas subdeduções com a mesma conclusão $\theta$, uma assumindo $\varphi$ e outra $\psi$, obter $\theta$.
$\to E$	De $\varphi\to\psi$ e $\varphi$, obter $\psi$. É modus ponens.
$\to I$	Se assumir $\varphi$ permite deduzir $\psi$, fechar essa hipótese e obter $\varphi\to\psi$.
$F I$	De $\varphi$ e $\neg\varphi$, obter a contradição $F$.
$F E$	De $F$, obter qualquer fórmula.
$\neg I$	Se assumir $\varphi$ permite obter $F$, fechar a hipótese e obter $\neg\varphi$.
$\neg E$	De $\neg\neg\varphi$, obter $\varphi$.
$R$	Repetir uma fórmula que está acessível.

A regra $\neg E$ aqui é a eliminação da dupla negação, conforme a notação da cadeira. Não a confundas com $F I$. Usa as regras de base quando o enunciado não autorizar regras derivadas.

Notação de Fitch e âmbito

Numeramos as linhas, escrevemos a regra e indicamos as linhas usadas. A indentação e a barra vertical assinalam uma subdedução.

Vamos provar $(p\lor q)\to r\vdash p\to r$. A conclusão é uma implicação. Abrimos a hipótese $p$ e tentamos obter $r$:

1  (p ∨ q) → r       premissa
2  | p              hipótese
3  | p ∨ q          ∨I, 2
4  | r              →E, 1, 3
5  p → r            →I, 2 a 4

A linha 5 usa a subdedução inteira. Não afirma $r$ sem condições, afirma que $p$ permite obter $r$.

Depois de fechar a caixa, as linhas 2 a 4 não podem servir como premissas de outro passo exterior. Uma linha exterior pode ser usada dentro de uma caixa, mas uma conclusão de uma caixa fechada só sai através da regra que a fecha. Também não podes usar uma linha de uma caixa irmã.

Provar por casos

Queremos $(p\land q)\lor(q\land r)\vdash q$. Não sabemos qual dos membros da disjunção é verdadeiro. Provamos que ambos levam a $q$:

1  (p ∧ q) ∨ (q ∧ r)    premissa
2  | p ∧ q              hipótese do primeiro caso
3  | q                  ∧E, 2
4  | q ∧ r              hipótese do segundo caso
5  | q                  ∧E, 4
6  q                    ∨E, 1, 2 a 3, 4 a 5

A linha 4 abre uma nova caixa, não fica dentro da primeira. As duas caixas terminam com a mesma fórmula. Não podemos concluir $p$, porque só o primeiro caso o garante.

Quando um caso já começa com a conclusão pretendida, podemos repeti-la por $R$. Isto permite citar uma subdedução com início e fim explícitos.

Experimentar uma dedução

No editor, altera uma regra ou uma referência da prova por casos e observa o diagnóstico. O separador | --- fecha o primeiro caso antes de abrir o segundo.

Escolhe um exercício para construir uma prova a partir das primeiras linhas. Nos exercícios, as premissas e a conclusão ficam fixas. Em Prova livre, escreve as tuas próprias premissas e conclusão. Só as regras de base desta lição são aceites.

Negação e contradição

Para provar $p\to q,\neg q\vdash\neg p$, assumimos o contrário da negação que queremos introduzir, isto é, $p$:

1  p → q         premissa
2  ¬q            premissa
3  | p           hipótese
4  | q           →E, 1, 3
5  | F           FI, 2, 4
6  ¬p            ¬I, 3 a 5

Esta dedução justifica a regra derivada modus tollens, MT. A conclusão é $\neg p$, não $p$. Para provar uma fórmula positiva $p$ por absurdo, assumimos $\neg p$, obtemos $F$, concluímos $\neg\neg p$ por $\neg I$ e depois $p$ por $\neg E$. Estes dois últimos passos podem abreviar-se por RA quando a redução ao absurdo for permitida.

A partir de $F$ podemos concluir qualquer fórmula por $F E$. Isso é útil numa prova por casos: se um dos casos contradiz uma premissa, esse caso também permite obter a conclusão comum.

Contraposição e caixas encaixadas

Vamos provar $\neg q\to\neg p\vdash p\to q$. Primeiro introduzimos a implicação. Para obter $q$, tentamos uma redução ao absurdo:

1  ¬q → ¬p       premissa
2  | p           hipótese
3  | | ¬q        hipótese
4  | | ¬p        →E, 1, 3
5  | | F         FI, 2, 4
6  | ¬¬q         ¬I, 3 a 5
7  | q           ¬E, 6
8  p → q         →I, 2 a 7

Na linha 6 fechamos só a caixa de $\neg q$. A hipótese $p$ continua aberta até à linha 8. Por isso, a linha 7 ainda depende de $p$.

Escolher o próximo passo

Olha primeiro para a conetiva principal da conclusão:

• Para $\varphi\land\psi$, procura uma prova de cada membro e termina com $\land I$.
• Para $\varphi\to\psi$, assume $\varphi$ e procura $\psi$.
• Para $\neg\varphi$, assume $\varphi$ e procura uma contradição.
• Para $\varphi\lor\psi$, tenta provar um dos membros.

Depois olha para as premissas. Uma conjunção dá informação por $\land E$. Uma implicação pede o seu antecedente. Uma disjunção pode obrigar a uma prova por casos. Estes critérios orientam a procura; não são um algoritmo que dispense raciocínio.

Se a prova parece impossível, procura um contraexemplo semântico, porque nenhuma combinação correta das regras prova uma consequência falsa. Por exemplo, de $p\to q$ e $q$ não conseguimos obter $p$: $p=F,q=T$ satisfaz as premissas.

Correção e completude

Um sistema é correto se $\Gamma\vdash\varphi$ implica $\Gamma\models\varphi$. As regras não permitem passar de premissas verdadeiras a uma conclusão falsa.

É completo se $\Gamma\models\varphi$ implica $\Gamma\vdash\varphi$. Toda a consequência semântica tem uma dedução. A DN clássica usada aqui tem as duas propriedades. Isso não significa que encontrar uma prova seja imediato.

A equivalência dedutiva $\varphi\dashv\vdash\psi$ exige provas nos dois sentidos. Uma só dedução estabelece apenas uma direção. Para provar $\vdash(\varphi\to\psi)\land(\psi\to\varphi)$, abre e fecha uma subdedução para cada implicação, depois junta-as com $\land I$.