Proprietà della conseguenza logica

Teorema: $\Delta\models A$ se e solo se $\Delta \cup \{\neg A\}$ è insoddisfacibile

Caso particolare

Nel caso in cui $\Delta= \varnothing$, la definizione di conseguenza logica diventa: $A$ è una conseguenza logica di $\varnothing$ se, per ogni valutazione $v$ tale che $v\models \varnothing$, si ha $v\models A$.

$v\models \varnothing$ è vero se, per ogni formula $A$ in $\varnothing$, $v\models A$. Siccome non c’è alcuna formula $A\in \varnothing$ da considerare, $v\models \varnothing$ è vero indipendentemente dalla scetla di $v$. Allora, tornando alla definizione di conseguenza logica, la condizione “tale che $v \models \varnothing$” si elimina, in quanto sempre verificata: $A$ è una conseguenza logica di $\varnothing$ se, per ogni valutazione $v$, $v\models A$, cioè se $A$ è una tautologia. Si ottiene così il seguente corollario del teorema precedente:

Corollario: $A$ è una tautologia se e solo se $\neg A$ è insoddisfacibile.

Teorema di deduzione (semantica)

Teorema: $\Delta,\ A\models B$ se e solo se $\Delta \models A\rarr B$.

Nota: Per semplificare la notazione, alla sinistra del simbolo di conseguenza logica si scrive $\Delta, \ A$ per indicare l’insieme $\Delta \cup \{A\}$.

Proprietà utile

Proposizione: $\Delta, A\models B\rarr C$ se e solo se $\Delta \models A\land B\rarr C$.

Alcune considerazioni

Sia $\Delta=\{A_1, ..., A_n\}$ un insieme finito di formule, tali che $A_1, ..., A_n\models B$. Applicando iterativamente il teorema di deduzione, si ottiene:

Untitled

Poi, utilizzando la proprietà

$$ \Delta, A\models B\rarr C\ \ sse\ \ \Delta \models A\land B\rarr C $$

le formule ottenute dalle applicazioni del teorema di deduzione possono essere riscritte usando la congiunzione invece di una catena di implicazioni: