helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.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 Per digitare i quantificatori:
  33
  34 * `∀` : `\forall`
  35 * `∃` : `\exists`
  36
  37 I termini, le formule e i nomi delle ipotesi
  38 ============================================
  39
  40 * I termini quantificati da `∀` e `∃`, quando argomenti di
  41   una regola, vengono scritti tra `{` e `}`.
  42
  43 * Le formule, quando argomenti di
  44   una regola, vengono scritte tra `(` e `)`.
  45
  46 * I nomi delle ipotesi, quando argomenti di
  47   una regola, vengono scritti tra `[` e `]`.
  48
  49
  50 DOCEND*)
  51
  52
  53 include "didactic/support/natural_deduction.ma".
  54
  55 (* Il nostro linguaggio del primo ordine prevede le seguenti
  56    - costanti: c
  57    - funzioni: f, g (unarie), h (binaria)
  58    - predicati: P, Q (unari), R, S (binari)
  59 *)
  60 axiom c : sort.
  61 axiom f : sort → sort.
  62 axiom g : sort → sort.
  63 axiom h : sort → sort → sort.
  64 axiom P : sort → CProp.
  65 axiom Q : sort → CProp.
  66 axiom R : sort →sort → CProp.
  67 axiom S : sort →sort → CProp.
  68
  69 (* assumiamo il terzo escluso *)
  70 axiom EM : ∀A:CProp.A ∨ ¬A.
  71
  72 (* intuizionista *)
  73 lemma ex1: ¬(∃x.P x) ⇒ ∀x.¬ P x.
  74 apply rule (prove (¬(∃x.P x) ⇒ ∀x.¬ P x));
  75 (*BEGIN*)
  76 apply rule (⇒_i [h1] (∀x.¬ P x));
  77 apply rule (∀_i {l} (¬P l));
  78 apply rule (¬_i [h2] (⊥));
  79 apply rule (¬_e (¬(∃x.P x)) (∃x.P x));
  80         [ apply rule (discharge [h1]);
  81         | apply rule (∃_i {l} (P l));
  82           apply rule (discharge [h2]);
  83         ]
  84 (*END*)
  85 qed.
  86
  87 (* classico *)
  88 lemma ex2: ¬(∀x.P x) ⇒ ∃x.¬ P x.
  89 apply rule (prove (¬(∀x.P x) ⇒ ∃x.¬ P x));
  90 (*BEGIN*)
  91 apply rule (⇒_i [h1] (∃x.¬ P x));
  92 apply rule (RAA [h2] (⊥));
  93 apply rule (¬_e (¬(∀x.P x)) (∀x.P x));
  94         [ apply rule (discharge [h1]);
  95         | apply rule (∀_i {y} (P y));
  96     apply rule (RAA [h3] (⊥));
  97     apply rule (¬_e (¬∃x.¬ P x) (∃x.¬ P x));
  98            [ apply rule (discharge [h2]);
  99            | apply rule (∃_i {y} (¬P y));
 100        apply rule (discharge [h3]);
 101            ]
 102         ]
 103 (*END*)
 104 qed.
 105
 106 (* intuizionista *)
 107 lemma ex3: ((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c.
 108 apply rule (prove (((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c));
 109 (*BEGIN*)
 110 apply rule (⇒_i [h1] (∀x.P x ⇒ Q c));
 111 apply rule (∀_i {l} (P l ⇒ Q c));
 112 apply rule (⇒_i [h2] (Q c));
 113 apply rule (⇒_e ((∃x.P x) ⇒ Q c) (∃x.P x));
 114         [ apply rule (discharge [h1]);
 115         | apply rule (∃_i {l} (P l));
 116           apply rule (discharge [h2]);
 117         ]
 118 (*END*)
 119 qed.
 120
 121 (* classico *)
 122 lemma ex4: ((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c.
 123 apply rule (prove (((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c));
 124 (*BEGIN*)
 125 apply rule (⇒_i [h1] (∃x.P x ⇒ Q c));
 126 apply rule (∨_e ((∀x.P x) ∨ ¬(∀x.P x)) [h3] (?) [h3] (?));
 127         [ apply rule (lem 0 EM);
 128         | apply rule (∃_i {y} (P y ⇒ Q c));
 129        apply rule (⇒_i [h4] (Q c));
 130        apply rule (⇒_e ((∀x.P x) ⇒ Q c) ((∀x.P x)));
 131                [ apply rule (discharge [h1]);
 132          | apply rule (discharge [h3]);
 133                ]
 134   | apply rule (∃_e (∃x.¬P x) {y} [h4] (∃x.P x ⇒ Q c));
 135            [ apply rule (lem 1 ex2 (¬(∀x.P x)));
 136              apply rule (discharge [h3]);
 137      | apply rule (∃_i {y} (P y ⇒ Q c));
 138        apply rule (⇒_i [h5] (Q c));
 139        apply rule (⊥_e (⊥));
 140        apply rule (¬_e (¬P y) (P y));
 141                [ apply rule (discharge [h4]);
 142                | apply rule (discharge [h5]);
 143                ]
 144            ]
 145   ]
 146 (*END*)
 147 qed.