Dimostrazioni completezza e correttezza & notazione polacca

Correttezza e Completezza del metodo di tableaux per la logica proposizionale

Se consideriamo l’insieme infinito delle formule della logica proposizionale , possiamo notare che in questo insieme esistono un insieme di formule che sono tautologie e un insieme di formule che sono dimostrabili con il metodo di tableaux , vogliamo dimostrare che i due insiemi ( sono in verità sotto-insiemi dell’insieme infinito delle formule della logica proposizionale ) sono lo stesso insieme , ovvero che tutte le formule che sono tautologie sono dimostrabili con il metodo di tableaux e viceversa , le formule dimostrabili con il metodo di tableaux sono formule tautologie. Consideriamo ora $T=\text{tautologie}$ e $D=\text{formule dimostrabili con il metodo di tableaux}$ , ci chiediamo allora come possiamo dimostrare $T=D$ ? Beh possiamo farlo con la doppia inclusione , ovvero :

$$\{\begin{array}{l}T\subseteq D\\ D\subseteq T\end{array}⟹T=D$$

Osserviamo inoltre che :

1. se dimostriamo $D\subseteq T$ allora stiamo dimostrando la correttezza del metodo di tableaux
2. se dimostriamo che $T\subseteq D$ allora stiamo dimostrando la completezza del metodo di tableaux

Correttezza

Possiamo osservare che : se abbiamo una alfa formula $\alpha$ , noi quello che facciamo e “dedurre” ${\alpha }_1$ e ${\alpha }_2$ :

$$\begin{array}{c}\alpha \\ {\alpha }_1\\ {\alpha }_2\end{array}$$

mentre se abbiamo una beta formula $\beta$ , noi quello che facciamo è “supporre” o ${\beta }_1$ o ${\beta }_2$ :

$$\begin{array}{c}\beta \\ \swarrow \searrow \\ {\beta }_1{\beta }_2\end{array}$$

quindi notiamo che :

1. Una interpretazione $I$ rende soddisfacibile [ rende vera la formula ] una $\alpha$ formula , se e solo se , rende soddisfacibile anche ${\alpha }_1$ e ${\alpha }_2$
2. Una interpretazione $I$ rende soddisfacibile una $\beta$ formula , se e solo se , rende soddisfacibile una delle due tra ${\beta }_1$ e ${\beta }_2$

Quindi l’idea della dimostrazione è che se facciamo il tableaux di $\neg \mathcal{F}$ applicando $\alpha$ e $\beta$ formule, arriviamo alla fine , e otteniamo l’impossibilità di soddisfare sia una che l’altra , allora neanche la formula originale , ovvero $\neg \mathcal{F}$ è soddisfacibile. Ci serve però dire sta roba in modo più preciso :

Definizione

Diciamo che una formula $\mathcal{F}$ è soddisfacibile se esiste una interpretazione $I$ che la rende vera.

Notiamo da questa definizione che $\mathcal{F}$ è soddisfacibile se e solo se non è una contraddizione [ è falsa sempre ]. Quindi possiamo dire che :

Definizione

Un insieme $S$ di formule è soddisfacibile se esiste una interpretazione $I$ che rende vere TUTTE le formule in $S$.

Teorema

Se $\mathcal{F}$ è dimostrabile con il metodo di tableaux , allora $\mathcal{F}$ è una tautologia

Dimostrazione :

Se $\mathcal{F}$ non fosse una tautologia allora $\neg \mathcal{F}$ sarebbe soddisfacibile , ma per l’osservazione di prima sulle $\alpha$ e $\beta$ formule , se facciamo il tableaux di $\neg \mathcal{F}$ , avremo sempre un ramo di formule soddisfacibili , più precisamente avremo un ramo $\theta$ , tale che l’insieme $S_{\theta }$ di tutte le formule su quel ramo $\theta$ , questo insieme $S_{\theta }$ è soddisfacibile . Ma se ad un certo punto si chiudono tutti i rami , allora per ogni ramo $\theta$ [ chiuso ] l’insieme $S_{\theta }$ delle formule su quel ramo $\theta$ , non è soddisfacibile. Ma quindi otteniamo che se il tableaux di $\neg \mathcal{F}$ si chiude allora per nessuna interpretazione $\neg \mathcal{F}$ è soddisfacibile , allora $\mathcal{F}$ è una tautologia.

Completezza

Vogliamo ora dimostrare che se $\mathcal{F}$ è una tautologia allora $\mathcal{F}$ è dimostrabile con il metodo di tableaux [si chiude].

Abbiamo bisogno prima di un ingrediente : insiemi di Hintikka

Definizione

Un insieme di formule $S$ è un insieme di Hintikka [ per logica proposizionale ] se succedono 3 cose [ che sono poi le proprietà dei rami che rimangono aperti ] :

• $H_0$ : in $S$ non c’è mai una variabile $p$ e la sua negata $\neg p$ [ solo una delle due ]
• $H_1$ : se in $S$ c’è una formula di tipo $\alpha$ allora necessariamente ci devono essere le sue due componenti ${\alpha }_1$ e ${\alpha }_2$
• $H_2$ : se in $S$ c’è una formula di tipo $\beta$ allora necessariamente c’è una delle due componenti ${\beta }_1$ e ${\beta }_2$

Possiamo osservare che : se un tableaux [ completo ] ha un ramo aperto , allora l’insieme delle formule su quel ramo è un insieme di Hintikka.

Lemma

Se $S$ è un insieme di Hintikka allora $S$ è soddisfacibile

Dimostrazione Lemma di Hintikka : Per induzione sulla lunghezza [numero di simboli nella formula] delle formule dell’insieme $S$ : Passo Base : Consideriamo solo formule che contengono 1 o 2 simboli , quindi o sono variabili del tipo $p$ oppure $\neg p$ , questo è ok per la proprietà $H_0$. Quindi ora fissiamo $n\ge 2$ e consideriamo che $P(n)$ è vera , ovvero che se prendo un insieme di $S$ di formule di lunghezza $n$ esisterà un’interpretazione che rende $S$ soddisfacibile [ la mia ipotesi induttiva ]. Passo Induttivo : Ora consideriamo $P(n+1)$ ovvero le formule di lunghezza $n+1$ , osserviamo che una formula di lunghezza $n+1$ potrà essere una $\alpha$ formula o una $\beta$ formula : - caso 1. : se $\alpha$ formula ⇒ per la proprietà $H_1$ , in $S$ ci saranno sia ${\alpha }_1$ che ${\alpha }_2$ , ma queste due avranno necessariamente lunghezza $\le n$ , ma per ipotesi induttiva esiste una interpretazione $I$ che soddisfa sia ${\alpha }_1$ che ${\alpha }_2$ ⇒ $I$ soddisfa anche $\alpha$ . - caso 2. : se $\beta$ formula ⇒ per la proprietà $H_2$ , in $S$ ci saranno una delle due tra ${\beta }_1$ e ${\beta }_2$ , ma queste due avranno necessariamente lunghezza $\le n$ , ma per ipotesi induttiva esiste una interpretazione $I$ che soddisfa almeno una delle due ⇒ $I$ soddisfa anche $\beta$ .

$\square$

Teorema

Se $\mathcal{F}$ è una tautologia allora $\mathcal{F}$ è dimostrabile con il metodo di tableaux [si chiude].

Dimostrazione : Sia $\mathcal{F}$ una tautologia , se $\mathcal{F}$ non fosse dimostrabile col metodo di tableaux , allora partendo da $\neg \mathcal{F}$ e sviluppando tutto il tableaux otteniamo sempre almeno un ramo aperto , ma se $\theta$ è un ramo aperto allora l’insieme $S_{\theta }$ di formule su quel ramo è un insieme di Hintikka [ per l’osservazione di prima ]. Ma allora per il Lemma di Hintikka $S_{\theta }$ sarebbe soddisfacibile , allora esiste un’interpretazione $I$ che rende vera tutte le formule $\in S_{\theta }$ , ma allora $I$ rende vera anche $\neg \mathcal{F}$ [ soddisfacibile ] , ma allora $\mathcal{F}$ non è una tautologia .

$\square$

Notazione polacca

Nella notazione polacca , invece di scrivere

• $[p\to q]$ si scrive $[\to pq]$
• $[p\wedge q]$ si scrive $[\wedge pq]$
• $[p\vee q]$ si scrive $[\vee pq]$ questo ci semplifica un sacco perché possiamo scrivere formule senza l’utilizzo delle parentesi. Ad esempio proviamo a scrivere la formula $\neg p\to (q\to \neg r)$ : $$\begin{array}{r}\neg p\wedge (q\to \neg r)=\wedge \neg p(\to q\neg r)=\wedge \neg p\to q\neg r\end{array}$$

Correttezza e completezza del metodo di tableaux per FOL

Vogliamo dimostrare che - secondo la definizione di formula valida e formula dimostrabile con il metodo di tableaux - tutte le formule dimostrabili con il metodo di tableaux sono formule valide ( Con formula valida si intende che quella formula è sempre True ). La “tattica” quindi è simile a quella per la logica proposizionale , quindi dimostriamo la doppia inclusione :

1. da un lato dimostriamo che se una formula è dimostrabile con il metodo ⇒ è una formula valida
2. dall’altro lato dimostriamo che se una formula è valida ⇒ esiste una dimostrazione con il metodo

1. Correttezza

Teorema

Se $\mathcal{F}$ è dimostrabile con il metodo di tableaux , allora $\mathcal{F}$ è una formula valida.

Dimostrazione : Il nostro obiettivo è dimostrare che se parto da $\mathcal{F}$ e faccio il tableaux per $\neg \mathcal{F}$ e ottengo tutti i rami chiusi , allora $\mathcal{F}$ è una formula valida. L’idea di base è che se consideriamo

• $A:$ $\mathcal{F}$ è dimostrabile
• $B:$ $\mathcal{F}$ è una formula valida e siccome il teorema afferma : $A⟹B$ , possiamo dimostrare il contrario ovvero : $$\neg B⟹\neg A$$ ovvero che “se $\mathcal{F}$ NON è una formula valida , allora , $\mathcal{F}$ NON è dimostrabile” . ( siccome dicono la stessa cosa )

Quindi l’idea della dimostrazione sta nei seguenti passi ( osservazioni ) :

1. $\mathcal{F}$ non è una formula valida se e solo se $\neg \mathcal{F}$ è soddisfacibile , ovvero che esiste una interpretazione che la rende True.

Siccome $\neg \mathcal{F}$ è soddisfacibile allora quando vado a svilupparla ci sono 4 casi.

2. incontro formule di tipo $\alpha$ e quindi è come la logica proposizionale [ vedi sopra ]

3. incontro formule di tipo $\beta$ e quindi è come la logica proposizionale [ vedi sopra ]

4. incontro formule di tipo $\gamma$ ovvero formule di tipo universale :

   $$\begin{array}{c}\forall xP(x)\\ P(a)\end{array}\text{oppure}\begin{array}{c}\neg \exists xP(x)\\ \neg P(a)\end{array}$$

dove $a$ è un qualunque parametro , e siccome è un qualunque elemento del dominio , sicuramente con la stessa interpretazione che rende soddisfacibile $\gamma$ ( quelle che sono sopra la riga ), rendiamo soddisfacibile anche $\gamma (a)$ , e quindi entrambe sono soddisfacibile

5. incontro formule di tipo $\delta$ ovvero formule di tipo esistenziale :

$$\begin{array}{c}\exists xP(x)\\ P(a)\end{array}\text{oppure}\begin{array}{c}\neg \forall xP(x)\\ \neg P(a)\end{array}$$

dove $a$ è un nuovo parametro , e siccome è un nuovo elemento del dominio sicuramente con la stessa interpretazione che rende soddisfacibile $\delta$ ( quelle che sono sopra la riga ) sicuramente rendiamo soddisfacibile anche $\delta (a)$ , e quindi entrambe sono soddisfacibili.

Siccome lo sviluppo del tableaux di $\neg \mathcal{F}$ è una sequenza di tableaux intermedi $(t_0,t_1,t_2,\dots )$, ovvero che prima ho la formula $\neg \mathcal{F}$ , poi ho $\neg \mathcal{F}$ con lo sviluppo di quest’ultima e cosi via … Osserviamo che partiamo da $\neg \mathcal{F}=t_0$ che è soddisfacibile e quindi ha almeno un ramo soddisfacibile , allora sicuramente quando lo andiamo ad estendere e ottenere l’altro tableaux $t_1$ , siccome seguo i 4 possibili sviluppi che posso incontrare , ottengo che anche $t_1$ ha almeno un ramo soddisfacibile , e questo vale per sempre ancora andando avanti.

6. Quindi avremo sempre un ramo aperto e quindi il tableaux non si chiude e quindi $\mathcal{F}$ non è dimostrabile

2. Completezza

Teorema

Se $\mathcal{F}$ è una formula valida , allora , $\mathcal{F}$ è dimostrabile con il metodo di tableaux.

Prima della dimostrazione , ci serve definire un metodo “automatico” per lo sviluppo del tableaux :

Definizione

Un tableaux sistematico è un tableaux che viene sviluppato seguendo queste regole :

• Fissiamo un ordine arbitrario per i parametri $a_1,a_2,a_3,\dots$ che andiamo ad usare quando incontriamo o una $\gamma$-formula o una $\delta$-formula.
• Sviluppiamo le formule nell’ordine in cui appaiono [ sarà più lungo ma ok ]
• Quando incontriamo una $\gamma$-formula , usiamo il primo parametro che non abbiamo utilizzato per una formula di tipo $\gamma$ sul ramo che stiamo considerando
• Inoltre quando incontriamo una $\gamma$-formula , la ricopiamo sulle “foglie” del nostro tableaux , in modo da “ricordarci” che possiamo riutilizzarla

Adesso invece ci serve un’altro ingrediente speciale che abbiamo già utilizzato per la logica proposizionale : ovvero gli insiemi di Hintikka

Definizione

Un insieme di formule $S$ è un insieme di Hintikka [ per logica di primo ordine ] se succedono 5 cose [ che sono poi le proprietà dei rami che rimangono aperti ] :

• $H_0$ : in $S$ non c’è mai una formula $\mathcal{F}$ e la sua negata $\neg \mathcal{F}$ [ solo una delle due ]
• $H_1$ : se in $S$ c’è una formula di tipo $\alpha$ allora necessariamente ci devono essere le sue due componenti ${\alpha }_1$ e ${\alpha }_2$
• $H_2$ : se in $S$ c’è una formula di tipo $\beta$ allora necessariamente c’è una delle due componenti ${\beta }_1$ e ${\beta }_2$
• $H_3$ : se in $S$ c’è una formula di tipo $\gamma$ allora necessariamente ci sono anche $\gamma (a_1),\gamma (a_2),\gamma (a_3),\dots$ per tutti gli infiniti parametri $a_n$
• $H_4$ : se in $S$ c’è una formula di tipo $\delta$ allora necessariamente ci sarà anche $\delta (a_i)$ con $i$ random

Dimostrazione : Quindi l’idea della dimostrazione è :

1. Partendo da $\neg \mathcal{F}$ e facciamo un tableaux sistematico , se non si chiude [ o è infinito ] allora ci deve essere almeno un ramo aperto.
2. Se $\theta$ è un ramo aperto , allora l’insieme di formule che sono nel ramo $\theta$ è un insieme di Hintikka
3. Facciamo vedere che ogni insieme di Hintikka è soddisfacibile [Lemma di Hintikka]

Per il punto 3. già lo abbiamo dimostrato per la logica proposizionale , per la logica di primo ordine è identico solo che nel passo induttivo si aggiungono altri 2 casi , ovvero che se la formula che consideriamo di lunghezza $n+1$ :

1. è di tipo $\gamma$ allora per la prop. $H_3$ ci saranno tutte le altre più corte , per ipotesi induttiva sono soddisfacibili , ma se sono tutte soddisfacibili , viene soddisfatta automaticamente anche $\gamma$ [ siccome è universale ]
2. è di tipo $\delta$ allora per la prop. $H_4$ ci sarà $\delta (a_i)$ con $i$ random, ancora per ipotesi induttiva è soddisfacibile e quindi è soddisfacibile anche $\delta$

Quindi se qualunque ramo $\theta$ aperto è un insieme soddisfacibile [perché è un insieme di Hintikka] allora vuol dire che $\neg \mathcal{F}$ è una formula soddisfacibile , ma se $\neg \mathcal{F}$ è soddisfacibile vuol dire che diventa almeno una volta True e quindi $\mathcal{F}$ è False e quindi non può essere valida .

$\square$