c
: intr
elim
∧
: ok
ok
∨
: check
ok
¬
: ok
check
⇒
: ok
bloccata + check
⊥
: ok
⊤
:
ok
Con il comando F2 aprire la palette con le shortcut per le regole di deduzione naturale
Con il comando F3 aprire un nuovo CIC browser e cliccare sul simbolo Home (una casa). In questa finestra verrà disegnato l'albero man mano che lo costruite.
Cominciate a ricopiare l'albero di deduzione naturale che avete scritto su carta. La copiatura procede dal basso verso l'alto.
Per digitare i connettivi logici:
∧
: \land
∨
: \lor
¬
: \lnot
⇒
: =>
, \Rightarrow
(!! Attenzione non usare →)⊥
: \bot
⊤
: \top
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
apply rule (lem 0 EM)
, mentre per usare il lemma NNAA (¬¬A⇒A
) bisogna digitare
apply rule (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 ...