Note di Logica Matematica n.4

Claudia Malvenuto e Roberto Maieli^{∗} canale E-O - a.a. 2002-2003

16 dicembre 2002

Indice

1 Logica dei predicati 1

2 Tableaux semantici 1 2.1 Esercizi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Calcolo dei sequenti di Gentzen 9 3.1 Esercizi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

1 Logica dei predicati

2 Tableaux semantici

Prima di dare la definizione formale dei tableaux predicativi, cerchiamo di affrontare intuitivamente la questione di costruire i tableaux, facendo emergere di volta in volta i problemi con i quali deve fare i conti la nostra intuizione. Ricordiamo che il tableau per una formula (o insieme di formule) è una ricerca sistematica di un controesempio. Il metodo dei tableaux consente :

• da un lato, di ridurre la questione della validità di una formula A a quella della soddisfacibilità della sua negazione ¬A (ricordiamo che “⊧ A se e solo se ¬A è insoddisfacibile”),

• dall’altro, di ridurre il problema della soddisfacibilità di una formula a quello più semplice della soddisfacibilità di un insieme di letterali.

Una formula A è soddisfacibile se esiste una interpretazione (modello) che la rende vera. Relativamente al frammento proposizionale della logica classica, il metodo dei tableaux è una procedura efficiente che consente di decidere se un enunciato è o no soddisfacibile. Poniamoci adesso la stessa questione per l’intero frammento del calcolo dei predicati. Cerchiamo di estendere il metodo della ricerca di modello di una formula dal caso proposizionale a quello predicativo. Procediamo per problemi. Vogliamo, ad esempio, stabilire se la formula ∀xP (x) → ∀xQ(x) è conseguenza logica del predicato ∀x(P (x) → Q(x)): questo equivale a provare che la formula predicativa

F = ∀x(P (x) → Q(x)) → ∀xP (x) → ∀xQ(x)

è valida, ovvero che ¬F è insoddisfacibile. Costruiamo il tableau associato a ¬F e verifichiamo che ogni sua foglia è chiusa. Etichettiamo la radice del tableau con la formula negata e procediamo come nel caso proposizionale fino ad ottenere un insieme di formule quantificate {∀x(P (x) → Q(x)), ∀xP (x), ¬∀xQ(x)}. A questo punto dobbiamo istanziare una di queste formule. Ma qual è il dominio su cui dobbiamo fare l’instanziazione ? Non andiamo lontano: prendiamo il dominio A delle costanti del linguaggio della logica dei predicati; è sufficientemente generico per il nostro scopo. Quindi istanziamo la formula ¬∀xQ(x) con una costante generica a in A (insieme non finito delle costanti del linguaggio). Otteniamo ¬Q(a) (teniamo presente il fatto che ¬∀xQ(x) ≡ ∃x¬Q(x)). Successivamente osserviamo che se ∀xP (x) è soddisfacibile allora lo deve essere in particolare anche l’istanza P (a). Analogo ragionamento per la formula ∀x(P (x) → Q(x)): se tale formula è soddisfacibile allora lo deve essere ogni sua istanza e quindi in particolare l’istanza P (a) → Q(a). Possiamo così eliminare, in un sol colpo, i due quantificatori universali e costruire un nuovo nodo dell’albero etichettato con {P (a) → Q(a), P (a), ¬Q(a)}. Infine applichiamo la (β)regola di eliminazione dell’implicazione → e otteniamo le due foglie etichettate da insiemi di letterali contraddittori. L’albero chiude quindi F è valida.

∗Dipartimento di Informatica, Università di Roma “La Sapienza”, Via Salaria, 113. E-mail: claudia, maieli@dsi.uniroma1.it.

