4 Compilare i seguenti campi:
23 Per digitare i connettivi logici:
28 * `⇒` : `=>`, `\Rightarrow`
32 Le regole di deduzione naturale
33 ===============================
35 Per digitare le regole di deduzione naturale
36 è possibile utilizzare la palette che compare
37 sulla sinistra dopo aver premuto `F2`.
39 L'albero si descrive partendo dalla radice. Le regole
40 con premesse multiple sono seguite da `[`, `|` e `]`.
43 apply rule (∧_i (A∨B) ⊥);
44 [ …continua qui il sottoalbero per (A∨B)
45 | …continua qui il sottoalbero per ⊥
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
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 `]`.
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).
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
71 Applicazioni di regole errate vengono contrassegnate con
76 include "didactic/support/natural_deduction.ma".
78 theorem EM: ∀A. A ∨ ¬ A.
79 (* Il comando assume è necessario perchè dimostriamo A∨¬A
80 per una A generica. *)
82 apply rule (prove (A ∨ ¬A));
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*)
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]).
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));
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]);
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]);
128 | apply rule (⊥_e (⊥));
129 apply rule (¬_e (¬L) (L));
130 [ apply rule (discharge [h4]);
131 | apply rule (discharge [h6]);
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));
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]);
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]);
160 | apply rule (discharge [h6]);
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));
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]);
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]);
187 | apply rule (⊥_e (⊥));
188 apply rule (¬_e (¬L) (L));
189 [ apply rule (discharge [h7]);
190 | apply rule (discharge [h4]);
192 | apply rule (discharge [h8]);
194 | apply rule (discharge [h6]);
199 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
200 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
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]);
215 | apply rule (∨_i_r (¬B));
216 apply rule (discharge [h5]);
218 | apply rule (∨_i_l (¬A));
219 apply rule (discharge [h3]);
224 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
225 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
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]);
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]);
244 | apply rule (∧_i (¬A) (¬B));
245 [ apply rule (discharge [h3]);
246 |apply rule (discharge [h11]);
253 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
254 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
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]);
265 | apply rule (¬_e (¬B) (B));
266 [ apply rule (∧_e_r (¬A∧¬B));
267 apply rule (discharge [h1]);
268 | apply rule (discharge [h3]);
274 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
275 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
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]);