Äquivalenzumformung

Einfache Sprache

Eine Äquivalenzumformung ist eine Herleitung, die das Ziel hat die Äquivalenz zweier Aussagenlogischen Formel zu zeigen. Sie besteht aus Schritten folgender Art:

• Direkte Anwendung eines Aussagenlogisches Gesetzes oder
• Anwendung des Ersetzungslemmas mit Angabe
  • der jeweiligen Formel die ersetzt wird,
  • der jeweiligen Äquivalente Substitutionen und
  • eine Begründung für die Äquivalenz der Substitutionen durch die Nennung von aussagenlogischen Gesetzen.

Def. Äquivalenzumformung

Beispiel Äquivalenzumformungen

Wir wollen zeigen das $\varphi \leftrightarrow \psi \models=| (\varphi \wedge \psi) \vee (\neg\varphi \vee \neg \psi)$ gilt.

Folgende Äquivalenzumformung beweist die Aussage.

$$\begin{array}{rcl|l}\varphi\leftrightarrow \psi & \models=|& (\varphi \to \psi) \wedge (\psi \to \varphi) &\text{Paraphrasierung von $\leftrightarrow$} \\ &\models=|& (\neg \varphi \vee \psi) \wedge (\neg \psi \vee \varphi) & \text{Ersetzungslemma für $X_0 \wedge X_1$ mit} \\ &&& \sigma = \{ X_0 \mapsto \varphi \to \psi, X_1 \mapsto \psi \to \varphi \} \\ &&& \sigma' = \{ X_0 \mapsto \neg\varphi \vee \psi, X_1 \mapsto \neg\psi \vee \varphi \} \\ &&& \text{zwei Mal Paraphrasierung von $\rightarrow$}\\ & \models=| & ((\neg \varphi \vee \psi) \wedge \neg \psi) \vee ((\neg \varphi \vee \psi) \wedge \varphi) & \text{Distributivität von $\wedge$}\\ &\models=|& (\neg \psi \wedge (\neg \varphi \vee \psi)) \vee (\varphi \wedge (\neg \varphi \vee \psi)) & \text{Ersetzungslemma für $X_0 \vee X_1$ mit} \\ &&& \sigma = \{ X_0 \mapsto (\neg \varphi \vee \psi) \wedge \neg \psi, X_1 \mapsto (\neg \varphi \vee \psi) \wedge \varphi\} \\ &&& \sigma' = \{ X_0 \mapsto \neg \psi \wedge (\neg\varphi \vee \psi), X_1 \mapsto \varphi \wedge (\neg\varphi \vee \psi) \} \\ &&& \text{zwei Mal Kommutativität von $\wedge$}\\ &\models=|& ((\neg \psi \wedge \neg \varphi) \vee (\neg \psi \wedge \psi)) \vee ((\varphi \wedge \neg \varphi) \vee (\varphi \wedge \psi)) & \text{Ersetzungslemma für $X_0 \vee X_1$ mit} \\ &&& \sigma = \{ X_0 \mapsto \neg \psi \wedge (\neg\varphi \vee \psi), X_1 \mapsto \varphi \wedge (\neg\varphi \vee \psi) \} \\ &&& \sigma' = \{ X_0 \mapsto (\neg \psi \wedge \neg \varphi) \vee (\neg \psi \wedge \psi), X_1 \mapsto (\varphi \wedge \neg \varphi) \vee (\varphi \wedge \psi) \} \\ &&& \text{zwei Mal Distributivität von $\wedge$} \\ &\models=|& ((\neg \psi \wedge \neg \varphi) \vee (\psi \wedge \neg \psi)) \vee (\bot \vee (\varphi \wedge \psi)) & \text{Ersetzungslemma für $((\neg \psi \wedge \neg \varphi) \vee X_i) \vee (X_j \vee (\varphi \wedge \psi))$ mit} \\ &&& \sigma = \{X_i \mapsto \neg \psi \wedge \psi, X_j \mapsto \varphi \wedge \neg \varphi \} \\ &&& \sigma' = \{ X_i \mapsto \psi \wedge \neg \psi, X_j \mapsto \bot \} \\ &&& \text{Kommutativität von $\wedge$, Komplement für $\wedge$} \\ &\models=|& ((\neg \psi \wedge \neg \varphi) \vee \bot) \vee ((\varphi \wedge \psi) \vee \bot)& \text{Ersetzungslemma für $((\neg \psi \wedge \neg \varphi) \vee X_i) \vee X_j$ mit} \\ &&& \sigma = \{ X_i \mapsto \psi \wedge \neg \psi, X_j \mapsto \bot \vee (\varphi \wedge \psi) \} \\ &&& \sigma' = \{ X_i \mapsto \bot, X_j \mapsto (\varphi \wedge \psi) \vee \bot \} \\ &&& \text{Komplement für $\wedge$, Kommutativität von $\wedge$} \\ &\models=|& (\neg \psi \wedge \neg \varphi) \vee (\varphi \wedge \psi) & \text{Ersetzungslemma für $X_0 \vee X_1$ mit} \\ &&& \sigma = \{ X_0 \mapsto (\neg \psi \wedge \neg \varphi) \vee \bot, X_1 \mapsto (\varphi \wedge \psi) \vee \bot \} \\ &&& \sigma' = \{ X_0 \mapsto \neg \psi \wedge \neg \varphi, X_1 \mapsto \varphi \wedge \psi \} \\ &&& \text{zwei Mal Neutralität für $\vee$} \\ &\models=|& (\neg \varphi \wedge \neg \psi) \vee (\varphi \wedge \psi) & \text{Ersetzungslemma für $X_i \vee (\varphi \wedge \psi)$ mit} \\ &&& \sigma = \{ X_i \mapsto \neg \psi \wedge \neg \varphi\} \\ &&& \sigma' = \{ X_i \mapsto \neg \varphi \wedge \neg \psi \} \\ &&& \text{Kommutativität von $\wedge$} \\ &\models=|& (\varphi \wedge \psi) \vee (\neg \varphi \wedge \neg \psi) & \text{Kommutativität $\vee$}\end{array}$$