Gli esercizi

  1. (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
  2. (F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E.
  3. (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E.
  4. (F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E.
  5. (F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E.
  6. ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.

La tabella vista a lezione

Le istruzioni per Matita

  1. Con il comando F2 aprire la palette con le shortcut per le regole di deduzione naturale

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

  3. Cominciate a ricopiare l'albero di deduzione naturale che avete scritto su carta. La copiatura procede dal basso verso l'alto.

I connettivi logici

Per digitare i connettivi logici:

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