I connettivi logici

Per digitare i connettivi logici:

• ∧ : \land
• ∨ : \lor
• ¬ : \lnot
• ⇒ : =>, \Rightarrow
• ⊥ : \bot
• ⊤ : \top

Per digitare i quantificatori:

• ∀ : \forall
• ∃ : \exists

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 scritte tra ( e ).

• I nomi delle ipotesi, quando argomenti di una regola, vengono scritti tra [ e ].

Le regole di deduzione naturale

Per digitare le regole di deduzione naturale è possibile utilizzare la palette che compare sulla sinistra dopo aver premuto F2.

L'albero si descrive partendo dalla radice. Le regole con premesse multiple sono seguite da [, | e ]. Ad esempio:

    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. 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 regole che hanno una sola premessa non vengono seguite da parentesi quadre.

L'albero di deduzione

Per visualizzare l'albero man mano che viene costruito dai comandi impartiti al sistema, premere F3 e poi premere sul bottome home (in genere contraddistinto da una icona rappresentate una casa).

Si suggerisce di marcare tale finestra come always on top utilizzando il menu a tendina che nella maggior parte degli ambienti grafici si apre cliccando nel suo angolo in 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. 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 ...