]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
updating the structures for sorts
[helm.git] / helm / software / matita / library / didactic / exercises / natural_deduction_fst_order.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* Esercizio 0
16    ===========
17
18    Compilare i seguenti campi:
19
20    Nome1: ...
21    Cognome1: ...
22    Matricola1: ...
23    Account1: ...
24
25    Nome2: ...
26    Cognome2: ...
27    Matricola2: ...
28    Account2: ...
29
30 *)
31
32 (*DOCBEGIN
33
34 I connettivi logici
35 ===================
36
37 Per digitare i connettivi logici:
38
39 * `∧` : `\land`
40 * `∨` : `\lor`
41 * `¬` : `\lnot`
42 * `⇒` : `=>`, `\Rightarrow` 
43 * `⊥` : `\bot`
44 * `⊤` : `\top`
45
46 Per digitare i quantificatori:
47
48 * `∀` : `\forall`
49 * `∃` : `\exists`
50
51 I termini, le formule e i nomi delle ipotesi
52 ============================================
53
54 * I termini quantificati da `∀` e `∃`, quando argomenti di
55   una regola, vengono scritti tra `{` e `}`.
56
57 * Le formule, quando argomenti di
58   una regola, vengono scritte tra `(` e `)`.
59
60 * I nomi delle ipotesi, quando argomenti di
61   una regola, vengono scritti tra `[` e `]`.
62
63 Le regole di deduzione naturale
64 ===============================
65
66 Per digitare le regole di deduzione naturale
67 è possibile utilizzare la palette che compare
68 sulla sinistra dopo aver premuto `F2`.
69
70 L'albero si descrive partendo dalla radice. Le regole
71 con premesse multiple sono seguite da `[`, `|` e `]`.
72 Ad esempio: 
73
74         apply rule (∧#i (A∨B) ⊥);
75           [ …continua qui il sottoalbero per (A∨B)
76           | …continua qui il sottoalbero per ⊥
77           ] 
78
79 Le regole vengono applicate alle loro premesse, ovvero
80 gli argomenti delle regole sono le formule che normalmente 
81 scrivete sopra la linea che rappresenta l'applicazione della
82 regola stessa. Ad esempio:
83
84         aply rule (∨#e (A∨B) [h1] C [h2] C);
85           [ …prova di (A∨B)
86           | …prova di C sotto l'ipotesi A (di nome h1)  
87           | …prova di C sotto l'ipotesi B (di nome h2)
88           ]
89
90 Le regole che hanno una sola premessa non vengono seguite 
91 da parentesi quadre.
92
93 L'albero di deduzione
94 =====================
95
96 Per visualizzare l'albero man mano che viene costruito
97 dai comandi impartiti al sistema, premere `F3` e poi
98 premere sul bottome home (in genere contraddistinto da
99 una icona rappresentate una casa).
100
101 Si suggerisce di marcare tale finestra come `always on top`
102 utilizzando il menu a tendina che nella maggior parte degli
103 ambienti grafici si apre cliccando nel suo angolo in 
104 alto a sinistra.
105
106 Applicazioni di regole errate vengono contrassegnate con
107 il colore rosso.
108
109 Usare i lemmi dimostrati in precedenza
110 ======================================
111
112 Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
113 riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
114
115 La "regola" `lem` prende come argomenti:
116
117 - Il numero delle ipotesi del lemma che si vuole utilizzare, nel
118   caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
119
120 - Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
121
122 - Infine, le formule che devono essere scritte come premesse per la 
123   "regola".
124
125 Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
126 `lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
127 `lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario 
128 far seguire le parentesi quadre come spiegato in precedenza.
129
130 Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
131 per rappresentare l'albero di prova del lemma che si sta riutilizzando.
132
133 Per motivi che saranno più chiari una volta studiate logiche del 
134 primo ordine o di ordine superiore, i lemmi che si intende 
135 riutilizzare è bene che siano dimostrati astratti sugli atomi. 
136 Ovvero per ogni atomo `A`...`Z` che compare nella formula, 
137 è bene aggiungere una quantificazione all'inizio della formula stessa.
138 Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
139 La dimostrazione deve poi iniziare con il comando `assume`. 
140
141 In tale modo il lemma EM può essere utilizzato sia per dimostrare 
142 `A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
143
144 DOCEND*)
145
146
147 include "didactic/support/natural_deduction.ma".
148
149 (* Il nostro linguaggio del primo ordine prevede le seguenti 
150    - costanti: c
151    - funzioni: f, g (unarie), h (binaria)
152    - predicati: P, Q (unari), R, S (binari) 
153 *)
154 axiom c : sort.
155 axiom f : sort → sort.
156 axiom g : sort → sort.
157 axiom h : sort → sort → sort.
158 axiom P : sort → CProp.
159 axiom Q : sort → CProp.
160 axiom R : sort →sort → CProp.
161 axiom S : sort →sort → CProp.
162
163 (* assumiamo il terzo escluso *)
164 theorem EM: ∀A:CProp. A ∨ ¬ A.
165 assume A: CProp.
166 apply rule (prove (A ∨ ¬A));
167 apply rule (RAA [H] (⊥)).
168 apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
169         [ apply rule (discharge [H]).
170         | apply rule (⊥#e (⊥));
171           apply rule (¬#e (¬¬A) (¬A));
172            [ apply rule (¬#i [K] (⊥)).
173        apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
174               [ apply rule (discharge [H]).
175               | apply rule (∨#i_r (¬A)).
176           apply rule (discharge [K]).
177               ]
178            | apply rule (¬#i [K] (⊥)).
179        apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
180               [ apply rule (discharge [H]).
181               | apply rule (∨#i_l (A)).
182           apply rule (discharge [K]).
183               ]
184            ]
185         ]
186 qed.
187
188 (* intuizionista *)
189 lemma ex1: ¬(∃x.P x) ⇒ ∀x.¬ P x.
190 apply rule (prove (¬(∃x.P x) ⇒ ∀x.¬ P x));
191 (*BEGIN*)
192 apply rule (⇒#i [h1] (∀x.¬ P x));
193 apply rule (∀#i {l} (¬P l));
194 apply rule (¬#i [h2] (⊥));
195 apply rule (¬#e (¬(∃x.P x)) (∃x.P x));
196         [ apply rule (discharge [h1]);
197         | apply rule (∃#i {l} (P l));
198           apply rule (discharge [h2]);
199         ]
200 (*END*)
201 qed.
202
203 (* classico *)
204 lemma ex2: ¬(∀x.P x) ⇒ ∃x.¬ P x.
205 apply rule (prove (¬(∀x.P x) ⇒ ∃x.¬ P x));
206 (*BEGIN*)
207 apply rule (⇒#i [h1] (∃x.¬ P x));
208 apply rule (RAA [h2] (⊥));
209 apply rule (¬#e (¬(∀x.P x)) (∀x.P x));
210         [ apply rule (discharge [h2]);
211         | apply rule (∀#i {y} (P y));
212     apply rule (RAA [h3] (⊥));
213     apply rule (¬#e (¬∃x.¬ P x) (∃x.¬ P x));
214            [ apply rule (discharge [h2]);
215            | apply rule (∃#i {y} (¬P y));
216        apply rule (discharge [h3]);
217            ]
218         ]
219 (*END*)
220 qed.
221
222 (* intuizionista *)
223 lemma ex3: ((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c.
224 apply rule (prove (((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c));
225 (*BEGIN*)
226 apply rule (⇒#i [h1] (∀x.P x ⇒ Q c));
227 apply rule (∀#i {l} (P l ⇒ Q c));
228 apply rule (⇒#i [h2] (Q c));
229 apply rule (⇒#e ((∃x.P x) ⇒ Q c) (∃x.P x));
230         [ apply rule (discharge [h1]);
231         | apply rule (∃#i {l} (P l));
232           apply rule (discharge [h2]);
233         ]
234 (*END*)
235 qed.
236
237 (* classico *)
238 lemma ex4: ((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c.
239 apply rule (prove (((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c));
240 (*BEGIN*)
241 apply rule (⇒#i [h1] (∃x.P x ⇒ Q c));
242 apply rule (∨#e ((∀x.P x) ∨ ¬(∀x.P x)) [h3] (?) [h3] (?));
243         [ apply rule (lem 0 EM);
244         | apply rule (∃#i {y} (P y ⇒ Q c));
245        apply rule (⇒#i [h4] (Q c));
246        apply rule (⇒#e ((∀x.P x) ⇒ Q c) ((∀x.P x)));
247                [ apply rule (discharge [h1]);
248          | apply rule (discharge [h3]);
249                ]
250   | apply rule (∃#e (∃x.¬P x) {y} [h4] (∃x.P x ⇒ Q c));
251            [ apply rule (lem 1 ex2 (¬(∀x.P x)));
252              apply rule (discharge [h3]);
253      | apply rule (∃#i {y} (P y ⇒ Q c));
254        apply rule (⇒#i [h5] (Q c));
255        apply rule (⊥#e (⊥));
256        apply rule (¬#e (¬P y) (P y));
257                [ apply rule (discharge [h4]);
258                | apply rule (discharge [h5]);
259                ]
260            ]
261   ]
262 (*END*)
263 qed.