LOGICA MATEMATICA

Claudia Malvenuto e Roberto Maieli^{∗} Canale E-O - a.a 2003/04 Scheda di esercizi n. 13

17 novembre 2003

Tableaux Semantici & Calcolo dei Sequenti di Gentzen

Esercizio 1 Verificare le seguenti tautologie (enunciati validi), usando il metodo dei tableaux o il calcolo dei sequenti di Gentzen:

((A → B) → B) ∨ ¬A), ((A → B) → B) → ¬A), (A → B ∧ ¬B) → ¬A), (A ↔ A ∧ ¬A) ↔ ¬A, ((A → B) → ¬(B → A)) ↔ ¬(A ↔ B), (A ↔ B) ∨ (A ↔ ¬B), ¬A → (A ∨ B → B), A ↔ ((A ∨ B) ∧ (A ∨ ¬B)), (A ∨ B → C) ↔ ((A → C) ∨ (B → C)), (A ∨ (B ∨ C)) → (A → (B → C)), ((A → B) → C) → ((C → A) → (D → A)), (A → C) ∧ (B → D) → (¬C ∨ ¬D → ¬A ∨ ¬B), (A → (A → B)) → (A → B), ((A → B) → (B → A)) → (B → A), ((A → B) → A) → ((A → B) → B), (((A → B) → B) → B) → (A → B), ((A → B) → (A → C)) → (A → (B → C)), (A → B) → ((A → (B → C)) → (A → C), (A → C) → (A → (B → C)), (A → B) ∧ (B → C) ∧ (C → A) → (A ↔ C), ((A → B) → C) → (((B → A) → C) → C).

∗Dipartimento di Informatica, Università di Roma “La Sapienza”, Via Salaria, 113.

E-mail: claudia, maieli@dsi.uniroma1.it.

Esercizio 2 Verificare le seguenti conseguenze logiche, usando il metodo dei Tableaux o il sistema dei sequenti di Gentzen:

A → B, B → C, ¬C ⊧ ¬A, A ∨ ¬C, A → B, C ⊧ B, A → ¬B, ¬B → ¬C ⊧ A → ¬C, A → (B → ¬A), A ↔ B ⊧ ¬B ∨ ¬A, B ∨ C, A → B, B → A ⊧ A ∨ C, A → B, B → C, C → D, ¬D, A ∨ E ⊧ E, (A ∨ B) ∧ (C ∨ D), (A → C) ∧ (B → D), ¬C ⊧ D, ¬A ∧ ¬B, A ∨ B ⊧ C, A → B ∨ C, ¬B → C ∧ ¬D ⊧ C → C.

Esercizio 3 Stabilire, usando i tableaux o il sistema di Gentzen, se la formula di sinistra è o no conseguenza logica della/e formule di destra:

\begin{matrix}A & (A → B) → A \\ (A → B) → A & A \\ (A → B) → B & A \\ A ∨ B & A → B, B ∨ C \\ A → (¬C ↔ B) & A ∨ B, A → ¬C \\ A → (B → D) & A ∧ B → C, ¬D → ¬(E → F), C → (E → F) \\ ¬E ∨ A → (E → D) & A → B, C → ¬B, (D → ¬A) → C \\ B → E & A ∨ (B → C), D → (C → E), A → ¬D, D \\ A ∨ B & ¬A ∧ ¬B → C, D ∧ ¬C \\ D ∧ C & ¬A ∧ ¬B, (C → A) ↔ ¬B, D \\ ¬A & B ∨ C → A, ¬B, A ∧ ¬C \\ A ∨ B & A ∨ ¬(B ∧ C), ¬B, ¬(A ∨ C) \\ A & A ∨ ¬(B ∨ C), ¬B, ¬(A ∨ ¬C). \end{matrix}