From 5755ebe4016316a474ad8ab8d33b1a1a9187cc9e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 1 Dec 2008 09:29:23 +0000 Subject: [PATCH] better doc --- .../didactic/exercises/natural_deduction.ma | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma index 1bc9717fd..3a5bca154 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma @@ -100,6 +100,39 @@ alto a sinistra. 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 (es. `∀A:CProp.`) +e iniziare la dimostrazione 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)` ... + DOCEND*) include "didactic/support/natural_deduction.ma". -- 2.39.2