-
Construa uma prova formal de validade para os argumentos e formas de argumentos a seguir.
Todos os advogados são ricos. Alguns poetas são advogados. Logo, existem poetas ricos.
- \forall x(A x \rightarrow R x)
- \exists x(P x \cap A x)
- \therefore \exists x(P x \wedge R x)
- P_{a} \wedge A a exemelificasós existencial em 2.
- Ao → Ra exemplizicapa universal em 1 .
- Pa simplificacha em 4.
- Aa simplificacia em 4.
- Ra madus panens em Seq .
- Panka conjuncás em 6 e 8.
- \exists x(P x \wedge R x) generacizagão existencial em 9).
c.q.p.
Todos os advogados são ricos. Alguns poetas são advogados. Logo, existem poetas ricos.
c.q.p.
Passo 1
O enunciado nos dá claramente três itens: duas premissas e a conclusão que se quer mostrar. Vou listar cada um tal como estão (peguei estes enunciados do problema):
- Premissa 1:
. - Premissa 2:
. - Conclusão desejada:
.
O que o problema pede: construir uma prova formal (em dedução natural ou sistema equivalente) que, a partir de
e
, se derive
. Não vou resolver nada ainda neste passo, apenas enumerei o dado e o pedido.
Passo 2
Vou usar como ferramenta a regra de eliminação do existencial (existential instantiation): a partir de
podemos introduzir um novo símbolo de constante — chamarei de
— e assumir
temporariamente, desde que
seja um nome novo (ou “fresh”), i.e., não aparece em nenhuma premissa nem na conclusão. Aplicando essa regra à premissa 2, obtemos:
Explicação da regra: \emph{Existential Instantiation} permite “pegar” uma testemunha hipotética
tal que a fórmula existencial seja verdadeira; depois pode-se derivar consequências dessa hipótese e, no fim, usar essas consequências para formar uma conclusão cujo único vínculo com
seja re-expressável como existencial. É essencial que
seja novo para evitar falsos argumentos por dependência de nomes já usados.
Passo 3
Da conjunção
(obtida no passo anterior) aplico a regra de eliminação da conjunção (simplificação) para obter cada um dos conectivos separadamente. Primeiro:
Explicação da regra: se se sabe
, então podemos inferir
(e também
). É uma regra básica: cada parte da conjunção é verdadeira.
Passo 4
Usando novamente eliminação da conjunção sobre
, obtenho:
Ou seja, tiramos a segunda conjuncta. Isso é análogo ao passo anterior.
Passo 5
Da premissa universal
aplico a eliminação do universal (universal instantiation) substituindo
por
. Assim obtenho:
Explicação da regra: \emph{Universal Instantiation} permite, de
, inferir
para qualquer termo
(aqui usamos o termo constante
). Ou seja, a implicação vale para todo indivíduo, logo vale para o representante concreto
.
Passo 6
Agora aplico modus ponens (eliminação da implicação) usando
(Passo 4) e
(Passo 5). Assim obtenho:
Explicação da regra: modus ponens diz que de
e
se pode inferir
.
Passo 7
Com
(Passo 3) e
(Passo 6) posso formar a conjunção:
Aplicação da regra de introdução da conjunção: se se tem
e
, então se pode inferir
.
Passo 8
Finalmente, aplico a introdução do existencial (existential introduction): a partir de
concluo
Explicação da regra: se
é verdadeira para algum termo
, então podemos inferir
. Aqui
é
e
é
.
Passo 9
Comentário sobre a correção da prova: a única sutileza técnica estava em garantir que o símbolo
usado na instanciação existencial fosse novo (não aparecia em nenhuma premissa nem na conclusão). Assim não houve dependência indevida e a aplicação da eliminação do existencial seguida de introdução do existencial é legítima na dedução natural. Todos os passos usados (eliminação do existencial por testemunha nova, eliminação da conjunção, eliminação do universal, modus ponens, introdução da conjunção, introdução do existencial) são regras padrão e foram aplicadas na ordem correta, portanto a conclusão está corretamente derivada das premissas.