3 http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html
10 Compilare i seguenti campi:
29 Lo scopo della lezione è di farvi imparare ad usare Matita
30 per auto-correggervi gli esercizi di deduzione naturale, che
31 saranno parte dell'esame scritto. Il consiglio è di
32 fare prima gli esercizi su carta e poi digitarli in Matita
33 per verificarne la correttezza. Fare direttamente gli esercizi
34 con Matita è difficile e richiede molto più tempo.
39 Per digitare i connettivi logici:
44 * `⇒` : `=>`, `\Rightarrow`
48 I termini, le formule e i nomi delle ipotesi
49 ============================================
51 * Le formule, quando argomenti di
52 una regola, vengono scritte tra `(` e `)`.
54 * I nomi delle ipotesi, quando argomenti di
55 una regola, vengono scritti tra `[` e `]`.
57 Le regole di deduzione naturale
58 ===============================
60 Per digitare le regole di deduzione naturale
61 è possibile utilizzare la palette che compare
62 sulla sinistra dopo aver premuto `F2`.
64 L'albero si descrive partendo dalla radice. Le regole
65 con premesse multiple sono seguite da `[`, `|` e `]`.
68 apply rule (∧_i (A∨B) ⊥);
69 [ …continua qui il sottoalbero per (A∨B)
70 | …continua qui il sottoalbero per ⊥
73 Le regole vengono applicate alle loro premesse, ovvero
74 gli argomenti delle regole sono le formule che normalmente
75 scrivete sopra la linea che rappresenta l'applicazione della
76 regola stessa. Ad esempio:
78 aply rule (∨_e (A∨B) [h1] C [h2] C);
80 | …prova di C sotto l'ipotesi A (di nome h1)
81 | …prova di C sotto l'ipotesi B (di nome h2)
84 Le regole che hanno una sola premessa non vengono seguite
90 Per visualizzare l'albero man mano che viene costruito
91 dai comandi impartiti al sistema, premere `F3` e poi
92 premere sul bottome home (in genere contraddistinto da
93 una icona rappresentate una casa).
95 Si suggerisce di marcare tale finestra come `always on top`
96 utilizzando il menu a tendina che nella maggior parte degli
97 ambienti grafici si apre cliccando nel suo angolo in
100 Applicazioni di regole errate vengono contrassegnate con
105 include "didactic/support/natural_deduction.ma".
107 theorem EM: ∀A:CProp. A ∨ ¬ A.
108 (* Il comando assume è necessario perchè dimostriamo A∨¬A
109 per una A generica. *)
111 (* Questo comando inizia a disegnare l'albero *)
112 apply rule (prove (A ∨ ¬A));
113 (* qui inizia l'albero, eseguite passo passo osservando come
114 si modifica l'albero. *)
115 apply rule (RAA [H] (⊥)).
116 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
117 [ apply rule (discharge [H]).
118 | apply rule (⊥_e (⊥));
119 apply rule (¬_e (¬¬A) (¬A));
120 [ apply rule (¬_i [K] (⊥)).
121 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
122 [ (*BEGIN*)apply rule (discharge [H]).(*END*)
123 | (*BEGIN*)apply rule (∨_i_r (¬A)).
124 apply rule (discharge [K]).(*END*)
126 | (*BEGIN*)apply rule (¬_i [K] (⊥)).
127 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
128 [ apply rule (discharge [H]).
129 | apply rule (∨_i_l (A)).
130 apply rule (discharge [K]).
136 theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
137 apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
139 apply rule (⇒_i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
140 apply rule (⇒_i [h2] (G ∨ L ⇒ ¬L ⇒ E));
141 apply rule (⇒_i [h3] (¬L ⇒ E));
142 apply rule (⇒_i [h4] (E));
143 apply rule (∨_e (G∨L) [h5] (E) [h6] (E));
144 [ apply rule (discharge [h3]);
145 | apply rule (∨_e (E∨C) [h6] (E) [h7] (E));
146 [ apply rule (⇒_e (¬L ⇒ E∨C) (¬L));
147 [ apply rule (discharge [h2]);
148 | apply rule (discharge [h4]);
150 | apply rule (discharge [h6]);
151 | apply rule (⇒_e (C∧G ⇒ E) (C∧G));
152 [ apply rule (discharge [h1]);
153 | apply rule (∧_i (C) (G));
154 [ apply rule (discharge [h7]);
155 | apply rule (discharge [h5]);
159 | apply rule (⊥_e (⊥));
160 apply rule (¬_e (¬L) (L));
161 [ apply rule (discharge [h4]);
162 | apply rule (discharge [h6]);
168 theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
169 apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
171 apply rule (⇒_i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
172 apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
173 apply rule (⇒_i [h3] (D ⇒ C));
174 apply rule (⇒_i [h4] (C));
175 apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
176 [ apply rule (lem 0 EM);
177 | apply rule (⇒_e (B∧D⇒C) (B∧D));
178 [ apply rule (discharge [h2]);
179 | apply rule (∧_i (B) (D));
180 [ apply rule (discharge [h5]);
181 | apply rule (discharge [h4]);
184 | apply rule (⇒_e (A∧¬B⇒C) (A∧¬B));
185 [ apply rule (discharge [h1]);
186 | apply rule (∧_i (A) (¬B));
187 [ apply rule (⇒_e (D⇒A) (D));
188 [ apply rule (discharge [h3]);
189 | apply rule (discharge [h4]);
191 | apply rule (discharge [h6]);
198 (* Per dimostrare questo teorema torna comodo il lemma EM
199 dimostrato in precedenza. *)
200 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
201 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
203 apply rule (⇒_i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
204 apply rule (⇒_i [h2] ((L⇒F) ⇒ L ⇒ E));
205 apply rule (⇒_i [h3] (L ⇒ E));
206 apply rule (⇒_i [h4] (E));
207 apply rule (∨_e (G∨E) [h5] (E) [h6] (E));
208 [ apply rule (⇒_e (F ⇒ G∨E) (F));
209 [ apply rule (discharge [h1]);
210 | apply rule (⇒_e (L⇒F) (L));
211 [ apply rule (discharge [h3]);
212 | apply rule (discharge [h4]);
215 |apply rule (∨_e (¬L∨E) [h7] (E) [h8] (E));
216 [ apply rule (⇒_e (G⇒¬L∨E) (G));
217 [ apply rule (discharge [h2]);
218 | apply rule (discharge [h5]);
220 | apply rule (⊥_e (⊥));
221 apply rule (¬_e (¬L) (L));
222 [ apply rule (discharge [h7]);
223 | apply rule (discharge [h4]);
225 | apply rule (discharge [h8]);
227 | apply rule (discharge [h6]);
232 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
233 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
235 apply rule (⇒_i [h1] (¬A∨¬B));
236 apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
237 [ apply rule (lem 0 EM);
238 | apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
239 [ apply rule (lem 0 EM);
240 | apply rule (⊥_e (⊥));
241 apply rule (¬_e (¬(A∧B)) (A∧B));
242 [ apply rule (discharge [h1]);
243 | apply rule (∧_i (A) (B));
244 [ apply rule (discharge [h2]);
245 | apply rule (discharge [h4]);
248 | apply rule (∨_i_r (¬B));
249 apply rule (discharge [h5]);
251 | apply rule (∨_i_l (¬A));
252 apply rule (discharge [h3]);
257 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
258 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
260 apply rule (⇒_i [h1] (¬A ∧ ¬B));
261 apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
262 [ apply rule (lem 0 EM);
263 | apply rule (⊥_e (⊥));
264 apply rule (¬_e (¬(A∨B)) (A∨B));
265 [ apply rule (discharge [h1]);
266 | apply rule (∨_i_l (A));
267 apply rule (discharge [h2]);
269 | apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
270 [ apply rule (lem 0 EM);
271 | apply rule (⊥_e (⊥));
272 apply rule (¬_e (¬(A∨B)) (A∨B));
273 [ apply rule (discharge [h1]);
274 | apply rule (∨_i_r (B));
275 apply rule (discharge [h10]);
277 | apply rule (∧_i (¬A) (¬B));
278 [ apply rule (discharge [h3]);
279 |apply rule (discharge [h11]);
286 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
287 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
289 apply rule (⇒_i [h1] (¬(A∨B)));
290 apply rule (¬_i [h2] (⊥));
291 apply rule (∨_e (A∨B) [h3] (⊥) [h3] (⊥));
292 [ apply rule (discharge [h2]);
293 | apply rule (¬_e (¬A) (A));
294 [ apply rule (∧_e_l (¬A∧¬B));
295 apply rule (discharge [h1]);
296 | apply rule (discharge [h3]);
298 | apply rule (¬_e (¬B) (B));
299 [ apply rule (∧_e_r (¬A∧¬B));
300 apply rule (discharge [h1]);
301 | apply rule (discharge [h3]);
307 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
308 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
310 apply rule (⇒_i [h1] (A));
311 apply rule (RAA [h2] (⊥));
312 apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
313 [ apply rule (discharge [h1]);
314 | apply rule (⇒_i [h3] (⊥));
315 apply rule (¬_e (¬A) (A));
316 [ apply rule (discharge [h2]);
317 | apply rule (discharge [h3]);