4 Compilare i seguenti campi:
23 Per digitare i connettivi logici:
28 * `⇒` : `=>`, `\Rightarrow`
32 Per digitare i quantificatori:
37 I termini, le formule e i nomi delle ipotesi
38 ============================================
40 * I termini quantificati da `∀` e `∃`, quando argomenti di
41 una regola, vengono scritti tra `{` e `}`.
43 * Le formule, quando argomenti di
44 una regola, vengono scritte tra `(` e `)`.
46 * I nomi delle ipotesi, quando argomenti di
47 una regola, vengono scritti tra `[` e `]`.
53 include "didactic/support/natural_deduction.ma".
55 (* Il nostro linguaggio del primo ordine prevede le seguenti
57 - funzioni: f, g (unarie), h (binaria)
58 - predicati: P, Q (unari), R, S (binari)
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.
69 (* assumiamo il terzo escluso *)
70 axiom EM : ∀A:CProp.A ∨ ¬A.
73 lemma ex1: ¬(∃x.P x) ⇒ ∀x.¬ P x.
74 apply rule (prove (¬(∃x.P x) ⇒ ∀x.¬ P x));
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]);
88 lemma ex2: ¬(∀x.P x) ⇒ ∃x.¬ P x.
89 apply rule (prove (¬(∀x.P x) ⇒ ∃x.¬ P x));
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]);
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));
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]);
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));
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]);
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]);