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

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* Esercizio 0
  16    ===========
  17
  18    Compilare i seguenti campi:
  19
  20    Nome1: ...
  21    Cognome1: ...
  22    Matricola1: ...
  23    Account1: ...
  24
  25    Nome2: ...
  26    Cognome2: ...
  27    Matricola2: ...
  28    Account2: ...
  29
  30 *)
  31
  32 (*DOCBEGIN
  33
  34 I connettivi logici
  35 ===================
  36
  37 Per digitare i connettivi logici:
  38
  39 * `∧` : `\land`
  40 * `∨` : `\lor`
  41 * `¬` : `\lnot`
  42 * `⇒` : `=>`, `\Rightarrow`
  43 * `⊥` : `\bot`
  44 * `⊤` : `\top`
  45
  46 Per digitare i quantificatori:
  47
  48 * `∀` : `\forall`
  49 * `∃` : `\exists`
  50
  51 I termini, le formule e i nomi delle ipotesi
  52 ============================================
  53
  54 * I termini quantificati da `∀` e `∃`, quando argomenti di
  55   una regola, vengono scritti tra `{` e `}`.
  56
  57 * Le formule, quando argomenti di
  58   una regola, vengono scritte tra `(` e `)`.
  59
  60 * I nomi delle ipotesi, quando argomenti di
  61   una regola, vengono scritti tra `[` e `]`.
  62
  63 Le regole di deduzione naturale
  64 ===============================
  65
  66 Per digitare le regole di deduzione naturale
  67 è possibile utilizzare la palette che compare
  68 sulla sinistra dopo aver premuto `F2`.
  69
  70 L'albero si descrive partendo dalla radice. Le regole
  71 con premesse multiple sono seguite da `[`, `|` e `]`.
  72 Ad esempio:
  73
  74         apply rule (∧#i (A∨B) ⊥);
  75           [ …continua qui il sottoalbero per (A∨B)
  76           | …continua qui il sottoalbero per ⊥
  77           ]
  78
  79 Le regole vengono applicate alle loro premesse, ovvero
  80 gli argomenti delle regole sono le formule che normalmente
  81 scrivete sopra la linea che rappresenta l'applicazione della
  82 regola stessa. Ad esempio:
  83
  84         aply rule (∨#e (A∨B) [h1] C [h2] C);
  85           [ …prova di (A∨B)
  86           | …prova di C sotto l'ipotesi A (di nome h1)
  87           | …prova di C sotto l'ipotesi B (di nome h2)
  88           ]
  89
  90 Le regole che hanno una sola premessa non vengono seguite
  91 da parentesi quadre.
  92
  93 L'albero di deduzione
  94 =====================
  95
  96 Per visualizzare l'albero man mano che viene costruito
  97 dai comandi impartiti al sistema, premere `F3` e poi
  98 premere sul bottome home (in genere contraddistinto da
  99 una icona rappresentate una casa).
 100
 101 Si suggerisce di marcare tale finestra come `always on top`
 102 utilizzando il menu a tendina che nella maggior parte degli
 103 ambienti grafici si apre cliccando nel suo angolo in
 104 alto a sinistra.
 105
 106 Applicazioni di regole errate vengono contrassegnate con
 107 il colore rosso.
 108
 109 Usare i lemmi dimostrati in precedenza
 110 ======================================
 111
 112 Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
 113 riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
 114
 115 La "regola" `lem` prende come argomenti:
 116
 117 - Il numero delle ipotesi del lemma che si vuole utilizzare, nel
 118   caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
 119
 120 - Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
 121
 122 - Infine, le formule che devono essere scritte come premesse per la
 123   "regola".
 124
 125 Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
 126 `lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
 127 `lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario
 128 far seguire le parentesi quadre come spiegato in precedenza.
 129
 130 Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
 131 per rappresentare l'albero di prova del lemma che si sta riutilizzando.
 132
 133 Per motivi che saranno più chiari una volta studiate logiche del
 134 primo ordine o di ordine superiore, i lemmi che si intende
 135 riutilizzare è bene che siano dimostrati astratti sugli atomi.
 136 Ovvero per ogni atomo `A`...`Z` che compare nella formula,
 137 è bene aggiungere una quantificazione all'inizio della formula stessa.
 138 Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
 139 La dimostrazione deve poi iniziare con il comando `assume`.
 140
 141 In tale modo il lemma EM può essere utilizzato sia per dimostrare
 142 `A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
 143
 144 DOCEND*)
 145
 146
 147 include "didactic/support/natural_deduction.ma".
 148
 149 (* Il nostro linguaggio del primo ordine prevede le seguenti
 150    - costanti: c
 151    - funzioni: f, g (unarie), h (binaria)
 152    - predicati: P, Q (unari), R, S (binari)
 153 *)
 154 axiom c : sort.
 155 axiom f : sort → sort.
 156 axiom g : sort → sort.
 157 axiom h : sort → sort → sort.
 158 axiom P : sort → CProp.
 159 axiom Q : sort → CProp.
 160 axiom R : sort →sort → CProp.
 161 axiom S : sort →sort → CProp.
 162
 163 (* assumiamo il terzo escluso *)
 164 theorem EM: ∀A:CProp. A ∨ ¬ A.
 165 assume A: CProp.
 166 apply rule (prove (A ∨ ¬A));
 167 apply rule (RAA [H] (⊥)).
 168 apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
 169         [ apply rule (discharge [H]).
 170         | apply rule (⊥#e (⊥));
 171           apply rule (¬#e (¬¬A) (¬A));
 172            [ apply rule (¬#i [K] (⊥)).
 173        apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
 174               [ apply rule (discharge [H]).
 175               | apply rule (∨#i_r (¬A)).
 176           apply rule (discharge [K]).
 177               ]
 178            | apply rule (¬#i [K] (⊥)).
 179        apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
 180               [ apply rule (discharge [H]).
 181               | apply rule (∨#i_l (A)).
 182           apply rule (discharge [K]).
 183               ]
 184            ]
 185         ]
 186 qed.
 187
 188 (* intuizionista *)
 189 lemma ex1: ¬(∃x.P x) ⇒ ∀x.¬ P x.
 190 apply rule (prove (¬(∃x.P x) ⇒ ∀x.¬ P x));
 191 (*BEGIN*)
 192 apply rule (⇒#i [h1] (∀x.¬ P x));
 193 apply rule (∀#i {l} (¬P l));
 194 apply rule (¬#i [h2] (⊥));
 195 apply rule (¬#e (¬(∃x.P x)) (∃x.P x));
 196         [ apply rule (discharge [h1]);
 197         | apply rule (∃#i {l} (P l));
 198           apply rule (discharge [h2]);
 199         ]
 200 (*END*)
 201 qed.
 202
 203 (* classico *)
 204 lemma ex2: ¬(∀x.P x) ⇒ ∃x.¬ P x.
 205 apply rule (prove (¬(∀x.P x) ⇒ ∃x.¬ P x));
 206 (*BEGIN*)
 207 apply rule (⇒#i [h1] (∃x.¬ P x));
 208 apply rule (RAA [h2] (⊥));
 209 apply rule (¬#e (¬(∀x.P x)) (∀x.P x));
 210         [ apply rule (discharge [h2]);
 211         | apply rule (∀#i {y} (P y));
 212     apply rule (RAA [h3] (⊥));
 213     apply rule (¬#e (¬∃x.¬ P x) (∃x.¬ P x));
 214            [ apply rule (discharge [h2]);
 215            | apply rule (∃#i {y} (¬P y));
 216        apply rule (discharge [h3]);
 217            ]
 218         ]
 219 (*END*)
 220 qed.
 221
 222 (* intuizionista *)
 223 lemma ex3: ((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c.
 224 apply rule (prove (((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c));
 225 (*BEGIN*)
 226 apply rule (⇒#i [h1] (∀x.P x ⇒ Q c));
 227 apply rule (∀#i {l} (P l ⇒ Q c));
 228 apply rule (⇒#i [h2] (Q c));
 229 apply rule (⇒#e ((∃x.P x) ⇒ Q c) (∃x.P x));
 230         [ apply rule (discharge [h1]);
 231         | apply rule (∃#i {l} (P l));
 232           apply rule (discharge [h2]);
 233         ]
 234 (*END*)
 235 qed.
 236
 237 (* classico *)
 238 lemma ex4: ((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c.
 239 apply rule (prove (((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c));
 240 (*BEGIN*)
 241 apply rule (⇒#i [h1] (∃x.P x ⇒ Q c));
 242 apply rule (∨#e ((∀x.P x) ∨ ¬(∀x.P x)) [h3] (?) [h3] (?));
 243         [ apply rule (lem 0 EM);
 244         | apply rule (∃#i {y} (P y ⇒ Q c));
 245        apply rule (⇒#i [h4] (Q c));
 246        apply rule (⇒#e ((∀x.P x) ⇒ Q c) ((∀x.P x)));
 247                [ apply rule (discharge [h1]);
 248          | apply rule (discharge [h3]);
 249                ]
 250   | apply rule (∃#e (∃x.¬P x) {y} [h4] (∃x.P x ⇒ Q c));
 251            [ apply rule (lem 1 ex2 (¬(∀x.P x)));
 252              apply rule (discharge [h3]);
 253      | apply rule (∃#i {y} (P y ⇒ Q c));
 254        apply rule (⇒#i [h5] (Q c));
 255        apply rule (⊥#e (⊥));
 256        apply rule (¬#e (¬P y) (P y));
 257                [ apply rule (discharge [h4]);
 258                | apply rule (discharge [h5]);
 259                ]
 260            ]
 261   ]
 262 (*END*)
 263 qed.