Dê uma prova formal para cada argumento:
Questão-07. As deduções estão corretas. Apenas forneça as justificativas em cada etapa da dedução
c) Deduzir (forall x)(forall y)(Ax wed>= Dxy Cy) das premissas P-1 e P-2
  1. P-1(forall x)(Ax (forall y)(Bxy Cy))
  2. P-2(forall x)(Ax (forall y)(Dxy Bxy))
  3. Ax wed>= Dxy
  4. Ax (forall y)(Bxy Cy)
  5. Ax ( forall y )(Dxy Bxy)
  6. (forall y)(Bxy Cy)
  7. ( forall y )(Dxy Bxy)
  8. Bxy Cy
  9. Dxy Bxy
  10. Bxy
  11. Cy
  12. Ax wed>= Dxy Cy
  13. (forall y)(Ax wed>= Dxy Cy)
  14. (forall x)(forall y)(Ax wed>= Dxy Cy)

Passo 1

Resumindo, queremos derivar
forall xforall y,(Axwed>= Dxy Cy)
a partir das premissas
P-1: forall x,(Ax forall y,(Bxy Cy))
P-2: forall x,(Ax forall y,(Dxy Bxy))
Usaremos regras de lógica de predicados: instanciação universal (UI), eliminação de conjunção ( landE), modus ponens ( toE), introdução de implicação ( toI) e generalização universal (UG).

Passo 2

De P-1 por Instanciação Universal obtemos a implicação
Ax forall y,(Bxy Cy)

Passo 3

De P-2 por Instanciação Universal obtemos a implicação
Ax forall y,(Dxy Bxy)

Passo 4

Suponha arbitrários x e y e assuma
Axwed>= Dxy
para deduzir Cy.

Passo 5

De Axwed>= Dxy por landE obtemos as fórmulas
,Ax e ,Dxy.

Passo 6

De Ax e de Ax forall y,(Bxy Cy) por toE segue
forall y,(Bxy Cy)

Passo 7

De forall y,(Bxy Cy) por UI extraímos
Bxy Cy

Passo 8

De Ax e de Ax forall y,(Dxy Bxy) por toE segue
forall y,(Dxy Bxy)

Passo 9

De forall y,(Dxy Bxy) por UI extraímos
Dxy Bxy

Passo 10

De Dxy e Dxy Bxy por toE obtemos
Bxy

Passo 11

De Bxy e Bxy Cy por toE obtemos
Cy

Passo 12

Descarregando a suposição Axwed>= Dxy por toI inferimos
Axwed>= Dxy Cy

Passo 13

Generalizando em y por UG, obtemos
forall y,(Axwed>= Dxy Cy)

Passo 14

Generalizando em x por UG, obtemos
forall xforall y,(Axwed>= Dxy Cy)

Resposta

forall xforall y,(Axwed>= Dxy Cy)

Exercícios relacionados