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