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
a) Deduzir (forall z)(Az neg Cz) das premissas P-1 e P-2
  1. P-1(forall x)(Ax Bx)
  2. P-2(forall y)(Cy neg By)
  3. Az
  4. Az Bz
  5. Bz
  6. Cz neg Bz
  7. neg Cz
  8. Az neg Cz
  9. (forall z)(A z neg C z)
    b) Deduzir (forall x)(Ax Dx) das premissas P-1, P-2 e P-3
  10. P-1(forall x)(Ax wed>= Bx Cx)
  11. P-2(forall x)(Bx neg Cx vee Dx)
  12. P-3(forall x)(Ax Bx)
  13. A x wed>= neg D x
  14. Ax Bx
  15. Bx
  16. Ax wed>= Bx
  17. Ax wed>= Bx Cx
  18. Cx
  19. Cx wed>= neg Dx
  20. neg(neg Cx vee Dx)
  21. Bx neg Cx vee Dx )
  22. neg Bx
  23. Bx wed>= neg Bx
  24. neg(Ax wed>= neg Dx)
  25. Ax Dx
  26. (forall x)(Ax Dx)
    c) Deduzir (forall x)(forall y)(Ax wed>= Dxy Cy) das premissas P-1 e P-2
  27. P-1(forall x)(Ax (forall y)(Bxy Cy))
  28. P-2(forall x)(Ax (forall y)(Dxy Bxy))
  29. Ax wed>= Dxy
  30. Ax (forall y)(Bxy Cy)
  31. Ax ( (forall y )(Dxy Bxy)
  32. (forall y)(Bxy Cy)
  33. ( (forall y )(Dxy Bxy)
  34. Bxy Cy
  35. Dxy Bxy
  36. Bxy
  37. Cy
  38. Ax wed>= Dxy Cy
  39. (forall y)(Ax wed>= Dxy Cy)
  40. (forall x)(forall y)(Ax wed>= Dxy Cy)

Passo 1

Temos as premissas
(forall x)(A x B x)
e
(forall y)(C y neg B y)
e queremos deduzir
(forall z)(A z neg C z)
O conteúdo é cálculo de predicados: usaremos instanciacão universal (UI), eliminação de implicação ( toE), introdução de negação ( neg I), introdução de implicação ( toI) e introdução universal ( forallI).

Passo 2

Instanciamos a primeira premissa com z:
A z B z (de (forall x)(A x B x) por UI)
Instanciamos a segunda premissa com z:
C z neg B z (de (forall y)(C y neg B y) por UI)

Passo 3

Assumimos (para introdução de implicação):
De e obtemos por E.

Passo 4

Assumimos C z (para introdução de negação):
[C z] (assump para neg I)
De C z e C z neg B z obtemos neg B z por toE.

Passo 5

De B z e neg B z obtemos contradição bot.

Passo 6

Das assunções C z que levam a bot introduzimos neg C z por neg I, dispensando a assunção de C z.
Das assunções A z que levaram a neg C z inferimos
A z neg C z
por toI, dispensando a assunção de A z.

Passo 7

Por forallI, como z é arbitrário e não aparece em hipótese aberta, concluímos
(forall z)(A z neg C z)

Passo 8

Temos as premissas
(forall x)(A x wed>= B x C x), (forall x)(B x neg C x vee D x), (forall x)(A x B x),
e queremos deduzir
(forall x)(A x D x)
Usaremos UI, landE, landI, toE, eliminação de disjunção, neg I, negneg E, toI e forallI.

Passo 9

Instanciamos cada premissa com x:
A x wed>= B x C x (UI)
B x neg C x vee D x (UI)
A x B x (UI)

Passo 10

Assumimos A x (para toI):
[A x]
Assumimos neg D x (para neg I):
[neg D x]

Passo 11

De A x e A x B x obtemos B x por toE.
De A x e B x formamos A x wed>= B x por landI.

Passo 12

De A x wed>= B x e A x wed>= B x C x obtemos C x por toE.
De B x e B x neg C x vee D x obtemos neg C x vee D x por toE.

Passo 13

De neg C x vee D x e neg D x (eliminação de disjunção com casos) inferimos neg C x.
De C x e neg C x obtemos contradição bot.

Passo 14

Da assunção neg D x que leva a bot introduzimos negneg D x por neg I.
De negneg D x inferimos D x por negneg E.

Passo 15

Das assunções A x que levam a D x introduzimos
A x D x
por toI, dispensando a assunção A x.
Por forallI, como x é arbitrário, concluímos
(forall x)(A x D x)

Passo 16

Temos as premissas
(forall x)l(A x (forall y)(B x y C y)r), (forall x)l(A x (forall y)(D x y B x y)r),
e queremos deduzir
(forall x)(forall y)(A x wed>= D x y C y)
Vamos usar UI, landE, toE, toI, forallI.

Passo 17

Instanciamos cada premissa com x:
A x (forall y)(B x y C y) (UI)
A x (forall y)(D x y B x y) (UI)

Passo 18

Assumimos A x wed>= D x y (para toI e forall introd.):
[A x wed>= D x y]

Passo 19

De A x wed>= D x y obtemos A x por landE.
De A x e A x (forall y)(B x y C y) obtemos
forall y)(B x y C y) por toE.
De A x e A x (forall y)(D x y B x y) obtemos
forall y)(D x y B x y) por toE.

Passo 20

Instanciamos cada um dos universais com y:
B x y C y e D x y B x y (UI)

Passo 21

De A x wed>= D x y obtemos D x y por landE.
De D x y e D x y B x y obtemos B x y por toE.

Passo 22

De B x y e B x y C y obtemos C y por toE.

Passo 23

Das assunções A x wed>= D x y que levaram a C y introduzimos
A x wed>= D x y C y
por toI, dispensando a assunção.

Passo 24

Por forallI sobre y, concluímos
(forall y)(A x wed>= D x y C y)
Por forallI sobre x, concluímos
(forall x)(forall y)(A x wed>= D x y C y)

Resposta

(forall x)(forall y)(A x wed>= D x y C y)

Exercícios relacionados