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 mostrarmos que
no sistema de Dedução Natural (Gentzen). A ideia é assumir o antecedente
, derivar o consequente
por eliminação de
e
, e então usar introdução de
para fechar a prova.
Passo 2
Assuma
Pela eliminação de
extraímos
e .
e
Passo 3
Para eliminar a disjunção
, fazemos duas subprovas de eliminação de
:
Subprova 1:
Assuma .
Com e
, por introdução de
obtemos
Então, por introdução de
à esquerda, concluímos
Assuma
Com
Fim da Subprova 1.
Subprova 2:
Assuma .
Com e
, por introdução de
obtemos
Então, por introdução de
à direita, concluímos
Assuma
Com
Fim da Subprova 2.
Passo 4
Agora aplicamos eliminação de
sobre a fórmula
usando as conclusões das duas subprovas. Dessa forma inferimos diretamente
Passo 5
Descarregamos a suposição inicial
e aplicamos introdução de
. Assim concluímos