Dedução Natural para a Lógica Clássica Proposicional
Material:
Aulas expositivas, reforço, sessões de dúvidas, desafios (tutores+fórum)
Videos sobre estratégias matemáticas de demonstração formuladas em Dedução Natural
Livro DGM, capítulo 1, páginas 1-5 e 15-46.
Verbetes wikipédicos:
- Dedução Natural (PT)
- Dedução Natural (EN)
Soluções dos exercícios das páginas 45-46 do capítulo 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
Temas importantes:
Sistema de dedução natural Np.
Meta-resultados importantes envolvendo a relação de consequência formal associada à dedução natural (monotonicidade, corte, compacidade, teorema da dedução, etc)
Exercícios DN-LCP:
0 ⊢ (A→A)
1 ⊢ (A→(B→A))
2 (A→B), (B→C) ⊢ (A→C)
3 (A→(B→C)), (A→B) ⊢ (A→C)
4 ((A→B)→(A→C)) ⊢ (A→(B→C))
5 (A→(A→B)) ⊢ (A→B)
6 (A→(B→C)) ⊢ (B→(A→C))
7 (A→(B→(C→D))) ⊢ (C→(B→(A→D)))
8 ((A→B)→C) ⊢ (A→(B→C))
9 ⊢ (A→ B) → A → (B → C) → C
10 ⊢ (A → B → C) → A → (A → B) → C
11 ⊢ ((A → B) → B → C) → (A → B) → A → C
12 ⊢ (A → B) → A → ((A → B) → C → B → D) → ((A → B) → C) → D
13 ⊢ (A → B → C → D) → A → ((A → B → C → D) → B) → ((A → B → C → D) → C) → D
14 A ⊢ (A∧A)
15 (A∧B) ⊢ (B∧A)
16 (A∧(B∧C)) ⊢ ((A∧B)∧C)
17 (A→C) ⊢ ((A∧B)→C)
18 (A→B) ⊢ ((C∧A)→(B∧C))
19 (A→(B→C)) ⊢ ((A∧B)→C)
20 ((A∧B)→C) ⊢ (A→(B→C))
21 ((A→B)→C) ⊢ ((A∧B)→C)
22 (A∧(B→C)) ⊢ ((A→B)→C)
23 ((A→B)∧(A→C)) ⊢ (A→(B∧C))
24 (A→(B∧C)) ⊢ ((A→B)∧(A→C))
25 (A∨A) ⊢ A
26 (A∨B) ⊢ (B∨A)
27 (A∨(B∨C)) ⊢ ((A∨B)∨C)
28 ((A∨B)∨C) ⊢ (A∨(B∨C))
29 (C∨(A∨B)) ⊢ ((B∨(A∨C))∨A)
30 ((B∨(A∨C))∨A) ⊢ (C∨(A∨B))
31 (A→B) ⊢ (A→(B∨C))
32 ((A∨B)→C) ⊢ (A→C)
33 (A∨B), (A→C), (B→D) ⊢ (C∨D)
34 (A→C), (B→C) ⊢ ((A∨B)→C)
35 (A→B) ⊢ ((C∨A)→(B∨C))
36 (A∧(B∨C)) ⊢ ((A∧B)∨(A∧C))
37 ((A∧B)∨(A∧C)) ⊢ (A∧(B∨C))
38 (A∨(B∧C)) ⊢ ((A∨B)∧(A∨C))
39 ((A∨B)∧(A∨C)) ⊢ (A∨(B∧C))
40 (A∧B) ⊢ (A∨B)
41 (A∧B) ⊢ (A→B)
42 A ⊢ (A∧(A∨B))
43 (A∨(A∧B)) ⊢ A
44 ⊢ (A∨⊤)
45 (A∧⊥) ⊢ B
46 ¬A ⊢ (A→⊥)
47 (A→⊥) ⊢ ¬A
48 A ⊢ ¬¬A
49 ¬¬¬A ⊢ ¬A
50 ¬¬A ⊢ A
51 A, ¬A ⊢ B
52 ¬(A∧¬A)
53 (A→B), (A→¬B) ⊢ ¬A
54 (¬¬A→B), (¬¬A→¬B) ⊢ ¬A
55 (¬A→B), (¬A→¬B) ⊢ A
56 ⊢ (A∨¬A)
57 (A→B), (¬A→B) ⊢ B
58 ⊢ ((A→¬A)→¬A)
59 ⊢ ((¬A→A)→A)
60 (A→B), ¬B ⊢ ¬A
61 (A→¬B), B ⊢ ¬A
62 (¬A→B), ¬B ⊢ A
63 (¬A→¬B), B ⊢ A
64 ¬(A∧B), A ⊢ ¬B
65 ¬(A∧B), B ⊢ ¬A
66 ¬(A∧¬B), A ⊢ B
67 ¬(¬A∧B), B ⊢ A
68 ¬(A∧B∧C), B ⊢ ¬(A∧C)
69 ¬(A∧E∧B), ¬(C∧¬E∧D) ⊢ ¬(A∧B∧C∧D)
70 (A∨B), ¬A ⊢ B
71 (¬A∨B), A ⊢ B
72 (A∨B), ¬B ⊢ A
73 (A∨¬B), B ⊢ A
74 A∨E∨B, C∨¬E∨D ⊢ A∨B∨C∨D
75 ¬A ⊢ ¬(A∧B)
76 ¬B ⊢ ¬(A∧B)
77 A ⊢ ¬(¬A∧B)
78 B ⊢ ¬(A∧¬B)
79 ¬(A∨B) ⊢ ¬A
80 ¬(A∨B) ⊢ ¬B
81 ¬(¬A∨B) ⊢ A
82 ¬(A∨¬B) ⊢ B
83 (A→B) ⊢ (¬A∨B)
84 (¬A→B) ⊢ (A∨B)
85 (A→B) ⊢ ¬(A∧¬B)
86 (A→¬B) ⊢ ¬(A∧B)
87 A, ¬B ⊢ ¬(A→B)
88 ¬(A→B) ⊢ A
89 ¬(A→B) ⊢ ¬B
90 ¬(A→¬B) ⊢ B
91 (¬A∧¬B) ⊢ ¬(A∨B)
92 ¬(A∨B) ⊢ (¬A∧¬B)
93 (A∨B) ⊢ ¬(¬A∧¬B)
94 ¬(¬A∧¬B) ⊢ (A∨B)
95 (A∧B) ⊢ ¬(¬A∨¬B)
96 ¬(¬A∨¬B) ⊢ (A∧B)
97 (¬A∨¬B) ⊢ ¬(A∧B)
98 ¬(A∧B) ⊢ (¬A∨¬B)
99 ¬(¬A∧B∧¬C), B ⊢ (A∨C)
100 ⊢ (A↔A)
101 (A↔B) ⊢ (B↔A)
102 (A↔B), (B↔C) ⊢ (A↔C)
103 A, B ⊢ (A↔B)
104 ¬A, ¬B ⊢ (A↔B)
105 A, ¬B ⊢ ¬(A↔B)
106 ¬A, B ⊢ ¬(A↔B)
107 (A↔B), ¬A ⊢ ¬B
108 (A↔B), ¬B ⊢ ¬A
109 (¬A↔B), A ⊢ ¬B
110 (A↔¬B), B ⊢ ¬A
111 ¬(A↔B), A ⊢ ¬B
112 ¬(A↔B), B ⊢ ¬A
113 ¬(A↔B), ¬A ⊢ B
114 ¬(A↔B), ¬B ⊢ A
115 (A↔B), (A↔¬B) ⊢ ⊥
116 ⊢ ¬(A↔B)↔¬(B↔A)
117 ⊢ ¬(A↔B)↔(¬A↔B)
118 ⊢ ¬(A↔B)↔(A↔¬B)
119 ⊢ (¬A↔B)↔(A↔¬B)
120 ⊢ (A↔(A∧⊤))
121 ⊢ (A↔(A∨⊥))
122 ⊢ ((A∧B)↔(B∧A))
123 ⊢ ((A∨B)↔(B∨A))
124 ⊢ ((A→B)↔(¬B→¬A))
125 ⊢ ((¬A→B)↔(¬B→A))
126 (A∧B) ⊢ ((A∨B)↔(A↔B))
127 (A∨B) ⊢ ((A∧B)↔(A↔B))
128 ⊢ ((A→B)↔(A↔(A∧B)))
129 ⊢ ((A→B)↔(B↔(A∨B)))
130 ⊢ ((A↔B)↔((A→B)∧(B→A)))
131 ⊢ ((A↔B)↔((A∨B)→(A∧B)))
132 ⊢ ((A∧B) ↔ (A↔(A→B)))
133 ⊢ ((A∧B) ↔ (B↔(B→A)))
134 ⊢ ((A∨B) ↔ (A↔(B→A)))
135 ⊢ ((A∨B) ↔ (B↔(A→B)))
136 ⊢ ((A∨B) ↔ ((A↔B)→A))
137 ⊢ ((A∨B) ↔ ((A↔B)→B))
138 ⊢ ((A↔B)↔((A∧B)∨(¬A∧¬B)))
139 ⊢ ((A↔B)↔((¬A∨B)∧(A∨¬B)))
140 (A↔B) ⊢ (¬A↔¬B)
141 (A↔B) ⊢ ((A∧C)↔(B∧C))
142 (A↔B) ⊢ ((A∨C)↔(B∨C))
143 (A↔B) ⊢ ((A→C)↔(B→C))
144 (A↔B) ⊢ ((C→A)↔(C→B))
145 ⊢ ¬(A↔¬A)
146 ⊢ (((A↔B)↔B)↔A)
147 (A↔(B↔C)) ⊢ ((C↔A)↔B)
148 (A↔(B↔C)) ⊢ (B↔(C↔A))
149 (A↔(B↔C)) ⊢ ((A↔B)↔C)