helm/software/matita/library/didactic/exercises/natural_deduction.ma

   1 (* Istruzioni:
   2
   3      http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html
   4
   5 *)
   6
   7 (* Esercizio 0
   8    ===========
   9
  10    Compilare i seguenti campi:
  11
  12    Nome1: ...
  13    Cognome1: ...
  14    Matricola1: ...
  15    Account1: ...
  16
  17    Nome2: ...
  18    Cognome2: ...
  19    Matricola2: ...
  20    Account2: ...
  21
  22 *)
  23
  24 (*DOCBEGIN
  25
  26 Scopo della lezione
  27 ===================
  28
  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.
  35
  36 I connettivi logici
  37 ===================
  38
  39 Per digitare i connettivi logici:
  40
  41 * `∧` : `\land`
  42 * `∨` : `\lor`
  43 * `¬` : `\lnot`
  44 * `⇒` : `=>`, `\Rightarrow`
  45 * `⊥` : `\bot`
  46 * `⊤` : `\top`
  47
  48 I termini, le formule e i nomi delle ipotesi
  49 ============================================
  50
  51 * Le formule, quando argomenti di
  52   una regola, vengono scritte tra `(` e `)`.
  53
  54 * I nomi delle ipotesi, quando argomenti di
  55   una regola, vengono scritti tra `[` e `]`.
  56
  57 Le regole di deduzione naturale
  58 ===============================
  59
  60 Per digitare le regole di deduzione naturale
  61 è possibile utilizzare la palette che compare
  62 sulla sinistra dopo aver premuto `F2`.
  63
  64 L'albero si descrive partendo dalla radice. Le regole
  65 con premesse multiple sono seguite da `[`, `|` e `]`.
  66 Ad esempio:
  67
  68         apply rule (∧_i (A∨B) ⊥);
  69           [ …continua qui il sottoalbero per (A∨B)
  70           | …continua qui il sottoalbero per ⊥
  71           ]
  72
  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:
  77
  78         aply rule (∨_e (A∨B) [h1] C [h2] C);
  79           [ …prova di (A∨B)
  80           | …prova di C sotto l'ipotesi A (di nome h1)
  81           | …prova di C sotto l'ipotesi B (di nome h2)
  82           ]
  83
  84 Le regole che hanno una sola premessa non vengono seguite
  85 da parentesi quadre.
  86
  87 L'albero di deduzione
  88 =====================
  89
  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).
  94
  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
  98 alto a sinistra.
  99
 100 Applicazioni di regole errate vengono contrassegnate con
 101 il colore rosso.
 102
 103 Usare i lemmi dimostrati in precedenza
 104 ======================================
 105
 106 Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
 107 riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
 108
 109 La "regola" `lem` prende come argomenti:
 110
 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`.
 113
 114 - Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
 115
 116 - Infine, le formule che devono essere scritte come premesse per la
 117   "regola".
 118
 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.
 123
 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.
 126
 127 Per motivi che saranno più chiari una volta studiate logiche del primo ordine
 128 o di ordine superiore, i lemmi che si intende riutilizzare è bene
 129 che siano dimostrati astratti sugli atomi, ovvero per ogni
 130 atomo `A`...`Z` che compare nella formula, è bene aggiungere
 131 una quantificazione all'inizio della formula stessa (es. `∀A:CProp.`)
 132 e iniziare la dimostrazione con il comando `assume`. In tale
 133 modo il lemma EM può essere utilizzato sia per dimostrare
 134 `A ∨ ¬A` sia `B ∨ ¬B` sia `(A∨C) ∨ ¬(A∨C)` ...
 135
 136 DOCEND*)
 137
 138 include "didactic/support/natural_deduction.ma".
 139
 140 theorem EM: ∀A:CProp. A ∨ ¬ A.
 141 (* Il comando assume è necessario perchè dimostriamo A∨¬A
 142    per una A generica. *)
 143 assume A: CProp.
 144 (* Questo comando inizia a disegnare l'albero *)
 145 apply rule (prove (A ∨ ¬A));
 146 (* qui inizia l'albero, eseguite passo passo osservando come
 147    si modifica l'albero. *)
 148 apply rule (RAA [H] (⊥)).
 149 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
 150         [ apply rule (discharge [H]).
 151         | apply rule (⊥_e (⊥));
 152           apply rule (¬_e (¬¬A) (¬A));
 153            [ apply rule (¬_i [K] (⊥)).
 154        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
 155               [ (*BEGIN*)apply rule (discharge [H]).(*END*)
 156               | (*BEGIN*)apply rule (∨_i_r (¬A)).
 157           apply rule (discharge [K]).(*END*)
 158               ]
 159            | (*BEGIN*)apply rule (¬_i [K] (⊥)).
 160        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
 161               [ apply rule (discharge [H]).
 162               | apply rule (∨_i_l (A)).
 163           apply rule (discharge [K]).
 164               ](*END*)
 165            ]
 166         ]
 167 qed.
 168
 169 theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
 170 apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
 171 (*BEGIN*)
 172 apply rule (⇒_i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
 173 apply rule (⇒_i [h2] (G ∨ L ⇒ ¬L ⇒ E));
 174 apply rule (⇒_i [h3] (¬L ⇒ E));
 175 apply rule (⇒_i [h4] (E));
 176 apply rule (∨_e (G∨L) [h5] (E) [h6] (E));
 177         [ apply rule (discharge [h3]);
 178         | apply rule (∨_e (E∨C) [h6] (E) [h7] (E));
 179             [ apply rule (⇒_e (¬L ⇒ E∨C) (¬L));
 180                 [ apply rule (discharge [h2]);
 181                 | apply rule (discharge [h4]);
 182                 ]
 183             | apply rule (discharge [h6]);
 184             | apply rule (⇒_e (C∧G ⇒ E) (C∧G));
 185                 [ apply rule (discharge [h1]);
 186                 | apply rule (∧_i (C) (G));
 187                     [ apply rule (discharge [h7]);
 188                     | apply rule (discharge [h5]);
 189                 ]
 190                 ]
 191             ]
 192         | apply rule (⊥_e (⊥));
 193           apply rule (¬_e (¬L) (L));
 194             [ apply rule (discharge [h4]);
 195             | apply rule (discharge [h6]);
 196             ]
 197         ]
 198 (*END*)
 199 qed.
 200
 201 theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
 202 apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
 203 (*BEGIN*)
 204 apply rule (⇒_i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
 205 apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
 206 apply rule (⇒_i [h3] (D ⇒ C));
 207 apply rule (⇒_i [h4] (C));
 208 apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
 209         [ apply rule (lem 0 EM);
 210         | apply rule (⇒_e (B∧D⇒C) (B∧D));
 211             [ apply rule (discharge [h2]);
 212         | apply rule (∧_i (B) (D));
 213                 [ apply rule (discharge [h5]);
 214                 | apply rule (discharge [h4]);
 215                 ]
 216             ]
 217         | apply rule (⇒_e (A∧¬B⇒C) (A∧¬B));
 218             [ apply rule (discharge [h1]);
 219             | apply rule (∧_i (A) (¬B));
 220                 [ apply rule (⇒_e (D⇒A) (D));
 221                     [ apply rule (discharge [h3]);
 222                     | apply rule (discharge [h4]);
 223                     ]
 224                 | apply rule (discharge [h6]);
 225                 ]
 226             ]
 227         ]
 228 (*END*)
 229 qed.
 230
 231 (* Per dimostrare questo teorema torna comodo il lemma EM
 232    dimostrato in precedenza. *)
 233 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
 234 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 235 (*BEGIN*)
 236 apply rule (⇒_i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 237 apply rule (⇒_i [h2] ((L⇒F) ⇒ L ⇒ E));
 238 apply rule (⇒_i [h3] (L ⇒ E));
 239 apply rule (⇒_i [h4] (E));
 240 apply rule (∨_e (G∨E) [h5] (E) [h6] (E));
 241         [ apply rule (⇒_e (F ⇒ G∨E) (F));
 242             [ apply rule (discharge [h1]);
 243             | apply rule (⇒_e (L⇒F) (L));
 244                 [ apply rule (discharge [h3]);
 245                 | apply rule (discharge [h4]);
 246                 ]
 247             ]
 248         |apply rule (∨_e (¬L∨E) [h7] (E) [h8] (E));
 249             [ apply rule (⇒_e (G⇒¬L∨E) (G));
 250                 [ apply rule (discharge [h2]);
 251                 | apply rule (discharge [h5]);
 252                 ]
 253             | apply rule (⊥_e (⊥));
 254         apply rule (¬_e (¬L) (L));
 255                 [ apply rule (discharge [h7]);
 256                 | apply rule (discharge [h4]);
 257                 ]
 258             | apply rule (discharge [h8]);
 259             ]
 260         | apply rule (discharge [h6]);
 261         ]
 262 (*END*)
 263 qed.
 264
 265 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
 266 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 267 (*BEGIN*)
 268 apply rule (⇒_i [h1] (¬A∨¬B));
 269 apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
 270         [ apply rule (lem 0 EM);
 271         | apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
 272             [ apply rule (lem 0 EM);
 273             | apply rule (⊥_e (⊥));
 274               apply rule (¬_e (¬(A∧B)) (A∧B));
 275                 [ apply rule (discharge [h1]);
 276                 | apply rule (∧_i (A) (B));
 277                     [ apply rule (discharge [h2]);
 278                     | apply rule (discharge [h4]);
 279                     ]
 280                 ]
 281             | apply rule (∨_i_r (¬B));
 282         apply rule (discharge [h5]);
 283             ]
 284         | apply rule (∨_i_l (¬A));
 285     apply rule (discharge [h3]);
 286         ]
 287 (*END*)
 288 qed.
 289
 290 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
 291 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 292 (*BEGIN*)
 293 apply rule (⇒_i [h1] (¬A ∧ ¬B));
 294 apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
 295         [ apply rule (lem 0 EM);
 296         | apply rule (⊥_e (⊥));
 297     apply rule (¬_e (¬(A∨B)) (A∨B));
 298             [ apply rule (discharge [h1]);
 299             | apply rule (∨_i_l (A));
 300         apply rule (discharge [h2]);
 301             ]
 302         | apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
 303             [ apply rule (lem 0 EM);
 304             | apply rule (⊥_e (⊥));
 305         apply rule (¬_e (¬(A∨B)) (A∨B));
 306                 [ apply rule (discharge [h1]);
 307                 | apply rule (∨_i_r (B));
 308             apply rule (discharge [h10]);
 309                 ]
 310             | apply rule (∧_i (¬A) (¬B));
 311                 [ apply rule (discharge [h3]);
 312                 |apply rule (discharge [h11]);
 313                 ]
 314             ]
 315         ]
 316 (*END*)
 317 qed.
 318
 319 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
 320 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
 321 (*BEGIN*)
 322 apply rule (⇒_i [h1] (¬(A∨B)));
 323 apply rule (¬_i [h2] (⊥));
 324 apply rule (∨_e (A∨B) [h3] (⊥) [h3] (⊥));
 325         [ apply rule (discharge [h2]);
 326         | apply rule (¬_e (¬A) (A));
 327             [ apply rule (∧_e_l (¬A∧¬B));
 328         apply rule (discharge [h1]);
 329             | apply rule (discharge [h3]);
 330             ]
 331         | apply rule (¬_e (¬B) (B));
 332             [ apply rule (∧_e_r (¬A∧¬B));
 333         apply rule (discharge [h1]);
 334             | apply rule (discharge [h3]);
 335             ]
 336         ]
 337 (*END*)
 338 qed.
 339
 340 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
 341 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
 342 (*BEGIN*)
 343 apply rule (⇒_i [h1] (A));
 344 apply rule (RAA [h2] (⊥));
 345 apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
 346         [ apply rule (discharge [h1]);
 347         | apply rule (⇒_i [h3] (⊥));
 348           apply rule (¬_e (¬A) (A));
 349             [ apply rule (discharge [h2]);
 350             | apply rule (discharge [h3]);
 351             ]
 352         ]
 353 (*END*)
 354 qed.
 355