\{¬F\} ; \{∀x(P (x) → Q(x)), ¬(∀xP (x) → ∀xQ(x))\} ; \{∀x(P (x) → Q(x)), ∀xP (x), ¬∀xQ(x)\} ; \{∀x(P (x) → Q(x)), ∀xP (x), ¬∀Q(x)\} ; \{∀x(P (x) → Q(x)), ∀xP (x), ¬Q(a)\} ¬∀ : a_{\{P (a) → Q(a), P (a), ¬Q(a)\} ∀ : a \begin{matrix}\{¬P (a), P (a), ¬Q(a)\} \\ × \end{matrix} ; \begin{matrix}\{Q(a), P (a), ¬Q(a)\} \\ × \end{matrix}}

Ci poniamo ora la questione se è vero che {∀x(P (x)∨Q(x))} ⊧ ∀xP (x)∨∀xQ(x). La risposta, senza aspettarla dai tableaux, è “no”: infatti la formula F = ∀x(P (x) ∨ Q(x)) → ∀xP (x) ∨ ∀xQ(x) è sia soddisfacibile che falsificabile, dunque non valida. Con l’interpretazione

I =< ℕ, {P (x) : x è pari , Q(x) : x è dispari}, ∅ >,

si vede subito che I ⊧ ∀x(P (x) ∨ Q(x)) (ogni naturale è pari oppure dispari) mentre I |̸= ∀xP (x) (non è vero che tutti i naturali sono pari) e I |̸= ∀xQ(x) (non è vero che tutti i naturali sono dispari): si deduce che la formula F è falsa nell’interpretazione I. Si noti che, in particolare, la formula F è vera nei modelli con un solo elemento nel dominio. Proviamo a costruire il tableau per ¬F ≡ [∀x(P (x) ∨ Q(x))] ∧ ¬(∀xP (x) ∨ ∀xQ(x)).

