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.
\vdash \mathrm{p} \vee \neg \mathrm{p}

Passo 1

O enunciado pede para mostrar que a fórmula clássica da “terceira excluída” \r p \vee \neg p \r
é um teorema, ou seja, \r
\vdash p \vee \neg p \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
\neg\bigl(p \vee \neg p\bigr)\quad[1]\r
Em seguida, dentro desse contexto, suponha também\r
\neg p\quad[2]\r
Usando a regra de introdução de disjunção à direita (∨I), de \neg p inferimos\r
p \vee \neg p\quad(\vee I\text{ em }[2])

Passo 3

A partir de \neg\bigl(p \vee \neg p\bigr) [1] e de p \vee \neg p acabamos de obter, obtemos uma contradição:\r
\bot\quad(\neg E\text{ em }[1]\text{ e resultado de }[2])\r
Logo, pela regra de introdução de negação (¬I), descartando a hipótese [2], concluímos\r
\neg\neg p\quad(\neg I\text{; descarga de }[2])

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
p\quad(\neg\neg E\text{ em }\neg\neg p)

Passo 5

Com p em mãos, usamos de novo a introdução de disjunção, agora à esquerda, para obter\r
p \vee \neg p\quad(\vee I\text{ em }p)\r
Mas isso entra em contradição com a hipótese inicial \neg(p \vee \neg p) [1], gerando outra vez \bot. Portanto, aplicando ¬I e descartando a hipótese [1], concluímos\r
\neg\neg\bigl(p \vee \neg p\bigr)\quad(\neg I\text{; descarga de }[1])

Passo 6

Finalmente, outra aplicação da eliminação do duplo não nos dá a fórmula desejada sem hipóteses:\r
p \vee \neg p\quad(\neg\neg E)

Resposta

\vdash p \vee \neg p

Exercícios relacionados