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

   1 (* Esercizio 0
   2    ===========
   3
   4    Compilare i seguenti campi:
   5
   6    Nome1: ...
   7    Cognome1: ...
   8    Matricola1: ...
   9    Account1: ...
  10
  11    Nome2: ...
  12    Cognome2: ...
  13    Matricola2: ...
  14    Account2: ...
  15
  16 *)
  17
  18 (*DOCBEGIN
  19
  20 I connettivi logici
  21 ===================
  22
  23 Per digitare i connettivi logici:
  24
  25 * `∧` : `\land`
  26 * `∨` : `\lor`
  27 * `¬` : `\lnot`
  28 * `⇒` : `=>`, `\Rightarrow`
  29 * `⊥` : `\bot`
  30 * `⊤` : `\top`
  31
  32 I termini, le formule e i nomi delle ipotesi
  33 ============================================
  34
  35 * I termini quantificati da `∀` e `∃`, quando argomenti di
  36   una regola, vengono scritti tra `{` e `}`.
  37
  38 * Le formule, quando argomenti di
  39   una regola, vengono scritti tra `(` e `)`.
  40
  41 * I nomi delle ipotesi, quando argomenti di
  42   una regola, vengono scritti tra `[` e `]`.
  43
  44 Le regole di deduzione naturale
  45 ===============================
  46
  47 Per digitare le regole di deduzione naturale
  48 è possibile utilizzare la palette che compare
  49 sulla sinistra dopo aver premuto `F2`.
  50
  51 L'albero si descrive partendo dalla radice. Le regole
  52 con premesse multiple sono seguite da `[`, `|` e `]`.
  53 Ad esempio
  54
  55         apply rule (∧_i (A∨B) ⊥);
  56           [ …continua qui il sottoalbero per (A∨B)
  57           | …continua qui il sottoalbero per ⊥
  58           ]
  59
  60 Le regole vengono applicate alle loro premesse, ovvero
  61 gli argomenti delle regole sono le formule che normalmente
  62 scrivete sopra la linea che rappresenta l'applicazione della
  63 regola stessa.
  64
  65 Le formule sono racchiuse tra `(` e `)`, mentre i nomi
  66 che date ad ipotesi aggiuntive (nella regola di eliminazione
  67 dell' OR, in RAA, e nella regola di introduzione
  68 dell'implicazione) sono ragghiusi tra `[` e `]`.
  69
  70 L'albero di deduzione
  71 =====================
  72
  73 Per visualizzare l'albero man mano che viene costruito
  74 dai comandi impartiti al sistema, premere `F3` e poi
  75 premere sul bottome home (in genere contraddistinto da
  76 una icona rappresentate una casa).
  77
  78 Si suggerisce di marcare tale finestra come `always on top`
  79 utilizzando il menu a tendina che nella maggior parte degli
  80 ambienti grafici si apre cliccando nel suo angolo in
  81 alto a sinistra.
  82
  83 Applicazioni di regole errate vengono contrassegnate con
  84 il colore rosso.
  85
  86 DOCEND*)
  87
  88 include "didactic/support/natural_deduction.ma".
  89
  90 theorem EM: ∀A:CProp. A ∨ ¬ A.
  91 (* Il comando assume è necessario perchè dimostriamo A∨¬A
  92    per una A generica. *)
  93 assume A: CProp.
  94 apply rule (prove (A ∨ ¬A));
  95
  96 apply rule (RAA [H] (⊥)).
  97 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
  98         [ apply rule (discharge [H]).
  99         | apply rule (⊥_e (⊥));
 100           apply rule (¬_e (¬¬A) (¬A));
 101            [ apply rule (¬_i [K] (⊥)).
 102        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
 103               [ (*BEGIN*)apply rule (discharge [H]).(*END*)
 104               | (*BEGIN*)apply rule (∨_i_r (¬A)).
 105           apply rule (discharge [K]).(*END*)
 106               ]
 107            | (*BEGIN*)apply rule (¬_i [K] (⊥)).
 108        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
 109               [ apply rule (discharge [H]).
 110               | apply rule (∨_i_l (A)).
 111           apply rule (discharge [K]).
 112               ](*END*)
 113            ]
 114         ]
 115 qed.
 116
 117 theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
 118 apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
 119 (*BEGIN*)
 120 apply rule (⇒_i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
 121 apply rule (⇒_i [h2] (G ∨ L ⇒ ¬L ⇒ E));
 122 apply rule (⇒_i [h3] (¬L ⇒ E));
 123 apply rule (⇒_i [h4] (E));
 124 apply rule (∨_e (G∨L) [h5] (E) [h6] (E));
 125         [ apply rule (discharge [h3]);
 126         | apply rule (∨_e (E∨C) [h6] (E) [h7] (E));
 127             [ apply rule (⇒_e (¬L ⇒ E∨C) (¬L));
 128                 [ apply rule (discharge [h2]);
 129                 | apply rule (discharge [h4]);
 130                 ]
 131             | apply rule (discharge [h6]);
 132             | apply rule (⇒_e (C∧G ⇒ E) (C∧G));
 133                 [ apply rule (discharge [h1]);
 134                 | apply rule (∧_i (C) (G));
 135                     [ apply rule (discharge [h7]);
 136                     | apply rule (discharge [h5]);
 137                 ]
 138                 ]
 139             ]
 140         | apply rule (⊥_e (⊥));
 141           apply rule (¬_e (¬L) (L));
 142             [ apply rule (discharge [h4]);
 143             | apply rule (discharge [h6]);
 144             ]
 145         ]
 146 (*END*)
 147 qed.
 148
 149 theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
 150 apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
 151 (*BEGIN*)
 152 apply rule (⇒_i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
 153 apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
 154 apply rule (⇒_i [h3] (D ⇒ C));
 155 apply rule (⇒_i [h4] (C));
 156 apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
 157         [ apply rule (lem EM);
 158         | apply rule (⇒_e (B∧D⇒C) (B∧D));
 159             [ apply rule (discharge [h2]);
 160         | apply rule (∧_i (B) (D));
 161                 [ apply rule (discharge [h5]);
 162                 | apply rule (discharge [h4]);
 163                 ]
 164             ]
 165         | apply rule (⇒_e (A∧¬B⇒C) (A∧¬B));
 166             [ apply rule (discharge [h1]);
 167             | apply rule (∧_i (A) (¬B));
 168                 [ apply rule (⇒_e (D⇒A) (D));
 169                     [ apply rule (discharge [h3]);
 170                     | apply rule (discharge [h4]);
 171                     ]
 172                 | apply rule (discharge [h6]);
 173                 ]
 174             ]
 175         ]
 176 (*END*)
 177 qed.
 178
 179 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
 180 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 181 (*BEGIN*)
 182 apply rule (⇒_i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 183 apply rule (⇒_i [h2] ((L⇒F) ⇒ L ⇒ E));
 184 apply rule (⇒_i [h3] (L ⇒ E));
 185 apply rule (⇒_i [h4] (E));
 186 apply rule (∨_e (G∨E) [h5] (E) [h6] (E));
 187         [ apply rule (⇒_e (F ⇒ G∨E) (F));
 188             [ apply rule (discharge [h1]);
 189             | apply rule (⇒_e (L⇒F) (L));
 190                 [ apply rule (discharge [h3]);
 191                 | apply rule (discharge [h4]);
 192                 ]
 193             ]
 194         |apply rule (∨_e (¬L∨E) [h7] (E) [h8] (E));
 195             [ apply rule (⇒_e (G⇒¬L∨E) (G));
 196                 [ apply rule (discharge [h2]);
 197                 | apply rule (discharge [h5]);
 198                 ]
 199             | apply rule (⊥_e (⊥));
 200         apply rule (¬_e (¬L) (L));
 201                 [ apply rule (discharge [h7]);
 202                 | apply rule (discharge [h4]);
 203                 ]
 204             | apply rule (discharge [h8]);
 205             ]
 206         | apply rule (discharge [h6]);
 207         ]
 208 (*END*)
 209 qed.
 210
 211 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
 212 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 213 (*BEGIN*)
 214 apply rule (⇒_i [h1] (¬A∨¬B));
 215 apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
 216         [ apply rule (lem EM);
 217         | apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
 218             [ apply rule (lem EM);
 219             | apply rule (⊥_e (⊥));
 220               apply rule (¬_e (¬(A∧B)) (A∧B));
 221                 [ apply rule (discharge [h1]);
 222                 | apply rule (∧_i (A) (B));
 223                     [ apply rule (discharge [h2]);
 224                     | apply rule (discharge [h4]);
 225                     ]
 226                 ]
 227             | apply rule (∨_i_r (¬B));
 228         apply rule (discharge [h5]);
 229             ]
 230         | apply rule (∨_i_l (¬A));
 231     apply rule (discharge [h3]);
 232         ]
 233 (*END*)
 234 qed.
 235
 236 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
 237 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 238 (*BEGIN*)
 239 apply rule (⇒_i [h1] (¬A ∧ ¬B));
 240 apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
 241         [ apply rule (lem EM);
 242         | apply rule (⊥_e (⊥));
 243     apply rule (¬_e (¬(A∨B)) (A∨B));
 244             [ apply rule (discharge [h1]);
 245             | apply rule (∨_i_l (A));
 246         apply rule (discharge [h2]);
 247             ]
 248         | apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
 249             [ apply rule (lem EM);
 250             | apply rule (⊥_e (⊥));
 251         apply rule (¬_e (¬(A∨B)) (A∨B));
 252                 [ apply rule (discharge [h1]);
 253                 | apply rule (∨_i_r (B));
 254             apply rule (discharge [h10]);
 255                 ]
 256             | apply rule (∧_i (¬A) (¬B));
 257                 [ apply rule (discharge [h3]);
 258                 |apply rule (discharge [h11]);
 259                 ]
 260             ]
 261         ]
 262 (*END*)
 263 qed.
 264
 265 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
 266 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
 267 (*BEGIN*)
 268 apply rule (⇒_i [h1] (¬(A∨B)));
 269 apply rule (¬_i [h2] (⊥));
 270 apply rule (∨_e (A∨B) [h3] (⊥) [h3] (⊥));
 271         [ apply rule (discharge [h2]);
 272         | apply rule (¬_e (¬A) (A));
 273             [ apply rule (∧_e_l (¬A∧¬B));
 274         apply rule (discharge [h1]);
 275             | apply rule (discharge [h3]);
 276             ]
 277         | apply rule (¬_e (¬B) (B));
 278             [ apply rule (∧_e_r (¬A∧¬B));
 279         apply rule (discharge [h1]);
 280             | apply rule (discharge [h3]);
 281             ]
 282         ]
 283 (*END*)
 284 qed.
 285
 286 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
 287 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
 288 (*BEGIN*)
 289 apply rule (⇒_i [h1] (A));
 290 apply rule (RAA [h2] (⊥));
 291 apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
 292         [ apply rule (discharge [h1]);
 293         | apply rule (⇒_i [h3] (⊥));
 294           apply rule (¬_e (¬A) (A));
 295             [ apply rule (discharge [h2]);
 296             | apply rule (discharge [h3]);
 297             ]
 298         ]
 299 (*END*)
 300 qed.
 301