- Prove a validade com o sistema axiomático A , convertendo a fórmula antes:
Passo 1
O enunciado pede para provar no sistema axiomático A a validade da fórmula
sabendo que, nesse sistema, os conectivos primitivos são
e
e a conjunção é dada por abreviação
Vamos usar os axiomas de conjunção e modus ponens junto com o esquema de dedução de implicação (axioma
) para montar a prova.
Passo 2
Listemos os axiomas de conjunção que usamos (Mendelson, p. 31–32):
e o axioma
(distribuição da implicação):
Passo 3
Aplique
com
e
. Obtemos
Passo 4
Aplique
com
e
. Obtemos
Passo 5
Aplique
com
e
. Obtemos
Passo 6
Agora usamos o axioma
para combinar o resultado de Passo 4 com
de Passo 5. Instancie
com
de modo que
Mas
é exatamente a fórmula de Passo 5 depois de trocar
por
. Logo, por modus ponens com Passo 5, segue
Passo 7
Finalmente usamos
de novo para combinar o resultado do Passo 6 com o de Passo 3. Instancie
com
obtendo
Aplicando modus ponens primeiro com o teorema de Passo 6 e depois com o de Passo 3, conclui-se
Resposta
A fórmula
é demonstrável no sistema axiomatico A conforme o encadeamento acima.