+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+(* Istruzioni:
+
+ http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html
+
+*)
+
(* Esercizio 0
===========
(*DOCBEGIN
+Scopo della lezione
+===================
+
+Lo scopo della lezione è di farvi imparare ad usare Matita
+per auto-correggervi gli esercizi di deduzione naturale, che
+saranno parte dell'esame scritto. Il consiglio è di
+fare prima gli esercizi su carta e poi digitarli in Matita
+per verificarne la correttezza. Fare direttamente gli esercizi
+con Matita è difficile e richiede molto più tempo.
+
I connettivi logici
===================
I termini, le formule e i nomi delle ipotesi
============================================
-* I termini quantificati da `∀` e `∃`, quando argomenti di
- una regola, vengono scritti tra `{` e `}`.
-
* Le formule, quando argomenti di
- una regola, vengono scritti tra `(` e `)`.
+ una regola, vengono scritte tra `(` e `)`.
* I nomi delle ipotesi, quando argomenti di
una regola, vengono scritti tra `[` e `]`.
L'albero si descrive partendo dalla radice. Le regole
con premesse multiple sono seguite da `[`, `|` e `]`.
-Ad esempio
+Ad esempio:
- apply rule (∧_i (A∨B) ⊥);
+ apply rule (∧#i (A∨B) ⊥);
[ …continua qui il sottoalbero per (A∨B)
| …continua qui il sottoalbero per ⊥
]
Le regole vengono applicate alle loro premesse, ovvero
gli argomenti delle regole sono le formule che normalmente
scrivete sopra la linea che rappresenta l'applicazione della
-regola stessa.
+regola stessa. Ad esempio:
+
+ aply rule (∨#e (A∨B) [h1] C [h2] C);
+ [ …prova di (A∨B)
+ | …prova di C sotto l'ipotesi A (di nome h1)
+ | …prova di C sotto l'ipotesi B (di nome h2)
+ ]
-Le formule sono racchiuse tra `(` e `)`, mentre i nomi
-che date ad ipotesi aggiuntive (nella regola di eliminazione
-dell' OR, in RAA, e nella regola di introduzione
-dell'implicazione) sono ragghiusi tra `[` e `]`.
+Le regole che hanno una sola premessa non vengono seguite
+da parentesi quadre.
L'albero di deduzione
=====================
Applicazioni di regole errate vengono contrassegnate con
il colore rosso.
+Usare i lemmi dimostrati in precedenza
+======================================
+
+Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
+riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
+
+La "regola" `lem` prende come argomenti:
+
+- Il numero delle ipotesi del lemma che si vuole utilizzare, nel
+ caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
+
+- Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
+
+- Infine, le formule che devono essere scritte come premesse per la
+ "regola".
+
+Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
+`lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
+`lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario
+far seguire le parentesi quadre come spiegato in precedenza.
+
+Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
+per rappresentare l'albero di prova del lemma che si sta riutilizzando.
+
+Per motivi che saranno più chiari una volta studiate logiche del
+primo ordine o di ordine superiore, i lemmi che si intende
+riutilizzare è bene che siano dimostrati astratti sugli atomi.
+Ovvero per ogni atomo `A`...`Z` che compare nella formula,
+è bene aggiungere una quantificazione all'inizio della formula stessa.
+Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
+La dimostrazione deve poi iniziare con il comando `assume`.
+
+In tale modo il lemma EM può essere utilizzato sia per dimostrare
+`A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
+
DOCEND*)
include "didactic/support/natural_deduction.ma".
(* Il comando assume è necessario perchè dimostriamo A∨¬A
per una A generica. *)
assume A: CProp.
+(* Questo comando inizia a disegnare l'albero *)
apply rule (prove (A ∨ ¬A));
-
+(* qui inizia l'albero, eseguite passo passo osservando come
+ si modifica l'albero. *)
apply rule (RAA [H] (⊥)).
-apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
[ apply rule (discharge [H]).
- | apply rule (⊥_e (⊥));
- apply rule (¬_e (¬¬A) (¬A));
- [ apply rule (¬_i [K] (⊥)).
- apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬¬A) (¬A));
+ [ apply rule (¬#i [K] (⊥)).
+ apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
[ (*BEGIN*)apply rule (discharge [H]).(*END*)
- | (*BEGIN*)apply rule (∨_i_r (¬A)).
+ | (*BEGIN*)apply rule (∨#i_r (¬A)).
apply rule (discharge [K]).(*END*)
]
- | (*BEGIN*)apply rule (¬_i [K] (⊥)).
- apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ | (*BEGIN*)apply rule (¬#i [K] (⊥)).
+ apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
[ apply rule (discharge [H]).
- | apply rule (∨_i_l (A)).
+ | apply rule (∨#i_l (A)).
apply rule (discharge [K]).
](*END*)
]
theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
(*BEGIN*)
-apply rule (⇒_i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
-apply rule (⇒_i [h2] (G ∨ L ⇒ ¬L ⇒ E));
-apply rule (⇒_i [h3] (¬L ⇒ E));
-apply rule (⇒_i [h4] (E));
-apply rule (∨_e (G∨L) [h5] (E) [h6] (E));
+apply rule (⇒#i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
+apply rule (⇒#i [h2] (G ∨ L ⇒ ¬L ⇒ E));
+apply rule (⇒#i [h3] (¬L ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (G∨L) [h5] (E) [h6] (E));
[ apply rule (discharge [h3]);
- | apply rule (∨_e (E∨C) [h6] (E) [h7] (E));
- [ apply rule (⇒_e (¬L ⇒ E∨C) (¬L));
+ | apply rule (∨#e (E∨C) [h6] (E) [h7] (E));
+ [ apply rule (⇒#e (¬L ⇒ E∨C) (¬L));
[ apply rule (discharge [h2]);
| apply rule (discharge [h4]);
]
| apply rule (discharge [h6]);
- | apply rule (⇒_e (C∧G ⇒ E) (C∧G));
+ | apply rule (⇒#e (C∧G ⇒ E) (C∧G));
[ apply rule (discharge [h1]);
- | apply rule (∧_i (C) (G));
+ | apply rule (∧#i (C) (G));
[ apply rule (discharge [h7]);
| apply rule (discharge [h5]);
]
]
]
- | apply rule (⊥_e (⊥));
- apply rule (¬_e (¬L) (L));
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬L) (L));
[ apply rule (discharge [h4]);
| apply rule (discharge [h6]);
]
theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
(*BEGIN*)
-apply rule (⇒_i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
-apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
-apply rule (⇒_i [h3] (D ⇒ C));
-apply rule (⇒_i [h4] (C));
-apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
- [ apply rule (lem EM);
- | apply rule (⇒_e (B∧D⇒C) (B∧D));
+apply rule (⇒#i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
+apply rule (⇒#i [h2] ((D ⇒ A) ⇒ D ⇒ C));
+apply rule (⇒#i [h3] (D ⇒ C));
+apply rule (⇒#i [h4] (C));
+apply rule (∨#e (B∨¬B) [h5] (C) [h6] (C));
+ [ apply rule (lem 0 EM);
+ | apply rule (⇒#e (B∧D⇒C) (B∧D));
[ apply rule (discharge [h2]);
- | apply rule (∧_i (B) (D));
+ | apply rule (∧#i (B) (D));
[ apply rule (discharge [h5]);
| apply rule (discharge [h4]);
]
]
- | apply rule (⇒_e (A∧¬B⇒C) (A∧¬B));
+ | apply rule (⇒#e (A∧¬B⇒C) (A∧¬B));
[ apply rule (discharge [h1]);
- | apply rule (∧_i (A) (¬B));
- [ apply rule (⇒_e (D⇒A) (D));
+ | apply rule (∧#i (A) (¬B));
+ [ apply rule (⇒#e (D⇒A) (D));
[ apply rule (discharge [h3]);
| apply rule (discharge [h4]);
]
(*END*)
qed.
+(* Per dimostrare questo teorema torna comodo il lemma EM
+ dimostrato in precedenza. *)
theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
(*BEGIN*)
-apply rule (⇒_i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
-apply rule (⇒_i [h2] ((L⇒F) ⇒ L ⇒ E));
-apply rule (⇒_i [h3] (L ⇒ E));
-apply rule (⇒_i [h4] (E));
-apply rule (∨_e (G∨E) [h5] (E) [h6] (E));
- [ apply rule (⇒_e (F ⇒ G∨E) (F));
+apply rule (⇒#i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
+apply rule (⇒#i [h2] ((L⇒F) ⇒ L ⇒ E));
+apply rule (⇒#i [h3] (L ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (G∨E) [h5] (E) [h6] (E));
+ [ apply rule (⇒#e (F ⇒ G∨E) (F));
[ apply rule (discharge [h1]);
- | apply rule (⇒_e (L⇒F) (L));
+ | apply rule (⇒#e (L⇒F) (L));
[ apply rule (discharge [h3]);
| apply rule (discharge [h4]);
]
]
- |apply rule (∨_e (¬L∨E) [h7] (E) [h8] (E));
- [ apply rule (⇒_e (G⇒¬L∨E) (G));
+ |apply rule (∨#e (¬L∨E) [h7] (E) [h8] (E));
+ [ apply rule (⇒#e (G⇒¬L∨E) (G));
[ apply rule (discharge [h2]);
| apply rule (discharge [h5]);
]
- | apply rule (⊥_e (⊥));
- apply rule (¬_e (¬L) (L));
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬L) (L));
[ apply rule (discharge [h7]);
| apply rule (discharge [h4]);
]
theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
(*BEGIN*)
-apply rule (⇒_i [h1] (¬A∨¬B));
-apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
- [ apply rule (lem EM);
- | apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
- [ apply rule (lem EM);
- | apply rule (⊥_e (⊥));
- apply rule (¬_e (¬(A∧B)) (A∧B));
+apply rule (⇒#i [h1] (¬A∨¬B));
+apply rule (∨#e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
+ [ apply rule (lem 0 EM);
+ | apply rule (∨#e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
+ [ apply rule (lem 0 EM);
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬(A∧B)) (A∧B));
[ apply rule (discharge [h1]);
- | apply rule (∧_i (A) (B));
+ | apply rule (∧#i (A) (B));
[ apply rule (discharge [h2]);
| apply rule (discharge [h4]);
]
]
- | apply rule (∨_i_r (¬B));
+ | apply rule (∨#i_r (¬B));
apply rule (discharge [h5]);
]
- | apply rule (∨_i_l (¬A));
+ | apply rule (∨#i_l (¬A));
apply rule (discharge [h3]);
]
(*END*)
theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
(*BEGIN*)
-apply rule (⇒_i [h1] (¬A ∧ ¬B));
-apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
- [ apply rule (lem EM);
- | apply rule (⊥_e (⊥));
- apply rule (¬_e (¬(A∨B)) (A∨B));
+apply rule (⇒#i [h1] (¬A ∧ ¬B));
+apply rule (∨#e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
+ [ apply rule (lem 0 EM);
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬(A∨B)) (A∨B));
[ apply rule (discharge [h1]);
- | apply rule (∨_i_l (A));
+ | apply rule (∨#i_l (A));
apply rule (discharge [h2]);
]
- | apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
- [ apply rule (lem EM);
- | apply rule (⊥_e (⊥));
- apply rule (¬_e (¬(A∨B)) (A∨B));
+ | apply rule (∨#e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
+ [ apply rule (lem 0 EM);
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬(A∨B)) (A∨B));
[ apply rule (discharge [h1]);
- | apply rule (∨_i_r (B));
+ | apply rule (∨#i_r (B));
apply rule (discharge [h10]);
]
- | apply rule (∧_i (¬A) (¬B));
+ | apply rule (∧#i (¬A) (¬B));
[ apply rule (discharge [h3]);
|apply rule (discharge [h11]);
]
theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
(*BEGIN*)
-apply rule (⇒_i [h1] (¬(A∨B)));
-apply rule (¬_i [h2] (⊥));
-apply rule (∨_e (A∨B) [h3] (⊥) [h3] (⊥));
+apply rule (⇒#i [h1] (¬(A∨B)));
+apply rule (¬#i [h2] (⊥));
+apply rule (∨#e (A∨B) [h3] (⊥) [h3] (⊥));
[ apply rule (discharge [h2]);
- | apply rule (¬_e (¬A) (A));
- [ apply rule (∧_e_l (¬A∧¬B));
+ | apply rule (¬#e (¬A) (A));
+ [ apply rule (∧#e_l (¬A∧¬B));
apply rule (discharge [h1]);
| apply rule (discharge [h3]);
]
- | apply rule (¬_e (¬B) (B));
- [ apply rule (∧_e_r (¬A∧¬B));
+ | apply rule (¬#e (¬B) (B));
+ [ apply rule (∧#e_r (¬A∧¬B));
apply rule (discharge [h1]);
| apply rule (discharge [h3]);
]
theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
(*BEGIN*)
-apply rule (⇒_i [h1] (A));
+apply rule (⇒#i [h1] (A));
apply rule (RAA [h2] (⊥));
-apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
+apply rule (⇒#e ((A⇒⊥)⇒⊥) (A⇒⊥));
[ apply rule (discharge [h1]);
- | apply rule (⇒_i [h3] (⊥));
- apply rule (¬_e (¬A) (A));
+ | apply rule (⇒#i [h3] (⊥));
+ apply rule (¬#e (¬A) (A));
[ apply rule (discharge [h2]);
| apply rule (discharge [h3]);
]
]
(*END*)
-qed.
+qed.