3 http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html
10 Compilare i seguenti campi:
24 include "didactic/support/natural_deduction.ma".
26 theorem EM: ∀A:CProp. A ∨ ¬ A.
28 apply rule (prove (A ∨ ¬A));
29 apply rule (RAA [H] (⊥)).
30 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
31 [ apply rule (discharge [H]).
32 | apply rule (⊥_e (⊥));
33 apply rule (¬_e (¬¬A) (¬A));
34 [ apply rule (¬_i [K] (⊥)).
35 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
36 [ apply rule (discharge [H]).
37 | apply rule (∨_i_r (¬A)).
38 apply rule (discharge [K]).
40 | apply rule (¬_i [K] (⊥)).
41 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
42 [ apply rule (discharge [H]).
43 | apply rule (∨_i_l (A)).
44 apply rule (discharge [K]).
50 theorem ex0 : (F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E.
51 apply rule (prove ((F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
53 apply rule (⇒_i [h1] ((G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
54 apply rule (⇒_i [h2] (F ∧ L ⇒ E));
55 apply rule (⇒_i [h3] (E));
56 apply rule (∨_e (G∨¬G) [h4] (E) [h4] (E));
57 [ apply rule (lem 0 EM);
58 | apply rule (⇒_e (G∧L⇒E) (G∧L));
59 [ apply rule (discharge [h2]);
60 | apply rule (∧_i (G) (L));
61 [ apply rule (discharge [h4]);
62 | apply rule (∧_e_r (F∧L));
63 apply rule (discharge [h3]);
66 | apply rule (⇒_e (L⇒E) (L));
67 [ apply rule (⇒_e (F∧¬G ⇒ L ⇒ E) (F∧¬G));
68 [ apply rule (discharge [h1]);
69 | apply rule (∧_i (F) (¬G));
70 [ apply rule (∧_e_l (F∧L));
71 apply rule (discharge [h3]);
72 | apply rule (discharge [h4]);
75 | apply rule (∧_e_r (F∧L));
76 apply rule (discharge [h3]);
82 theorem ex1 : (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E.
83 apply rule (prove (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E);
85 apply rule (⇒_i [h1] ((G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E));
86 apply rule (⇒_i [h2] ((¬L ∨ F) ⇒ L ⇒ E));
87 apply rule (⇒_i [h3] (L ⇒ E));
88 apply rule (⇒_i [h4] (E));
89 apply rule (∨_e (¬L∨F) [h5] (E) [h5] (E));
90 [ apply rule (discharge [h3]);
91 | apply rule (⊥_e (⊥));
92 apply rule (¬_e (¬L) (L));
93 [ apply rule (discharge [h5]);
94 | apply rule (discharge [h4]);
96 | apply rule (∨_e (G∨E) [h6] (E) [h6] (E));
97 [ apply rule (⇒_e (F⇒G∨E) (F));
98 [ apply rule (discharge [h1]);
99 | apply rule (discharge [h5]);
101 | apply rule (RAA [h7] (⊥));
102 apply rule (¬_e (¬ (L ∧ ¬E)) (L ∧ ¬E));
103 [ apply rule (⇒_e (G ⇒ ¬ (L ∧ ¬E)) (G));
104 [apply rule (discharge [h2]);
105 |apply rule (discharge [h6]);
107 | apply rule (∧_i (L) (¬E));
108 [ apply rule (discharge [h4]);
109 | apply rule (discharge [h7]);
112 | apply rule (discharge [h6]);
118 theorem ex2 : (F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E.
119 apply rule (prove ((F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
121 apply rule (⇒_i [h1] ((H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
122 apply rule (⇒_i [h2] ((¬G ⇒ ¬H) ⇒ H ⇒ E));
123 apply rule (⇒_i [h3] (H ⇒ E));
124 apply rule (⇒_i [h4] (E));
125 apply rule (∨_e (G∨¬G) [h5] (E) [h5] (E));
126 [apply rule (lem 0 EM);
127 | apply rule (∨_e (E∨F) [h6] (E) [h6] (E));
128 [ apply rule (⇒_e (H ⇒ E∨F) (H));
129 [ apply rule (discharge [h2]);
130 | apply rule (discharge [h4]);
132 | apply rule (discharge [h6]);
133 | apply rule (⇒_e (F∧G ⇒ E) (F∧G));
134 [apply rule (discharge [h1]);
135 |apply rule (∧_i (F) (G));
136 [ apply rule (discharge [h6]);
137 | apply rule (discharge [h5]);
141 | apply rule (⊥_e (⊥));
142 apply rule (¬_e (¬H) (H));
143 [ apply rule (⇒_e (¬G ⇒ ¬H) (¬G));
144 [ apply rule (discharge [h3]);
145 | apply rule (discharge [h5]);
147 | apply rule (discharge [h4]);
153 theorem ex3 : (F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E.
154 apply rule (prove ((F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E)).
156 apply rule (⇒_i [h1] ((¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E));
157 apply rule (⇒_i [h2] ((L ⇒ F) ⇒ L ⇒ E));
158 apply rule (⇒_i [h3] (L ⇒ E));
159 apply rule (⇒_i [h4] (E));
160 apply rule (RAA [h5] (⊥));
161 apply rule (∨_e (G∨¬L) [h6] (⊥) [h6] (⊥));
162 [ apply rule (⇒_e (¬E ⇒ G∨¬L) (¬E));
163 [ apply rule (discharge [h2]);
164 | apply rule (discharge [h5]);
166 | apply rule (¬_e (¬E) (E));
167 [ apply rule (discharge [h5]);
168 | apply rule (⇒_e (F∧G ⇒ E) (F∧G));
169 [ apply rule (discharge [h1]);
170 | apply rule (∧_i (F) (G));
171 [ apply rule (⇒_e (L⇒F) (L));
172 [ apply rule (discharge [h3]);
173 | apply rule (discharge [h4]);
175 | apply rule (discharge [h6]);
179 | apply rule (¬_e (¬L) (L));
180 [ apply rule (discharge [h6]);
181 | apply rule (discharge [h4]);