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

Per digitare i connettivi logici:

I termini, le formule e i nomi delle ipotesi

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:

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 ...