\{∀x(P (x) ∨ Q(x), ¬(∀xP (x) ∨ ∀xQ(x))\} ; \{∀x(P (x) ∨ Q(x), ¬∀xP (x) ∧ ¬∀xQ(x))\} ; \{∀x(P (x) ∨ Q(x)), ¬∀xP (x), ¬∀xQ(x)\} ; \{∀x(P (x) ∨ Q(x)), ¬∀xP (x), ¬Q(a)\} ¬∀ : a_{\{∀x(P (x) ∨ Q(x)), ¬P (a), ¬Q(a)\} ¬∀ : a_{\{P (a) ∨ Q(a), ¬P (a), ¬Q(a)\} ∀ : a \begin{matrix}\{P (a), ¬P (a), ¬Q(a)\} \\ × \end{matrix} ; \begin{matrix}\{Q(a), ¬P (b), ¬Q(a)\} \\ × \end{matrix}}}

Osserviamo che il tableau chiude, quindi ¬F insoddisfacibile, o equivalentemente, F è valida, contraddicendo il fatto visto sopra che F è falsificabile. Dove abbiamo sbagliato? Abbiamo istanziato la ¬∀P (x) (equivalente alla ∃x¬P (x)) con una costante a sulla quale avevamo già fatto un’ipotesi, istanziandola nella formula ¬∀xQ(x). Dobbiamo quindi usare una costante nuova ogni volta che si istanzia una formula di tipo esistenziale ∃xR(x) (o, equivalentemente, la negazione di un universale ¬∀xR(x)). Di seguito è riportato il tableau con l’istanziazione corretta.

\{∀x(P (x) ∨ Q(x), ¬(∀xP (x) ∨ ∀xQ(x))\} ; \{∀x(P (x) ∨ Q(x)), ¬∀xP (x), ¬∀xQ(x)\} ; \{∀x(P (x) ∨ Q(x)), ¬∀xP (x), ¬∀xQ(x)\} ; \{∀x(P (x) ∨ Q(x)), ¬∀P (x), ¬Q(a)\} ¬∀ : a_{\{∀x(P (x) ∨ Q(x)), ¬P (b), ¬Q(a)\} ¬∀ : b_{\{P (a) ∨ Q(a), ¬P (b), ¬Q(a)\} ∀ : a \begin{matrix}\{P (a), ¬P (b), ¬Q(a)\} \\ ◯ \end{matrix} ; \begin{matrix}\{Q(a), ¬P (b), ¬Q(a)\} \\ × \end{matrix}}}

Osserviamo adesso che il tableau ha un ramo aperto etichettato con un insieme di letterali {P (a), ¬P (b), ¬Q(a)}, che non costituisce ancora un modello per F. Infatti {P (a), ¬P (b), ¬Q(a)} |̸= ∀x(P (x) ∨ Q(x)) ∧ ¬(∀xP (x) ∨ ∀xQ(x)). Dobbiamo estendere il ramo aperto con un’altra istanza, P (b) ∨ Q(b), della formula quantificata universalmente ∀x(P (x) ∨ Q(x)); ed infine applicare una regola di eliminazione della disgiunzione ∨ ed ottenere così l’unica foglia aperta etichettata con l’insieme {Q(b), ¬P (b), ¬Q(a), P (a)} (si osservi che la radice dell’albero è adesso conseguenza logica di tale insieme). Chiaramente, essendoci una foglia aperta, si ha |̸= F.

\{P (b) ∨ Q(b), ¬P (b), ¬Q(a), P (a)\} ; \begin{matrix}\{P (b), ¬P (b), ¬Q(a), P (a)\} \\ × \end{matrix} ; \begin{matrix}\{Q(b), ¬P (b), ¬Q(a), P (a)\} \\ ◯ \end{matrix}

Quest’ultimo esempio mette in evidenza due fatti:

1. quando eliminiamo un quantificatore esistenziale (o la negazione di un quantificatore universale), il nodo figlio che contiene l’istanza del quantificatore eliminato deve usare una costante nuova (o fresca), una costante cioè sulla quale non abbiamo ancora fatto assunzioni. La variabile, in altre parole, non deve comparire nel ramo che va dal nodo in cui appare l’istanza fino alla radice del tableau;

2. ogni volta che istanziamo un quantificatore universale o la negazione di un quantificatore esistenziale, allora nel nodo figlio la costante utilizzata per l’istanziazione può essere una qualsiasi delle costanti che appaiono in qualche formula presente nel nodo che precede (padre) l’istanziazione. Inoltre assumiamo, per completezza, un principio di sistematicità, secondo il quale il quantificatore deve essere istanziato con ogni costante che appare in almeno in una formula presente nel cammino che va dal nodo dell’applicazione della regola fino alla radice del tableau.

Riportiamo di seguito le regole dei tableaux. Le regole relative ai connettivi rimangono invariate come nel caso proposizionale. Aggiungiamo solo le regole relative alle eliminazione dei quantificatori:

• (γ)-Regole di tipo universale - si tratta di regole unarie che consentono di estendere il nodo l con il nodo l′, etichettati come sotto. U′ è un isieme di formule; la costante a è appare eventualmente in qualcuna delle formule che etichettatano qualche nodo del ramo che va da l alla radice del tableau :

l : U′, ∀A(x) ; \begin{matrix}l′ : U′, ∀A(x), A(a) \\ ∀ : a \end{matrix}  l : U′, ¬∃xA(x) ; \begin{matrix}l′ : U′, ¬∃xA(x), ¬A(a) \\ ¬∃ : a \end{matrix}

• (δ)-Regole di tipo esistenziale - si tratta di regole unarie che consentono di estendere il nodo l con il nodo l′, etichettati come sotto. U′ è un isieme di formule; la costante a è nuova (fresca), non appare cioè in nessuna formula che etichetta un qualsiasi nodo del ramo che va da l alla radice del tableau:

l : U′, ∃A(x) ; \begin{matrix}l′ : U′, A(a) \\ ∃ : a \end{matrix}  l : U′, ¬∀xA(x) ; \begin{matrix}l′ : U′, ¬A(a) \\ ¬∀ : a \end{matrix}

Teorema 1 Il metodo dei tableaux è corretto e completo, i.e., data una formula A,

⊧ A se e solo se il tableau di ¬A chiude

2.1 Esercizi

Verificare le tautologie seguenti usando il metodo dei tableaux.

1. ⊧ F = ∀xA(x) → A(a). Costruiamo il tableau di ¬F:

\{∀A(x), ¬A(a)\} ; \begin{matrix}\{∀A(x), A(a), ¬A(a)\} \\ × \end{matrix} ; ∀ : a

2. ⊧ F = ∀xA(x) ↔ ¬∃x¬A(x). Costruiamo il tableau di ¬F :

\begin{matrix}\{¬((∀xA(x) → ¬∃x¬A(x)) ∧ (¬∃x¬A(x) → ∀xA(x)))\} \\ \{¬(∀xA(x) → ¬∃x¬A(x))\} ; \{(∀xA(x), ¬(¬∃x¬A(x))\} ; \{∀xA(x), ∃x¬A(x)\} ; \{∀xA(x), ¬A(a)\} ; \begin{matrix}\{∀xA(x), A(a), ¬A(a)\} \\ × \end{matrix} & \{¬(¬∃x¬A(x) → ∀xA(x))\} ; \{¬∃x¬A(x), ¬∀xA(x)\} ; \{¬∃x¬A(x), ¬A(a)\} ; \{¬∃x¬A(x), ¬¬A(a), ¬A(a)\} ; \begin{matrix}\{¬∃x¬A(x), A(a), ¬A(a)\} \\ × \end{matrix} \end{matrix}

Tutti i suoi rami sono chiusi, quindi la formula F è valida.

3. ⊧ ∀xA(x) → ∃xA(x). Costruiamo il tableau per ¬(∀xA(x) → ∃xA(x)).

\{∀xA(x), ¬∃xA(x)\} ; \{∀xA(x), A(a), ¬∃xA(x)\} ; \begin{matrix}\{∀xA(x), A(a), ¬∃xA(x), ¬A(a)\} \\ × \end{matrix}

Poiché tutte le foglie sono chiuse, ne segue che ¬(∀xA(x) → ∃xA(x)) è insoddisfacibile, i.e. ∀xA(x) → ∃xA(x) è valida.

4. Ponimamoci la questione : ⊧ P (a) ∨ ¬∃xP (x) ? Costruiamo il tableau della negazione di tale formula e vediamo se tutti i rami chiudono.

\{¬(P (a) ∨ ¬∃xP (x))\} ; \{¬P (a), ¬¬∃xP (x)\} ; \{¬P (a), ∃xP (x)\} ; \begin{matrix}\{¬P (a), P (b)\} \\ ◯ \end{matrix}

Il tableau non chiude quindi l’etichetta della radice è soddisfacibile. Cerchiamo, dunque, di costruire un modello I per ¬(P (a)∨¬∃xP (x)) a partire dall’etichetta del nodo aperto ¬P (a), P (b). Poniamo la questione:

I =< {a, b}, {P } >⊧ ¬(P (a) ∨ ¬∃xP (x))?

La risposta è positiva, infatti, v(¬(P (a) ∨ ¬∃xP (x))) = V se e solo se v(¬P (a) ∧ ∃xP (x)) = V se e solo se v(¬P (a)) = V e v(∃xP (x)) = V, allora v(P (b)) = V.

5. Dimostrare che ⊧ (∀P (x) ∨ ∀Q(x)) → ∀(P (x) ∨ Q(x)).

Mostriamo equivalentemente che il tableau per la formula negata ¬(∀P (x) ∨ ∀Q(x)) → ∀(P (x) ∨ Q(x)) è chiuso:

\{∀P (x) ∨ ∀Q(x), ¬∀(P (x) ∨ Q(x)\} ; \{∀P (x) ∨ ∀Q(x), ¬(P (a) ∨ Q(a))\} ; \begin{matrix}\{∀P (x) ∨ ∀Q(x), ¬P (a), ¬Q(a)\} \\ \{∀P (x), ¬P (a), ¬Q(a)\} ; \begin{matrix}\{∀P (x), P (a), ¬P (a), ¬Q(a)\} \\ × \end{matrix} & \{∀Q(x), ¬P (a), ¬Q(a)\} ; \begin{matrix}\{∀Q(x), Q(a)¬P (a), ¬Q(a)\} \\ × \end{matrix} \end{matrix}

6. Verificare la validità della formula

F = ∀x(P (x) → Q(a)) ↔ (∃xP (x) → Q(a)).

Costruiamo il tableau di ¬F per mostrare che ¬F è insoddisfacibile:

\begin{matrix}\{¬[∀x(P (x) → Q(a)) ↔ (∃xP (x) → Q(a))]\} \\ \{¬[∀x(P (x) → Q(a)) → (∃xP (x) → Q(a))]\} ; \{∀x(P (x) → Q(a)), ¬(∃xP (x) → Q(a))\} ; \{∀x(P (x) → Q(a)), ∃xP (x), ¬Q(a)\} ; \{∀x(P (x) → Q(a)), P (b), ¬Q(a)\} ; \{P (b) → Q(a), P (b), ¬Q(a)\} ; \begin{matrix}\{¬P (b), P (b), ¬Q(a)\} \\ × \end{matrix} ; \begin{matrix}\{Q(a), P (b), ¬Q(a)\} \\ × \end{matrix} & \{¬[(∃xP (x) → Q(a)) → ∀x(P (x) → Q(a))]\} ; \{∃xP (x) → Q(a), ¬∀x(P (x) → Q(a))\} ; \{∃xP (x) → Q(a), ¬(P (b) → Q(a))\} ; \begin{matrix}\{∃xP (x) → Q(a), P (b), ¬Q(a))\} \\ \{¬∃xP (x), P (b), ¬Q(a)\} ; \begin{matrix}\{¬P (b), P (b), ¬Q(a)\} \\ × \end{matrix} & \begin{matrix}\{Q(a), P (b), ¬Q(a)\} \\ × \end{matrix} \end{matrix} \end{matrix}

7. Dire se la seguente inferenza

{∀x(Q(x) → ¬P (x)), ∀x(R(x) → Q(x)) \atop ∀x(R(x) → ¬P (x))}

è corretta.

Costruiamo il tableau per

¬[∀x(Q(x) → ¬P (x)) ∧ ∀x(R(x) → Q(x)) → (∀x(R(x) → ¬P (x)))]

\{∀x(Q(x) → ¬P (x)), ∀x(R(x) → Q(x)), ¬∀x(R(x) → ¬P (x))\} ; \{∀x(Q(x) → ¬P (x)), ∀x(R(x) → Q(x)), ¬(R(a) → ¬P (a))\} ; \{∀x(Q(x) → ¬P (x)), ∀x(R(x) → Q(x)), R(a), ¬¬P (a)\} ; \begin{matrix}\{∀x(Q(x) → ¬P (x)), ∀x(R(x) → Q(x)), Q(a) → ¬P (a), R(a), P (a)\} \\ \begin{matrix}\{∀x(Q(x) → ¬P (x)), ∀x(R(x) → Q(x)), \\ ¬Q(a), R(a), P (a)\} \end{matrix} ; \{R(a) → Q(a), ¬Q(a), R(a), P (a)\} ; \begin{matrix}\{¬R(a), ¬Q(a), R(a), P (a)\} \\ × \end{matrix} ; \begin{matrix}\{¬Q(a), ¬Q(a), R(a), P (a)\} \\ × \end{matrix} & \begin{matrix}\{∀x(Q(x) → ¬P (x)), ∀x(R(x) → Q(x)), \\ ¬P (a), R(a), P (a)\} \\ × \end{matrix} \end{matrix}

3 Calcolo dei sequenti di Gentzen

Diamo le regole di introduzione dei quantificatori per il calcolo dei sequenti di Gentzen. Assumiamo che Γ sia un (multi-)insieme di formule:

• regole di introduzione per ∃ e ¬A: Γ è un (multi-)insieme di formule

⊢ Γ, ∃xA(x), A(a) ; ∃ ; ⊢ Γ, ∃xA(x)  ⊢ Γ, ¬∀xA(x), ¬A(a) ; ¬A ; ⊢ Γ, ¬∀xA(x)

• regole di introduzione per ∀ e ¬E:

\begin{aligned}⊢ Γ, A(a) \\ & ∀^{∗} \\ ⊢ Γ, ∀xA(x) \end{aligned}  \begin{aligned}⊢ Γ, ¬A(a) \\ & ¬E^{∗} \\ ⊢ Γ, ¬∃xA(x) \end{aligned}

(*) Restrizione sulla variabile propria: la costante a deve essere “fresca”, non deve comparire libera in alcuna formula della conclusione della regola ⊢ Γ, ∀xA(x) (rispettivamente, ⊢ Γ, ¬ExA(x)). Viceversa, la costante a può occorre libera in qualche formula, oltre ad A(a) (risp. ¬A(a)) che appartiene al sottoalbero radicato nella premessa della regola.

Una dimostrazione di un sequente ⊢ Γ è un albero la cui radice è etichettata con il sequente Γ, le foglie sono etichettate con assiomi, regole 0-arie del tipo

assioma

⊢ Γ, P (a), ¬P (a)

ed ogni nodo è etichettato con la conclusione di una regola, la cui premessa (premesse) etichetta (etichettano) il nodo (i nodi) genitore (genitori).

Teorema 2 Il cacolo dei sequenti di Gentzen è corretto e completo, i.e. data una formula A,

⊧ A se e solo se esiste una dimostrazione nel calcolo dei sequenti di ⊢ A.

3.1 Esercizi

Esercizio 1 Dimostrare il sequente ⊢ ∃x∀yP (x, y) → ∀y∃xP (x, y):

\begin{matrix}⊢ ¬∀yP (a, y), ¬P (a, b), ¬P (a, a), ∃xP (x, b), P (a, b) \\ ⊢ ¬∀yP (a, y), ¬P (a, a), ∃xP (x, b), P (a, b) \end{matrix} ; ⊢ ¬∀yP (a, y), ∃xP (x, b), P (a, b) ; ⊢ ¬∀yP (a, y), ∃xP (x, b) ; ⊢ ¬∀yP (a, y), ∀y∃xP (x, y) ; ⊢ ¬∃x∀yP (x, y), ∀y∃xP (x, y) ; ⊢ ∃x∀yP (x, y) → ∀y∃xP (x, y)

Una dimostrazione alternativa dello stesso sequente è data di seguito:

\begin{matrix}⊢ ¬∀yP (b, y), ¬P (b, a), ∃xP (x, a), P (b, a) \\ ⊢ ¬∀yP (b, y), ∃xP (x, a), P (b, a) \end{matrix} ; ⊢ ¬∀yP (b, y), ∃xP (x, a) ; ⊢ ¬∃x∀yP (x, y), ∃xP (x, a) ; ⊢ ¬∃x∀yP (x, y), ∀y∃xP (x, y) ; ⊢ ∃x∀yP (x, y) → ∀y∃xP (x, y)

Esercizio 2 Dimostrare il sequente ⊢ ∀xP (x) ∨ ∀xQ(x) → ∀x(P (x) ∨ Q(x)):

\begin{matrix}{⊢ ¬∀xP (x), ¬P (a), P (a), Q(a) \atop ⊢ ¬∀xP (x), P (a), Q(a)} ; ⊢ ¬∀xP (x), P (a) ∨ Q(a) ; ⊢ ¬∀xP (x), ∀x(P (x) ∨ Q(x)) & {⊢ ¬∀xQ(x), ¬Q(a), P (a), Q(a) \atop ⊢ ¬∀xQ(x), P (a), Q(a)} ; ⊢ ¬∀xQ(x), P (a) ∨ Q(a) ; ⊢ ¬∀xQ(x), ∀x(P (x) ∨ Q(x)) \\ ⊢ ¬(∀xP (x) ∨ ∀xQ(x)), ∀x(P (x) ∨ Q(x)) \end{matrix} ; ⊢ ∀xP (x) ∨ ∀xQ(x) → ∀x(P (x) ∨ Q(x))