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:

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

I termini, le formule e i nomi delle ipotesi

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

In questa palette troverete i template per tutte le regole di introduzione ed eliminazione dei connettivi viste a lezione TRANNE il template della regola di eliminazione dell'AND.

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:

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

Quando arrivate ad una foglia del vostro albero utilizzerete la regola Discharge (Si trova tra Misc Rules)

    apply rule (discharge [nome ipotesi]);

Template per la regola di eliminazione dell'∧

    apply rule (∧#e (A ∧ B) [h1] [h2] (C));
      [ dimostrazione di (A ∧ B)
      | dimostrazione di (C) utilizzando le ipotesi A (chiamata h1) e B (chiamata h2)
      ]

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

Suggerimenti

• Nelle regole con più premesse ricordatevi di indentare il codice. In questo modo sarà più facile trovare gli errori e correggerli.

• Nella regola di eliminazione del ¬ la premessa di sinistra è quella negata. Esempio:

  apply rule (¬#e (¬ F) (F));
  [ dimostrazione di ¬ F
  | dimostrazione di F
  ]
  

Nota di compatibilità

In Matita 0.5.6 (versione installata nei laboratori), le regole della deduzione naturale utilizzano la sintassi ∨_i_l (con due caratteri _). In versioni più recenti di Matita (come la 0.5.8), la stessa regola viene espressa con la sintassi ∨#i_l (il primo underscore _ è sostituito da un cancelletto #).