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
103 Usare i lemmi dimostrati in precedenza
104 ======================================
106 Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
107 riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
109 La "regola" `lem` prende come argomenti:
111 - Il numero delle ipotesi del lemma che si vuole utilizzare, nel
112 caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
114 - Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
116 - Infine, le formule che devono essere scritte come premesse per la
119 Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
120 `lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
121 `lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario
122 far seguire le parentesi quadre come spiegato in precedenza.
124 Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
125 per rappresentare l'albero di prova del lemma che si sta riutilizzando.
127 Per motivi che saranno più chiari una volta studiate logiche del
128 primo ordine o di ordine superiore, i lemmi che si intende
129 riutilizzare è bene che siano dimostrati astratti sugli atomi.
130 Ovvero per ogni atomo `A`...`Z` che compare nella formula,
131 è bene aggiungere una quantificazione all'inizio della formula stessa.
132 Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
133 La dimostrazione deve poi iniziare con il comando `assume`.
135 In tale modo il lemma EM può essere utilizzato sia per dimostrare
136 `A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
140 include "didactic/support/natural_deduction.ma".
142 theorem EM: ∀A:CProp. A ∨ ¬ A.
143 (* Il comando assume è necessario perchè dimostriamo A∨¬A
144 per una A generica. *)
146 (* Questo comando inizia a disegnare l'albero *)
147 apply rule (prove (A ∨ ¬A));
148 (* qui inizia l'albero, eseguite passo passo osservando come
149 si modifica l'albero. *)
150 apply rule (RAA [H] (⊥)).
151 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
152 [ apply rule (discharge [H]).
153 | apply rule (⊥_e (⊥));
154 apply rule (¬_e (¬¬A) (¬A));
155 [ apply rule (¬_i [K] (⊥)).
156 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
157 [ (*BEGIN*)apply rule (discharge [H]).(*END*)
158 | (*BEGIN*)apply rule (∨_i_r (¬A)).
159 apply rule (discharge [K]).(*END*)
161 | (*BEGIN*)apply rule (¬_i [K] (⊥)).
162 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
163 [ apply rule (discharge [H]).
164 | apply rule (∨_i_l (A)).
165 apply rule (discharge [K]).
171 theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
172 apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
174 apply rule (⇒_i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
175 apply rule (⇒_i [h2] (G ∨ L ⇒ ¬L ⇒ E));
176 apply rule (⇒_i [h3] (¬L ⇒ E));
177 apply rule (⇒_i [h4] (E));
178 apply rule (∨_e (G∨L) [h5] (E) [h6] (E));
179 [ apply rule (discharge [h3]);
180 | apply rule (∨_e (E∨C) [h6] (E) [h7] (E));
181 [ apply rule (⇒_e (¬L ⇒ E∨C) (¬L));
182 [ apply rule (discharge [h2]);
183 | apply rule (discharge [h4]);
185 | apply rule (discharge [h6]);
186 | apply rule (⇒_e (C∧G ⇒ E) (C∧G));
187 [ apply rule (discharge [h1]);
188 | apply rule (∧_i (C) (G));
189 [ apply rule (discharge [h7]);
190 | apply rule (discharge [h5]);
194 | apply rule (⊥_e (⊥));
195 apply rule (¬_e (¬L) (L));
196 [ apply rule (discharge [h4]);
197 | apply rule (discharge [h6]);
203 theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
204 apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
206 apply rule (⇒_i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
207 apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
208 apply rule (⇒_i [h3] (D ⇒ C));
209 apply rule (⇒_i [h4] (C));
210 apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
211 [ apply rule (lem 0 EM);
212 | apply rule (⇒_e (B∧D⇒C) (B∧D));
213 [ apply rule (discharge [h2]);
214 | apply rule (∧_i (B) (D));
215 [ apply rule (discharge [h5]);
216 | apply rule (discharge [h4]);
219 | apply rule (⇒_e (A∧¬B⇒C) (A∧¬B));
220 [ apply rule (discharge [h1]);
221 | apply rule (∧_i (A) (¬B));
222 [ apply rule (⇒_e (D⇒A) (D));
223 [ apply rule (discharge [h3]);
224 | apply rule (discharge [h4]);
226 | apply rule (discharge [h6]);
233 (* Per dimostrare questo teorema torna comodo il lemma EM
234 dimostrato in precedenza. *)
235 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
236 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
238 apply rule (⇒_i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
239 apply rule (⇒_i [h2] ((L⇒F) ⇒ L ⇒ E));
240 apply rule (⇒_i [h3] (L ⇒ E));
241 apply rule (⇒_i [h4] (E));
242 apply rule (∨_e (G∨E) [h5] (E) [h6] (E));
243 [ apply rule (⇒_e (F ⇒ G∨E) (F));
244 [ apply rule (discharge [h1]);
245 | apply rule (⇒_e (L⇒F) (L));
246 [ apply rule (discharge [h3]);
247 | apply rule (discharge [h4]);
250 |apply rule (∨_e (¬L∨E) [h7] (E) [h8] (E));
251 [ apply rule (⇒_e (G⇒¬L∨E) (G));
252 [ apply rule (discharge [h2]);
253 | apply rule (discharge [h5]);
255 | apply rule (⊥_e (⊥));
256 apply rule (¬_e (¬L) (L));
257 [ apply rule (discharge [h7]);
258 | apply rule (discharge [h4]);
260 | apply rule (discharge [h8]);
262 | apply rule (discharge [h6]);
267 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
268 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
270 apply rule (⇒_i [h1] (¬A∨¬B));
271 apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
272 [ apply rule (lem 0 EM);
273 | apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
274 [ apply rule (lem 0 EM);
275 | apply rule (⊥_e (⊥));
276 apply rule (¬_e (¬(A∧B)) (A∧B));
277 [ apply rule (discharge [h1]);
278 | apply rule (∧_i (A) (B));
279 [ apply rule (discharge [h2]);
280 | apply rule (discharge [h4]);
283 | apply rule (∨_i_r (¬B));
284 apply rule (discharge [h5]);
286 | apply rule (∨_i_l (¬A));
287 apply rule (discharge [h3]);
292 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
293 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
295 apply rule (⇒_i [h1] (¬A ∧ ¬B));
296 apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
297 [ apply rule (lem 0 EM);
298 | apply rule (⊥_e (⊥));
299 apply rule (¬_e (¬(A∨B)) (A∨B));
300 [ apply rule (discharge [h1]);
301 | apply rule (∨_i_l (A));
302 apply rule (discharge [h2]);
304 | apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
305 [ apply rule (lem 0 EM);
306 | apply rule (⊥_e (⊥));
307 apply rule (¬_e (¬(A∨B)) (A∨B));
308 [ apply rule (discharge [h1]);
309 | apply rule (∨_i_r (B));
310 apply rule (discharge [h10]);
312 | apply rule (∧_i (¬A) (¬B));
313 [ apply rule (discharge [h3]);
314 |apply rule (discharge [h11]);
321 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
322 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
324 apply rule (⇒_i [h1] (¬(A∨B)));
325 apply rule (¬_i [h2] (⊥));
326 apply rule (∨_e (A∨B) [h3] (⊥) [h3] (⊥));
327 [ apply rule (discharge [h2]);
328 | apply rule (¬_e (¬A) (A));
329 [ apply rule (∧_e_l (¬A∧¬B));
330 apply rule (discharge [h1]);
331 | apply rule (discharge [h3]);
333 | apply rule (¬_e (¬B) (B));
334 [ apply rule (∧_e_r (¬A∧¬B));
335 apply rule (discharge [h1]);
336 | apply rule (discharge [h3]);
342 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
343 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
345 apply rule (⇒_i [h1] (A));
346 apply rule (RAA [h2] (⊥));
347 apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
348 [ apply rule (discharge [h1]);
349 | apply rule (⇒_i [h3] (⊥));
350 apply rule (¬_e (¬A) (A));
351 [ apply rule (discharge [h2]);
352 | apply rule (discharge [h3]);