Dimostrazione teorema di completezza forte
Assumo l'ipotesi di lavorare sempre con strutture che utilizzano l'algebra di Boole a due valori (${0,1}$).
Teorema di completezza forte:
Siano $Gamma$ un arbitrario insieme di proposizioni e $A$ una proposizione tali che per ogni struttura e per ogni interpretazione $V(-)$ si abbia $V(Gamma)<=V(A)$. Allora $Gamma\vdashA$.
Per dimostrare il teorema di completezza forte si utilizzano i seguenti due teoremi:
Teorema di completezza debole:
Siano $Gamma$ un insieme finito di proposizioni e $A$ una proposizione tali che per ogni struttura e per ogni interpretazione $V(-)$ si abbia $V(Gamma)<=V(A)$. Allora $Gamma\vdashA$.
Teorema di compattezza:
Sia $Gamma$ un insieme di formule in un linguaggio del primo ordine. Allora $Gamma $ è soddisfacibile se e solo se ogni suo sottoinsieme finito $Gamma_0$ è soddisfacibile.
Dimostrazione del teorema di completezza forte:
Siano $Gamma$ un arbitrario insieme di proposizioni e $A$ una proposizione tali che per ogni struttura e per ogni interpretazione $V(-)$ si abbia $V(Gamma)<=V(A)$.
Allora in ogni struttura in cui vale $Gamma$ (cioè $V(Gamma)=1$) deve valere anche $A$ (cioè $V(A)=1$).
Allora l'insieme $Gammauu{\notA}$ non può essere soddisfacibile.
Allora per il teorema di compattezza esiste un sottoinsieme finito $Gamma_0$ di $Gamma$ tale che $Gamma_0uu{\notA}$ non è soddisfacibile.
Allora per ogni struttura e per ogni interpretazione $V(-)$ si ha $V(Gamma_0)<=V(A)$.
Allora $Gamma_0\vdashA$.
Allora $Gamma\vdashA$.
Quello che non mi è chiaro è il passaggio
Perchè il fatto che $Gamma_0uu{\notA}$ non sia soddisfacibile comporta che $V(Gamma_0)<=V(A)$?
Teorema di completezza forte:
Siano $Gamma$ un arbitrario insieme di proposizioni e $A$ una proposizione tali che per ogni struttura e per ogni interpretazione $V(-)$ si abbia $V(Gamma)<=V(A)$. Allora $Gamma\vdashA$.
Per dimostrare il teorema di completezza forte si utilizzano i seguenti due teoremi:
Teorema di completezza debole:
Siano $Gamma$ un insieme finito di proposizioni e $A$ una proposizione tali che per ogni struttura e per ogni interpretazione $V(-)$ si abbia $V(Gamma)<=V(A)$. Allora $Gamma\vdashA$.
Teorema di compattezza:
Sia $Gamma$ un insieme di formule in un linguaggio del primo ordine. Allora $Gamma $ è soddisfacibile se e solo se ogni suo sottoinsieme finito $Gamma_0$ è soddisfacibile.
Dimostrazione del teorema di completezza forte:
Siano $Gamma$ un arbitrario insieme di proposizioni e $A$ una proposizione tali che per ogni struttura e per ogni interpretazione $V(-)$ si abbia $V(Gamma)<=V(A)$.
Allora in ogni struttura in cui vale $Gamma$ (cioè $V(Gamma)=1$) deve valere anche $A$ (cioè $V(A)=1$).
Allora l'insieme $Gammauu{\notA}$ non può essere soddisfacibile.
Allora per il teorema di compattezza esiste un sottoinsieme finito $Gamma_0$ di $Gamma$ tale che $Gamma_0uu{\notA}$ non è soddisfacibile.
Allora per ogni struttura e per ogni interpretazione $V(-)$ si ha $V(Gamma_0)<=V(A)$.
Allora $Gamma_0\vdashA$.
Allora $Gamma\vdashA$.
Quello che non mi è chiaro è il passaggio
Allora per il teorema di compattezza esiste un sottoinsieme finito $Gamma_0$ di $Gamma$ tale che $Gamma_0uu{\notA}$ non è soddisfacibile.
Allora per ogni struttura e per ogni interpretazione $V(-)$ si ha $V(Gamma_0)<=V(A)$.
Perchè il fatto che $Gamma_0uu{\notA}$ non sia soddisfacibile comporta che $V(Gamma_0)<=V(A)$?
Risposte
Ciao,
Io affrontai in maniera un po' diversa questa dimostrazione, comunque il tuo dubbio, se ho interpretato bene il simbolismo perché ero abituata ad altro, è, tra le mie carte, proprio un lemma, anzi, un "se e solo se".
Purtroppo posso solo fornirti una versione più discorsiva e leggera:
$T$ conseguenza logica di $A$ se e solo se $A\cup \{\not T\}$ non soddisfacibile.
Dim. $T$ è conseguenza logica di $A$ se e solo se $T$ è valido in ogni modello di $A$, se e solo se $\not T$ è soddisfatto in nessun modello di $A$, ovvero $A\cup \{\not T\}$ è non soddisfacibile.
Io affrontai in maniera un po' diversa questa dimostrazione, comunque il tuo dubbio, se ho interpretato bene il simbolismo perché ero abituata ad altro, è, tra le mie carte, proprio un lemma, anzi, un "se e solo se".
Purtroppo posso solo fornirti una versione più discorsiva e leggera:
$T$ conseguenza logica di $A$ se e solo se $A\cup \{\not T\}$ non soddisfacibile.
Dim. $T$ è conseguenza logica di $A$ se e solo se $T$ è valido in ogni modello di $A$, se e solo se $\not T$ è soddisfatto in nessun modello di $A$, ovvero $A\cup \{\not T\}$ è non soddisfacibile.
"thedarkhero":
Quello che non mi è chiaro è il passaggio
Allora per il teorema di compattezza esiste un sottoinsieme finito $Gamma_0$ di $Gamma$ tale che $Gamma_0uu{\notA}$ non è soddisfacibile.
Allora per ogni struttura e per ogni interpretazione $V(-)$ si ha $V(Gamma_0)<=V(A)$.
Perchè il fatto che $Gamma_0uu{\notA}$ non sia soddisfacibile comporta che $V(Gamma_0)<=V(A)$?
È passato un po' di tempo dall'ultima volta che mi sono attivamente occupato di logica del prim'ordine. Tuttavia, direi che l'ipotesi implica [tex]V(\Gamma_0 \cup \{\lnot A\}) = 0[/tex] per ogni funzione di interpretazione (per ogni modello del linguaggio). Ora, [tex]V(\Gamma_0 \cup \{\lnot A\}) = V(\Gamma_0) \wedge V(\{\lnot A\})[/tex], dove [tex]\wedge[/tex] denota l'operazione di meet nell'algebra di Boole $\{0,1\}$; ne segue che o [tex]V(\Gamma_0) = 0[/tex] oppure [tex]V(\{\lnot A\}) = 0[/tex], i.e. o [tex]V(\Gamma_0) = 0[/tex] oppure [tex]V(\{A\}) = 1[/tex].
Se [tex]V(\Gamma_0) = 0[/tex], allora [tex]V(\Gamma_0) \le V(\{A\})[/tex] (per forza di cose).
Se invece [tex]V(\Gamma_0) = 1[/tex], allora necessariamente [tex]V(\{A\}) = 1[/tex] per l'argomentazione precedente.
Quindi [tex]V(\Gamma_0) \le V(\{A\})[/tex] per ogni funzione di interpretazione $V$.