TU Wien:Einführung in wissensbasierte Systeme VU (Egly)/Übungen WS12/Blatt 3 - Beispiel 5

Let $T\,$ be a consistent propositional theory. Show that ${\text{CWA}}(T)$ is inconsistent iff there are atomic formulas $a_{1},...,a_{n}$ such that $T\models a_{1}\lor ...\lor a_{n}$ and $T\models a_{i}{\text{ for }}i=1,...,n$.

Hint: to show the only-if direction (left to right implication) you might first prove that if ${\text{CWA}}(T)$ is inconsistent, then $T_{asm}$ is non-empty. Further on, you might find it useful to consider the propositional variables appearing in $T_{asm}$ and to use the Contradiction Theorem.

Lösungsvorschlag

Ich beginne hier mal mit der Richtung von links nach rechts, denn die andere Richtung ist trivial. Laut Hinweis soll man als erstes zeigen, dass $T_{asm}$ nicht leer sein kann, wenn $CWA(T)$ inconsistent ist.

$\Rightarrow :$

Laut Voraussetzung ist $CWA(T)$ inconsistent und $T$ consistent

Schritt 1: $T_{asm}\neq \varnothing$

Per Definition: $CWA(T)=\{\varphi |T\cup T_{asm}\models \varphi ,\varphi \ closed\}$

Annahme: $T_{asm}=\varnothing$

Dann gilt:

$CWA(T)=\{\varphi |T\cup T_{asm}\models \varphi ,\varphi \ closed\}=\{\varphi |T\models \varphi ,\varphi \ closed\}=Cn(T)$

$Cn(T)$ ist aber nur dannn inconsistent wenn $T$ inconsistent ist $\Rightarrow$ Widerspruch

Schritt 2: Es gibt besagte Atomformeln

Contradiction Theorem: $W\cup \{\phi \}\ unsatisfiable\Leftrightarrow W\models \neg \phi$

$T_{asm}=\{\neg P|P\ ground\ atom,T\not \models P\}$

Da $T$ consistent aber $T\cup T_{asm}$ inconsistent (bzw. unerfüllbar), muss es ein $C\subseteq T_{asm}$ geben mit $T\cup C$ inconsistent. Das heißt aber genau, dass $T\cup C$ unerfüllbar ist und deshalb folgt aus dem Contradiction Theorem $T\models \neg C$. Jetzt stammt aber $C$ aus $T_{asm}$ und $T_{asm}$ enthält nur Negationen, sprich $C$ ist von der Form $\neg a_{1}\land \neg a_{2}\land ...\land \neg a_{n}$ sprich $T\models \neg (\neg a_{1}\land \neg a_{2}\land ...\land \neg a_{n})\equiv T\models a_{1}\lor a_{2}\lor ...\lor a_{n}$. Da aber $C\subseteq T_{asm}$ gilt gleichzeitig $T\not \models a_{i},i=1..n$

$\Leftarrow :$

Diese Richtung ist trivial, da sobald eine Disjunktion aber gleichzeitig die Negation aller Glieder enthalten ist, die entstehende Menge inconsistent sein muss.