Dedução Natural para a Lógica Clássica de Primeira Ordem
Material:
Tema: sistema de dedução natural Nc, 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:
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