Demonstre que as fórmulas abaixo são teoremas. Para as provas, você pode escolher entre o Sistema Axiomático de Hilbert, utilizando apenas os axiomas apresentados em sala e a regra do modus ponens(MP) ou o Sistema de Dedução Natural no estilo de Gentzen.
Passo 1
O enunciado pede para mostrar que a fórmula clássica da “terceira excluída” \r
\r
é um teorema, ou seja, \r
é um teorema, ou seja, \r
Vamos usar o Sistema de Dedução Natural (estilo Gentzen) em lógica clássica, valendo-nos das regras de introdução e eliminação de negação, da introdução de disjunção e, crucialmente, da eliminação do duplo não (princípio clássico).
Passo 2
Iniciamos com uma prova por contradição da fórmula inteira. Suponha:\r
Em seguida, dentro desse contexto, suponha também\r
Usando a regra de introdução de disjunção à direita (∨I), de
inferimos\r
Passo 3
A partir de
[1] e de
acabamos de obter, obtemos uma contradição:\r
Logo, pela regra de introdução de negação (¬I), descartando a hipótese [2], concluímos\r
Passo 4
Agora aplicamos a eliminação do duplo não (¬¬E), disponível em lógica clássica, para retirar as duas negações e chegar a:\r
Passo 5
Com
em mãos, usamos de novo a introdução de disjunção, agora à esquerda, para obter\r
Mas isso entra em contradição com a hipótese inicial
[1], gerando outra vez
. Portanto, aplicando ¬I e descartando a hipótese [1], concluímos\r
Passo 6
Finalmente, outra aplicação da eliminação do duplo não nos dá a fórmula desejada sem hipóteses:\r