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
Isso é a comutatividade da disjunção em lógica proposicional. Vamos usar Dedução Natural no estilo Gentzen, com as regras de introdução e eliminação de
e de introdução de
.
Passo 2
Para provar
por introdução de
, assumimos temporariamente
e a partir dessa hipótese vamos deduzir
.
Passo 3
Aplicamos prova por casos usando eliminação de
. Primeiro caso: suponha
Então, pela regra de introdução de
(que permite inferir
a partir de
), obtemos
Passo 4
Segundo caso: suponha
Então, novamente pela introdução de
, obtemos
Passo 5
Agora aplicamos eliminação de
à hipótese
. A regra diz que, se temos
, se de
podemos derivar
e de
também podemos derivar
, então inferimos
Passo 6
Por fim, descarregamos a hipótese
usando introdução de
. Como de
chegamos a
, concluímos