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 DOCEND*)
 104
 105 include "didactic/support/natural_deduction.ma".
 106
 107 theorem EM: ∀A:CProp. A ∨ ¬ A.
 108 (* Il comando assume è necessario perchè dimostriamo A∨¬A
 109    per una A generica. *)
 110 assume A: CProp.
 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*)
 125               ]
 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]).
 131               ](*END*)
 132            ]
 133         ]
 134 qed.
 135
 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));
 138 (*BEGIN*)
 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]);
 149                 ]
 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]);
 156                 ]
 157                 ]
 158             ]
 159         | apply rule (⊥_e (⊥));
 160           apply rule (¬_e (¬L) (L));
 161             [ apply rule (discharge [h4]);
 162             | apply rule (discharge [h6]);
 163             ]
 164         ]
 165 (*END*)
 166 qed.
 167
 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));
 170 (*BEGIN*)
 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]);
 182                 ]
 183             ]
 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]);
 190                     ]
 191                 | apply rule (discharge [h6]);
 192                 ]
 193             ]
 194         ]
 195 (*END*)
 196 qed.
 197
 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));
 202 (*BEGIN*)
 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]);
 213                 ]
 214             ]
 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]);
 219                 ]
 220             | apply rule (⊥_e (⊥));
 221         apply rule (¬_e (¬L) (L));
 222                 [ apply rule (discharge [h7]);
 223                 | apply rule (discharge [h4]);
 224                 ]
 225             | apply rule (discharge [h8]);
 226             ]
 227         | apply rule (discharge [h6]);
 228         ]
 229 (*END*)
 230 qed.
 231
 232 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
 233 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 234 (*BEGIN*)
 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]);
 246                     ]
 247                 ]
 248             | apply rule (∨_i_r (¬B));
 249         apply rule (discharge [h5]);
 250             ]
 251         | apply rule (∨_i_l (¬A));
 252     apply rule (discharge [h3]);
 253         ]
 254 (*END*)
 255 qed.
 256
 257 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
 258 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 259 (*BEGIN*)
 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]);
 268             ]
 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]);
 276                 ]
 277             | apply rule (∧_i (¬A) (¬B));
 278                 [ apply rule (discharge [h3]);
 279                 |apply rule (discharge [h11]);
 280                 ]
 281             ]
 282         ]
 283 (*END*)
 284 qed.
 285
 286 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
 287 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
 288 (*BEGIN*)
 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]);
 297             ]
 298         | apply rule (¬_e (¬B) (B));
 299             [ apply rule (∧_e_r (¬A∧¬B));
 300         apply rule (discharge [h1]);
 301             | apply rule (discharge [h3]);
 302             ]
 303         ]
 304 (*END*)
 305 qed.
 306
 307 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
 308 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
 309 (*BEGIN*)
 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]);
 318             ]
 319         ]
 320 (*END*)
 321 qed.
 322