1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
17 http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html
24 Compilare i seguenti campi:
43 Lo scopo della lezione è di farvi imparare ad usare Matita
44 per auto-correggervi gli esercizi di deduzione naturale, che
45 saranno parte dell'esame scritto. Il consiglio è di
46 fare prima gli esercizi su carta e poi digitarli in Matita
47 per verificarne la correttezza. Fare direttamente gli esercizi
48 con Matita è difficile e richiede molto più tempo.
53 Per digitare i connettivi logici:
58 * `⇒` : `=>`, `\Rightarrow`
62 I termini, le formule e i nomi delle ipotesi
63 ============================================
65 * Le formule, quando argomenti di
66 una regola, vengono scritte tra `(` e `)`.
68 * I nomi delle ipotesi, quando argomenti di
69 una regola, vengono scritti tra `[` e `]`.
71 Le regole di deduzione naturale
72 ===============================
74 Per digitare le regole di deduzione naturale
75 è possibile utilizzare la palette che compare
76 sulla sinistra dopo aver premuto `F2`.
78 L'albero si descrive partendo dalla radice. Le regole
79 con premesse multiple sono seguite da `[`, `|` e `]`.
82 apply rule (∧_i (A∨B) ⊥);
83 [ …continua qui il sottoalbero per (A∨B)
84 | …continua qui il sottoalbero per ⊥
87 Le regole vengono applicate alle loro premesse, ovvero
88 gli argomenti delle regole sono le formule che normalmente
89 scrivete sopra la linea che rappresenta l'applicazione della
90 regola stessa. Ad esempio:
92 aply rule (∨_e (A∨B) [h1] C [h2] C);
94 | …prova di C sotto l'ipotesi A (di nome h1)
95 | …prova di C sotto l'ipotesi B (di nome h2)
98 Le regole che hanno una sola premessa non vengono seguite
101 L'albero di deduzione
102 =====================
104 Per visualizzare l'albero man mano che viene costruito
105 dai comandi impartiti al sistema, premere `F3` e poi
106 premere sul bottome home (in genere contraddistinto da
107 una icona rappresentate una casa).
109 Si suggerisce di marcare tale finestra come `always on top`
110 utilizzando il menu a tendina che nella maggior parte degli
111 ambienti grafici si apre cliccando nel suo angolo in
114 Applicazioni di regole errate vengono contrassegnate con
117 Usare i lemmi dimostrati in precedenza
118 ======================================
120 Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
121 riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
123 La "regola" `lem` prende come argomenti:
125 - Il numero delle ipotesi del lemma che si vuole utilizzare, nel
126 caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
128 - Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
130 - Infine, le formule che devono essere scritte come premesse per la
133 Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
134 `lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
135 `lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario
136 far seguire le parentesi quadre come spiegato in precedenza.
138 Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
139 per rappresentare l'albero di prova del lemma che si sta riutilizzando.
141 Per motivi che saranno più chiari una volta studiate logiche del
142 primo ordine o di ordine superiore, i lemmi che si intende
143 riutilizzare è bene che siano dimostrati astratti sugli atomi.
144 Ovvero per ogni atomo `A`...`Z` che compare nella formula,
145 è bene aggiungere una quantificazione all'inizio della formula stessa.
146 Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
147 La dimostrazione deve poi iniziare con il comando `assume`.
149 In tale modo il lemma EM può essere utilizzato sia per dimostrare
150 `A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
154 include "didactic/support/natural_deduction.ma".
156 theorem EM: ∀A:CProp. A ∨ ¬ A.
157 (* Il comando assume è necessario perchè dimostriamo A∨¬A
158 per una A generica. *)
160 (* Questo comando inizia a disegnare l'albero *)
161 apply rule (prove (A ∨ ¬A));
162 (* qui inizia l'albero, eseguite passo passo osservando come
163 si modifica l'albero. *)
164 apply rule (RAA [H] (⊥)).
165 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
166 [ apply rule (discharge [H]).
167 | apply rule (⊥_e (⊥));
168 apply rule (¬_e (¬¬A) (¬A));
169 [ apply rule (¬_i [K] (⊥)).
170 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
171 [ (*BEGIN*)apply rule (discharge [H]).(*END*)
172 | (*BEGIN*)apply rule (∨_i_r (¬A)).
173 apply rule (discharge [K]).(*END*)
175 | (*BEGIN*)apply rule (¬_i [K] (⊥)).
176 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
177 [ apply rule (discharge [H]).
178 | apply rule (∨_i_l (A)).
179 apply rule (discharge [K]).
185 theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
186 apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
188 apply rule (⇒_i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
189 apply rule (⇒_i [h2] (G ∨ L ⇒ ¬L ⇒ E));
190 apply rule (⇒_i [h3] (¬L ⇒ E));
191 apply rule (⇒_i [h4] (E));
192 apply rule (∨_e (G∨L) [h5] (E) [h6] (E));
193 [ apply rule (discharge [h3]);
194 | apply rule (∨_e (E∨C) [h6] (E) [h7] (E));
195 [ apply rule (⇒_e (¬L ⇒ E∨C) (¬L));
196 [ apply rule (discharge [h2]);
197 | apply rule (discharge [h4]);
199 | apply rule (discharge [h6]);
200 | apply rule (⇒_e (C∧G ⇒ E) (C∧G));
201 [ apply rule (discharge [h1]);
202 | apply rule (∧_i (C) (G));
203 [ apply rule (discharge [h7]);
204 | apply rule (discharge [h5]);
208 | apply rule (⊥_e (⊥));
209 apply rule (¬_e (¬L) (L));
210 [ apply rule (discharge [h4]);
211 | apply rule (discharge [h6]);
217 theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
218 apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
220 apply rule (⇒_i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
221 apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
222 apply rule (⇒_i [h3] (D ⇒ C));
223 apply rule (⇒_i [h4] (C));
224 apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
225 [ apply rule (lem 0 EM);
226 | apply rule (⇒_e (B∧D⇒C) (B∧D));
227 [ apply rule (discharge [h2]);
228 | apply rule (∧_i (B) (D));
229 [ apply rule (discharge [h5]);
230 | apply rule (discharge [h4]);
233 | apply rule (⇒_e (A∧¬B⇒C) (A∧¬B));
234 [ apply rule (discharge [h1]);
235 | apply rule (∧_i (A) (¬B));
236 [ apply rule (⇒_e (D⇒A) (D));
237 [ apply rule (discharge [h3]);
238 | apply rule (discharge [h4]);
240 | apply rule (discharge [h6]);
247 (* Per dimostrare questo teorema torna comodo il lemma EM
248 dimostrato in precedenza. *)
249 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
250 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
252 apply rule (⇒_i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
253 apply rule (⇒_i [h2] ((L⇒F) ⇒ L ⇒ E));
254 apply rule (⇒_i [h3] (L ⇒ E));
255 apply rule (⇒_i [h4] (E));
256 apply rule (∨_e (G∨E) [h5] (E) [h6] (E));
257 [ apply rule (⇒_e (F ⇒ G∨E) (F));
258 [ apply rule (discharge [h1]);
259 | apply rule (⇒_e (L⇒F) (L));
260 [ apply rule (discharge [h3]);
261 | apply rule (discharge [h4]);
264 |apply rule (∨_e (¬L∨E) [h7] (E) [h8] (E));
265 [ apply rule (⇒_e (G⇒¬L∨E) (G));
266 [ apply rule (discharge [h2]);
267 | apply rule (discharge [h5]);
269 | apply rule (⊥_e (⊥));
270 apply rule (¬_e (¬L) (L));
271 [ apply rule (discharge [h7]);
272 | apply rule (discharge [h4]);
274 | apply rule (discharge [h8]);
276 | apply rule (discharge [h6]);
281 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
282 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
284 apply rule (⇒_i [h1] (¬A∨¬B));
285 apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
286 [ apply rule (lem 0 EM);
287 | apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
288 [ apply rule (lem 0 EM);
289 | apply rule (⊥_e (⊥));
290 apply rule (¬_e (¬(A∧B)) (A∧B));
291 [ apply rule (discharge [h1]);
292 | apply rule (∧_i (A) (B));
293 [ apply rule (discharge [h2]);
294 | apply rule (discharge [h4]);
297 | apply rule (∨_i_r (¬B));
298 apply rule (discharge [h5]);
300 | apply rule (∨_i_l (¬A));
301 apply rule (discharge [h3]);
306 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
307 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
309 apply rule (⇒_i [h1] (¬A ∧ ¬B));
310 apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
311 [ apply rule (lem 0 EM);
312 | apply rule (⊥_e (⊥));
313 apply rule (¬_e (¬(A∨B)) (A∨B));
314 [ apply rule (discharge [h1]);
315 | apply rule (∨_i_l (A));
316 apply rule (discharge [h2]);
318 | apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
319 [ apply rule (lem 0 EM);
320 | apply rule (⊥_e (⊥));
321 apply rule (¬_e (¬(A∨B)) (A∨B));
322 [ apply rule (discharge [h1]);
323 | apply rule (∨_i_r (B));
324 apply rule (discharge [h10]);
326 | apply rule (∧_i (¬A) (¬B));
327 [ apply rule (discharge [h3]);
328 |apply rule (discharge [h11]);
335 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
336 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
338 apply rule (⇒_i [h1] (¬(A∨B)));
339 apply rule (¬_i [h2] (⊥));
340 apply rule (∨_e (A∨B) [h3] (⊥) [h3] (⊥));
341 [ apply rule (discharge [h2]);
342 | apply rule (¬_e (¬A) (A));
343 [ apply rule (∧_e_l (¬A∧¬B));
344 apply rule (discharge [h1]);
345 | apply rule (discharge [h3]);
347 | apply rule (¬_e (¬B) (B));
348 [ apply rule (∧_e_r (¬A∧¬B));
349 apply rule (discharge [h1]);
350 | apply rule (discharge [h3]);
356 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
357 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
359 apply rule (⇒_i [h1] (A));
360 apply rule (RAA [h2] (⊥));
361 apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
362 [ apply rule (discharge [h1]);
363 | apply rule (⇒_i [h3] (⊥));
364 apply rule (¬_e (¬A) (A));
365 [ apply rule (discharge [h2]);
366 | apply rule (discharge [h3]);