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
 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`.
 134
 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 ...
 137
 138 DOCEND*)
 139
 140 include "didactic/support/natural_deduction.ma".
 141
 142 theorem EM: ∀A:CProp. A ∨ ¬ A.
 143 (* Il comando assume è necessario perchè dimostriamo A∨¬A
 144    per una A generica. *)
 145 assume A: CProp.
 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*)
 160               ]
 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]).
 166               ](*END*)
 167            ]
 168         ]
 169 qed.
 170
 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));
 173 (*BEGIN*)
 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]);
 184                 ]
 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]);
 191                 ]
 192                 ]
 193             ]
 194         | apply rule (⊥_e (⊥));
 195           apply rule (¬_e (¬L) (L));
 196             [ apply rule (discharge [h4]);
 197             | apply rule (discharge [h6]);
 198             ]
 199         ]
 200 (*END*)
 201 qed.
 202
 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));
 205 (*BEGIN*)
 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]);
 217                 ]
 218             ]
 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]);
 225                     ]
 226                 | apply rule (discharge [h6]);
 227                 ]
 228             ]
 229         ]
 230 (*END*)
 231 qed.
 232
 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));
 237 (*BEGIN*)
 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]);
 248                 ]
 249             ]
 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]);
 254                 ]
 255             | apply rule (⊥_e (⊥));
 256         apply rule (¬_e (¬L) (L));
 257                 [ apply rule (discharge [h7]);
 258                 | apply rule (discharge [h4]);
 259                 ]
 260             | apply rule (discharge [h8]);
 261             ]
 262         | apply rule (discharge [h6]);
 263         ]
 264 (*END*)
 265 qed.
 266
 267 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
 268 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 269 (*BEGIN*)
 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]);
 281                     ]
 282                 ]
 283             | apply rule (∨_i_r (¬B));
 284         apply rule (discharge [h5]);
 285             ]
 286         | apply rule (∨_i_l (¬A));
 287     apply rule (discharge [h3]);
 288         ]
 289 (*END*)
 290 qed.
 291
 292 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
 293 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 294 (*BEGIN*)
 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]);
 303             ]
 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]);
 311                 ]
 312             | apply rule (∧_i (¬A) (¬B));
 313                 [ apply rule (discharge [h3]);
 314                 |apply rule (discharge [h11]);
 315                 ]
 316             ]
 317         ]
 318 (*END*)
 319 qed.
 320
 321 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
 322 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
 323 (*BEGIN*)
 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]);
 332             ]
 333         | apply rule (¬_e (¬B) (B));
 334             [ apply rule (∧_e_r (¬A∧¬B));
 335         apply rule (discharge [h1]);
 336             | apply rule (discharge [h3]);
 337             ]
 338         ]
 339 (*END*)
 340 qed.
 341
 342 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
 343 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
 344 (*BEGIN*)
 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]);
 353             ]
 354         ]
 355 (*END*)
 356 qed.
 357