Dedução Natural para a Lógica Clássica de Primeira Ordem

Material:

• Tema: sistema de dedução natural N_c, com e sem igualdade.

• Aulas expositivas, reforço e sessões de dúvidas (tutores+fórum)

• Livro DGM, de Dionísio-Gouveia-Marcos, capítulo 3.1, páginas 27-43

• Exercícios resolvidos sobre dedução natural do capítulo 3.1 do livro DGM

• Avaliações + soluções:

  • - Avaliação 00 (DN): enunciado - gabarito

• Exercícios da nossa disciplina no sistema ProofWeb de apoio ao ensino (tutorial).

• Desafios de dedução natural a serem resolvidos no ProofWeb

Exercícios DN-LCPO:

0 (∀x.R(x))∧P ⊢ ∀x.(R(x)∧P)

1 ∃x.(R(x)∧P) ⊢ ∃x.R(x)

2 ∃x.(R(x)∧P) ⊢ P

3 ∀x.(R(x)→P) ⊢ (∀x.R(x))→P

4 (∃x.R(x))→P ⊢ ∃x.(R(x)→P)

5 P→∀x.R(x) ⊢ ∃x.(P→R(x))

6 ∀x.(P→R(x)) ⊢ P→∀x.R(x)

7 P→∀x.R(x) ⊢ ∀x.(P→R(x))

8 ∃x.(P→R(x)) ⊢ P→∃x.R(x)

9 ∀x.(R(x)→P) ⊢ (∃x.R(x))→P

10 ∃x.(R(x)→P) ⊢ (∀x.R(x))→P

11 (∀x.R(x))∨P ⊢ ∀x.(R(x)∨P)

12 ∃x.(R(x)∨P) ⊢ (∃x.R(x))∨P

13 ∀x.(P(x)↔Q) ⊢ (∀x.P(x))↔Q

14 R(j), ∀x.(R(x)→S(x)) ⊢ S(j)

15 ∀x.(R(x)→S(x)) ⊢ ∀y.R(y)→∀z.S(z)

16 ∀x.(R(x)→S(x)), ∀y.(S(y)→T(y)) ⊢ ∀z.(R(z)→T(z))

17 ∀x.(P(x)∧Q(x)) ⊢ ∀y.(Q(y)∧P(y))

18 ∃x.(P(x)∧Q(x)) ⊢ ∃y.(Q(y)∧P(y))

19 ∀x.R(x)∧∀y.S(y) ⊢ ∀z.(R(z)∧S(z))

20 ∀x.(R(x)∧S(x)) ⊢ ∀y.R(y)∧∀z.S(z)

21 ∀x.R(x)∨∀y.S(y) ⊢ ∀z.(R(z)∨S(z))

22 ∀x.R(x) ⊢ ∀y.(P∨R(y)∨Q)

23 ∀x.(R(x)→S(x)) ⊢ ∃y.R(y)→∃z.S(z)

24 ∃x.(R(x)∧S(x)) ⊢ ∃y.R(y)∧∃z.S(z)

25 ∃x.R(x) ⊢ ∃y.(P∨R(y)∨Q)

26 ∃x.(R(x)∨S(x)) ⊢ ∃y.R(y)∨∃z.S(z)

27 ∃x.R(x)∨∃y.S(y) ⊢ ∃z.(R(z)∨S(z))

28 ∀x.(R(x)↔S(x)) ⊢ ∃y.R(y)↔∃z.S(z)

29 ∀x.P(x) ⊢ ∃y.P(y)

30 ∀x.P(x) ⊢ ¬∀x.¬P(x)

31 P(i) ⊢ ¬∀x.¬P(x)

32 ⊢ ∃x.∃y.(R(x,y)→R(y,x))

33 ∀x.P(x) ⊢ ∀y.P(y)

34 ∃x.P(x) ⊢ ∃y.P(y)

35 ∀x.∀x.P(x) ⊢ ∀x.P(x)

36 ∃x.∃x.P(x) ⊢ ∃x.P(x)

37 ∀x.P(x) ⊢ ∀x.∀y.(P(x)∨P(y))

38 ∀x.P(x) ⊢ ∀x.∀y.(P(x)∧P(y))

39 ∃x.P(x) ⊢ ∃x.∃y.(P(x)∨P(y))

40 ∃x.P(x) ⊢ ∃x.∃y.(P(x)∧P(y))

41 ∀x.∀y.(P(x)∧P(y)) ⊢ ∀x.P(x)

42 ∀x.∀y.(P(x)∨P(y)) ⊢ ∀x.P(x)

43 ∃x.∃y.(P(x)∧P(y)) ⊢ ∃x.P(x)

44 ∃x.∃y.(P(x)∨P(y)) ⊢ ∃x.P(x)

45 ∃x.(∃y.P(y)→P(x)) ⊢ ∃x.∀y.(P(y)→P(x))

46 ∃x.∀y.(P(y)→P(x)) ⊢ ∃x.(∃y.P(y)→P(x))

47 ∀x.(∃y.P(y)→P(x)) ⊢ ∀x.∀y.(P(y)→P(x))

48 ∀x.∀y.(P(y)→P(x)) ⊢ ∀x.(∃y.P(y)→P(x))

49 ∀x.∀y.R(x,y) ⊢ ∀z.R(z,z)

