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".
projects / helm.git / commitdiff