Logica matematica/Calcolo delle proposizioni/I tableaux semantici: differenze tra le versioni

Sia <math>\Gamma_0</math> un insieme finito di formule. Allora, <math>\Gamma_0 \vdash_T A</math> sse <math>\Gamma_0 \cup \{\neg A\}</math> è insoddifacibileinsoddisfacibile.

Per definizione, <math>\Gamma_0 \vdash_T A</math> sse esiste una tableau-deduzione <math>\mathcal{T}</math> di <math>A</math> da <math>\Gamma_0</math>. <math>\mathcal{T}</math> è un tableau chiuso. Per il teorema dei modelli, abbiamo che <math>\mathcal{T}</math> è chiuso sse <math>\mathrm T(\Gamma_0 \cup \{\neg A\})</math> è insoddisfacibile, dunque, per il [[Logica matematica/Calcolo delle proposizioni/I tableaux semantici#Lemma della verità|lemma della verità]], <math>\mathrm T(\Gamma_0 \cup \{\neg A\})</math> è insoddifacibileinsoddisfacibile sse <math>\Gamma_0 \cup \{\neg A\}</math> è insoddifacibileinsoddisfacibile.

Dato che <math>\Gamma_0 \subseteq \Gamma</math>, allora <math>\Gamma_0 \cup \{\neg A\} \subseteq \Gamma \cup \{\neg A\} </math>. Dal [[Logica matematica/Calcolo delle proposizioni#Teorema di compattezza della soddisfacibilità|teorema di compattezza della soddisfacibilità]], sapendo che <math>\Gamma_0 \cup \{\neg A\} \subseteq \Gamma \cup \{\neg A\} </math>, si deduce che <math>\Gamma_0 \cup \{\neg A\}</math> è insoddifacibileinsoddisfacibile sse <math>\Gamma \cup \{\neg A\}</math> è insoddisfacibile e, per il lemma della verità, <math>\Gamma \cup \{\neg A\}</math> è insoddisfacibile sse <math>\mathrm T(\Gamma \cup \{\neg A\})</math> è insoddisfacibile; quindi, per il teorema dei modelli, abbiamo che <math>\mathrm T(\Gamma \cup \{\neg A\})</math> è insoddisfacibile sse <math>\mathrm T(\Gamma \cup \{\neg A\})</math> ha un tableau chiuso sse <math>\Gamma \vdash_T A</math>, quindi <math>\Gamma_0 \vdash_T A</math> sse <math>\Gamma \vdash_T A</math>.

Per il [[Logica matematica/Calcolo delle proposizioni/I tableaux semantici#Teorema di compattezza della dimostrabilità|teorema di compattezza]], <math>\Gamma \vdash_T A</math> sse esiste un insieme finito di formule <math>\Gamma_0 \subseteq \Gamma</math> tale che <math>\Gamma_0 \vdash_T A</math>. Per il [[Logica matematica/Calcolo delle proposizioni/I tableaux semantici#Lemma della dimostrabilità|lemma della dimostrabilità]], <math>\Gamma_0 \vdash_T A</math> sse <math>\Gamma_0 \cup \{\neg A\}</math> è insoddifacibileinsoddisfacibile. Dal [[Logica matematica/Calcolo delle proposizioni#Teorema di soddisfacibilità|teorema di soddisfacibilità]], <math>\Gamma_0 \cup \{\neg A\}</math> è insoddifacibileinsoddisfacibile sse <math>\Gamma_0 \vDash A</math> e, dal [[Logica matematica/Calcolo delle proposizioni#Corollario del teorema di compattezza|corollario del teorema di compattezza della soddisfacibilità]], abbiamo che <math>\Gamma_0 \vDash A</math> sse <math>\Gamma \vDash A</math>.