50 ∃z.R(z,z) ⊢ ∃x.∃y.R(x,y)

51 ∀x.∀y.R(x,y) ⊢ ∀y.∀x.R(x,y)

52 ∃x.∃y.R(x,y) ⊢ ∃y.∃x.R(x,y)

53 ∃x.∀y.R(x,y) ⊢ ∀y.∃x.R(x,y)

54 ∀x.R(x) ⊢ ¬∃x.¬R(x)

55 ∃x.R(x) ⊢ ¬∀x.¬R(x)

56 ∃x.¬R(x) ⊢ ¬∀x.R(x)

57 ∀x.¬R(x) ⊢ ¬∃x.R(x)

58 ¬∃x.R(x) ⊢ ∀x.¬R(x)

59 ¬∃x.¬R(x) ⊢ ∀x.R(x)

60 ¬∀x.¬R(x) ⊢ ∃x.R(x)

61 ¬∀x.R(x) ⊢ ∃x.¬R(x)

62 ∀x.(R(x)→Q(x)), ∀x.(P(x)→R(x)) ⊢ ∀x.(P(x)→Q(x))

63 ∀x.(R(x)→¬Q(x)), ∀x.(P(x)→R(x)) ⊢ ∀x.(P(x)→¬Q(x))

64 ∀x.(R(x)→Q(x)), ∃x.(P(x)∧R(x)) ⊢ ∃x.(P(x)∧Q(x))

65 ∀x.(R(x)→¬Q(x)), ∃x.(P(x)∧R(x)) ⊢ ∃x.(P(x)∧¬Q(x))

66 ∀x.(Q(x)→¬R(x)), ∀x.(P(x)→R(x)) ⊢ ∀x.(P(x)→¬Q(x))

67 ∀x.(Q(x)→R(x)), ∀x.(P(x)→¬R(x)) ⊢ ∀x.(P(x)→¬Q(x))

68 ∀x.(Q(x)→¬R(x)), ∃x.(P(x)∧R(x)) ⊢ ∃x.(P(x)∧¬Q(x))

69 ∀x.(Q(x)→R(x)), ∃x.(P(x)∧¬R(x)) ⊢ ∃x.(P(x)∧¬Q(x))

70 ∀x.(R(x)→Q(x)), ∀x.(R(x)→P(x)), ∃x.R(x) ⊢ ∃x.(P(x)∧Q(x))

71 ∃x.(R(x)∧Q(x)), ∀x.(R(x)→P(x)) ⊢ ∃x.(P(x)∧Q(x))

72 ∀x.(R(x)→Q(x)), ∃x.(R(x)∧P(x)) ⊢ ∃x.(P(x)∧Q(x))

73 ∀x.(R(x)→¬Q(x)), ∀x.(R(x)→P(x)), ∃x.R(x) ⊢ ∃x.(P(x)∧¬Q(x))

74 ∃x.(R(x)∧¬Q(x)), ∀x.(R(x)→P(x)) ⊢ ∃x.(P(x)∧¬Q(x))

75 ∀x.(R(x)→¬Q(x)), ∃x.(R(x)∧P(x)) ⊢ ∃x.(P(x)∧¬Q(x))

76 ∀x.(Q(x)→R(x)), ∀x.(R(x)→P(x)), ∃x.Q(x) ⊢ ∃x.(P(x)∧Q(x))

77 ∀x.(Q(x)→R(x)), ∀x.(R(x)→¬P(x)) ⊢ ∀x.(P(x)→¬Q(x))

78 ∃x.(Q(x)∧R(x)), ∀x.(R(x)→P(x)) ⊢ ∃x.(P(x)∧Q(x))

79 ∀x.(Q(x)→¬R(x)), ∀x.(R(x)→P(x)), ∃x.R(x) ⊢ ∃x.(P(x)∧¬Q(x))

80 ∀x.(Q(x)→¬R(x)), ∃x.(R(x)∧P(x)) ⊢ ∃x.(P(x)∧¬Q(x))

81 ∃x.∃y.(P(x)∧Q(x,y)) ⊢ ∃x.(P(x)∧∃y.Q(x,y))

82 ∃x.(P(x)∧∃y.Q(x,y)) ⊢ ∃x.∃y.(P(x)∧Q(x,y))

83 ∃y.∀x.(P(x)→Q(x,y)) ⊢ ∀x.(P(x)→∃y.Q(x,y))

84 ∃x.(P(x)∨Q(x)), ∀x.(P(x)→Q(x)) ⊢ ∃x.Q(x)

85 ∀x.∀y.(R(x,y)→R(y,x)), ∀x.∀y.∀z.(R(x,y)→(R(y,z)→R(x,z)))

⊢ ∀x.∀y.∀z.(R(x,z)→(R(y,z)→R(x,y)))

86 ∀x.∀y.(R(x,y)→R(y,x)), ∀x.∀y.∀z.(R(x,y)→(R(y,z)→R(x,z)))

⊢ ∀x.∀y.∀z.(R(z,x)→(R(z,y)→R(x,y)))

87 ∀x.∀y.(R(x,y)→R(y,x)), ∀x.∀y.∀z.(R(x,y)→(R(y,z)→R(x,z)))

⊢ (∀x.∃y.R(x,y))↔(∀x.R(x,x))

88 x=z, y=z ⊢ x=y

89 z=x, z=y ⊢ x=y