4 Compilare i seguenti campi:
23 Per digitare i connettivi logici:
28 * `⇒` : `=>`, `\Rightarrow`
32 I termini, le formule e i nomi delle ipotesi
33 ============================================
35 * I termini quantificati da `∀` e `∃`, quando argomenti di
36 una regola, vengono scritti tra `{` e `}`.
38 * Le formule, quando argomenti di
39 una regola, vengono scritti tra `(` e `)`.
41 * I nomi delle ipotesi, quando argomenti di
42 una regola, vengono scritti tra `[` e `]`.
44 Le regole di deduzione naturale
45 ===============================
47 Per digitare le regole di deduzione naturale
48 è possibile utilizzare la palette che compare
49 sulla sinistra dopo aver premuto `F2`.
51 L'albero si descrive partendo dalla radice. Le regole
52 con premesse multiple sono seguite da `[`, `|` e `]`.
55 apply rule (∧_i (A∨B) ⊥);
56 [ …continua qui il sottoalbero per (A∨B)
57 | …continua qui il sottoalbero per ⊥
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
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 `]`.
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).
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
83 Applicazioni di regole errate vengono contrassegnate con
88 include "didactic/support/natural_deduction.ma".
90 theorem EM: ∀A:CProp. A ∨ ¬ A.
91 (* Il comando assume è necessario perchè dimostriamo A∨¬A
92 per una A generica. *)
94 apply rule (prove (A ∨ ¬A));
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*)
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]).
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));
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]);
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]);
140 | apply rule (⊥_e (⊥));
141 apply rule (¬_e (¬L) (L));
142 [ apply rule (discharge [h4]);
143 | apply rule (discharge [h6]);
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));
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]);
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]);
172 | apply rule (discharge [h6]);
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));
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]);
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]);
199 | apply rule (⊥_e (⊥));
200 apply rule (¬_e (¬L) (L));
201 [ apply rule (discharge [h7]);
202 | apply rule (discharge [h4]);
204 | apply rule (discharge [h8]);
206 | apply rule (discharge [h6]);
211 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
212 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
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]);
227 | apply rule (∨_i_r (¬B));
228 apply rule (discharge [h5]);
230 | apply rule (∨_i_l (¬A));
231 apply rule (discharge [h3]);
236 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
237 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
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]);
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]);
256 | apply rule (∧_i (¬A) (¬B));
257 [ apply rule (discharge [h3]);
258 |apply rule (discharge [h11]);
265 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
266 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
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]);
277 | apply rule (¬_e (¬B) (B));
278 [ apply rule (∧_e_r (¬A∧¬B));
279 apply rule (discharge [h1]);
280 | apply rule (discharge [h3]);
286 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
287 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
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]);