Actions

Deriving equivalences in propositional logic

From Learning Logic for Computer Science

Starting from a (small) set of laws of propositional logic and using basic properties of the equivalence relation one can derive equivalences between propositional formulas. This is a purely syntactic way of proving equivalences.

Example of proving an equivalence

As an example, we consider the equivalence $$(X_2 \wedge \neg X_0) \leftrightarrow X_1 \SemEquiv ((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge (X_1 \rightarrow (X_2 \wedge \neg X_0)) \enspace.$$ Our goal is to establish this equivalence in a purely syntactic fashion.

First, we notice that (rew$\leftrightarrow$) gives us: $$(X_2 \wedge \neg X_0) \leftrightarrow X_1 \SemEquiv (\neg (X_2 \wedge \neg X_0) \vee X_1) \wedge ((X_2 \wedge \neg X_0) \vee \neg X_1) \enspace.$$ To be more precise, we not only use (rew$\leftrightarrow$), but also that in a given equivalence variables can be replaced by formulas.

Further, (rew$\rightarrow$) in combination with the symmetry of $\SemEquiv$ tells us: $$\neg (X_2 \wedge \neg X_0) \vee X_1 \SemEquiv (X_2 \wedge \neg X_0) \rightarrow X_1 \enspace.$$ Again, we also use that in a given equivalence variables can be replaced by formulas.

If we now use that formulas can be replaced by equivalent formulas (which is a generalization of the congruence property of $\SemEquiv$, see below), then we obtain: $$(\neg (X_2 \wedge \neg X_0) \vee X_1) \wedge ((X_2 \wedge \neg X_0) \vee \neg X_1) \SemEquiv ((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge ((X_2 \wedge \neg X_0) \vee \neg X_1) \enspace.$$

Using (com$\vee$) in the same fashion, we obtain $$((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge ((X_2 \wedge \neg X_0) \vee \neg X_1) \SemEquiv ((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge (\neg X_1 \vee (X_2 \wedge \neg X_0))\enspace.$$

Next, using (rew$\rightarrow$) and the symmetry of $\SemEquiv$, we obtain: $$((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge (\neg X_1 \vee (X_2 \wedge \neg X_0)) \SemEquiv ((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge (X_1 \rightarrow (X_2 \wedge \neg X_0)) \enspace.$$

Finally, we use transitivity of $\SemEquiv$ several times to obtain the desired equivalence.

What we have used:

  • The laws of propositions logic.
  • The basic properties of the equivalence relation (symmetry, transitivity).
  • That variables in equivalences can be replaced by formulas (equivalence lemma).
  • That subformulas can be replaced by equivalent ones (congruence lemma, below).

All this, except for the last item, is discussed in equivalence and substitution. The last item ist discussed below.

Generalized congruence lemma

In the above chain of reasoning, a generalized congruence property of the equivalence relation plays a crucial role. This can be formalized using the notion of equivalent substitutions.

Definition Substitutions $\sigma_0$ and $\sigma_1$ are equivalent, in symbols $\sigma_0 \SemEquiv \sigma_1$, if $X_i\sigma_0 \SemEquiv X_i\sigma_1$ holds for all $i \in \mathbf N$.

Congruence lemma (generalized variant) Let $\varphi$ be a propositional formula and $\sigma_0$ and $\sigma_1$ substitutions. If $\sigma_0 \SemEquiv \sigma_1$, then $\varphi\sigma_0 \SemEquiv \varphi\sigma_1$.

Proof The proof is by induction on $\varphi$.

Base cases. Let $\varphi = \bot$. Then \begin{align} \varphi\sigma_0 & = \bot\sigma_0\\ & = \bot && \text{application of $\sigma_0$}\\ & = \bot\sigma_1 && \text{application of $\sigma_1$}\\ & = \varphi\sigma_1 \end{align}

The argument for $\varphi = \top$ is dual.

Let $\varphi = X_i$ for some $i$. Then \begin{align} \varphi\sigma_0 & = X_i\sigma_0\\ & \SemEquiv X_i\sigma_1 && \text{assumption $\sigma_0 \SemEquiv \sigma_1$}\\ & = \varphi\sigma_1 \end{align}

Inductive step. Let $\varphi = C(\varphi_0, \dots, \varphi_{n-1})$ for $C$ an $n$-ary connective and $\varphi_0, \dots, \varphi_{n-1}$ propositional formulas. The inductive assumption is that $\varphi_i\sigma_0 \SemEquiv \varphi_i\sigma_1$ holds for every $i<n$. Then \begin{align} C(\varphi_0, \dots, \varphi_{n-1})\sigma_0 & = C(\varphi_0\sigma_0, \dots, \varphi_{n-1}\sigma_0) && \text{application of $\sigma_0$}\\ & \SemEquiv C(\varphi_0\sigma_1, \dots, \varphi_{n-1}\sigma_1) && \text{congruence property (simple variant)}\\ & = C(\varphi_0, \dots, \varphi_{n-1})\sigma_1 && \text{application of $\sigma_1$} \end{align} This concludes the proof.

Example Let $\psi = X_2 \wedge (X_0 \vee \neg X_1)$, $\sigma_0 = \{X_2 \mapsto \neg X_0 \vee X_1\}$, and $\sigma_2 = \{X_2 \mapsto X_0 \rightarrow X_1\}$. Applying the lemma, we obtain $$ (\neg X_0 \vee X_1) \wedge (X_0 \vee \neg X_1) \SemEquiv (X_0 \rightarrow X_1) \wedge (X_0 \vee \neg X_1) \enspace.$$

Formal derivations of equivalences

A formal derivation of an equivalence is a formalized version of the above reasoning. It is a chain of equivalences where each step is an application of the congruence lemma in combination with the equivalence lemma and one of the list of laws of propositional logic.

Every step is justified by:

  • the law used,
  • the substitution applied to the law (according to the equivalence lemma),
  • the formula the congruence lemma is applied to,
  • the suitable substitutions.

Reflexivity, symmetry, and transitivity of the equivalence relation can be used without mentioning them.

Here is an example: \begin{aligned} (X_2 \wedge \neg X_0) \leftrightarrow X_1 & \SemEquiv (\neg (X_2 \wedge \neg X_0) \vee X_1) \wedge ((X_2 \wedge \neg X_0) \vee \neg X_1) & & \text{(rew$\leftrightarrow$)} \text{ with } \{X_0 \mapsto X_2 \wedge \neg X_0\}\\ & \SemEquiv ((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge ((X_2 \wedge \neg X_0) \vee \neg X_1) & & \text{(rew$\rightarrow$) with } \{X_0 \mapsto X_2 \wedge \neg X_0\} \text{ applied to} \\ & & & \quad X_3 \wedge ((X_2 \wedge \neg X_0) \vee \neg X_1) \text{ with } \\ & & & \qquad \{X_3 \mapsto \neg (X_2 \wedge \neg X_0) \vee X_1\}\\ & & & \qquad \{X_3 \mapsto (X_2 \wedge \neg X_0) \rightarrow X_1\} \\ & \SemEquiv ((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge (\neg X_1 \vee (X_2 \wedge \neg X_0)) & & \text{(com$\vee$) with } \{X_0 \mapsto X_2 \wedge \neg X_0, X_1 \mapsto \neg X_1\} \text{ applied to} \\ & & & \quad ((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge X_3 \text{ with } \\ & & & \qquad \{X_3 \mapsto (X_2 \wedge \neg X_0) \vee \neg X_1\} \text{ and } \\ & & & \qquad \{X_3 \mapsto \neg X_1 \vee (X_2 \wedge \neg X_0)\} \\ & \SemEquiv ((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge (X_1 \rightarrow (X_2 \wedge \neg X_0)) & & \text{(rew$\rightarrow$) with } \{X_0 \mapsto X_1, X_1 \mapsto X_2 \wedge \neg X_0\} \text{ applied to} \\ & & & \quad ((X_2 \wedge \neg X_0) \rightarrow X_1) \wedge X_3 \text{ with } \\ & & & \qquad \{X_3 \mapsto \neg X_1 \vee (X_2 \wedge \neg X_0)\} \\ & & & \qquad \{X_3 \mapsto X_1 \rightarrow (X_2 \wedge \neg X_0)\} \end{aligned}

Completeness

An obvious question is whether every equivalence can be derived formally. The answer is the following theorem.

Theorem Let $\varphi$ and $\psi$ be propositional formulas. Then $\varphi \SemEquiv \psi$ if, and only if, the equivalence can be formally derived.

Exercises

Exercise Leiten Sie eine der beiden Varianten des Gesetzes (ann) formal unter ausschließlichem Rückgriff auf die Basisaxiome nach den hier gemachten Vorgaben her.



Lösung

\begin{aligned} X_0 \wedge \bot & \SemEquiv \bot \wedge X_0 && \text{(comm) mit } \{X_1\mapsto \bot\} \\ & \SemEquiv (\bot \wedge X_0) \vee \bot && \text{(id) mit } \{X_0\mapsto \bot \wedge X_0\} \\ & \SemEquiv (\bot \wedge X_0) \vee (X_0\wedge \neg X_0) && \text{(comp)} \text{ angewendet auf } \\ &&& \quad (\bot \wedge X_0) \vee X_1 \text{ mit } \\ &&& \qquad \{X_1 \mapsto \bot\} \\ &&& \qquad \{X_1 \mapsto X_0\wedge \neg X_0\}\\ & \SemEquiv (\bot \wedge X_0) \vee (\neg X_0\wedge X_0) && \text{(comm) mit } \{X_0 \mapsto X_0, X_1\mapsto \neg X_0\} \text{ angewendet auf } \\ &&& \quad (\bot \wedge X_0) \vee X_1 \text{ mit } \\ &&& \qquad \{X_1 \mapsto X_0 \wedge \neg X_0\} \\ &&& \qquad \{X_1 \mapsto \neg X_0 \wedge X_0\} \\ & \SemEquiv (\bot \vee \neg X_0) \wedge X_0 && \text{(dist) mit } \{X_0\mapsto \bot, X_1\mapsto \neg X_0, X_2 \mapsto X_0\} \\ & \SemEquiv (\neg X_0 \vee \bot) \wedge X_0 && \text{(comm) mit } \{X_0 \mapsto \bot, X_1\mapsto \neg X_0\} \text{ angewendet auf } \\ &&& \quad (X_1) \wedge X_0 \text{ mit } \\ &&& \qquad \{X_1 \mapsto \bot \vee \neg X_0\} \\ &&& \qquad \{X_1 \mapsto \neg X_0 \vee \bot\} \\ & \SemEquiv \neg X_0 \wedge X_0 && \text{(id) mit } \{X_0 \mapsto \neg X_0\} \text{ angewendet auf } \\ &&& \quad X_1 \vee X_0 \text{ mit } \\ &&& \qquad \{X_1 \mapsto \neg X_0 \} \\ &&& \qquad \{X_1 \mapsto \neg X_0 \vee \bot \} \\ & \SemEquiv X_0 \wedge \neg X_0 && \text{(comm) mit } \{X_0 \mapsto \neg X_0, X_1\mapsto X_0\}\\ & \SemEquiv \bot && \text{(comp) }\\ \end{aligned}
\begin{aligned} X_0 \vee \top & \SemEquiv \top \vee X_0 && \text{(comm) mit } \{X_1\mapsto \top\} \\ & \SemEquiv (\top \vee X_0) \wedge \top && \text{(id) mit } \{X_0\mapsto \top \vee X_0\} \\ & \SemEquiv (\top \vee X_0) \wedge (X_0\vee \neg X_0) && \text{(comp)} \text{ angewendet auf } \\ &&& \quad (\top \vee X_0) \wedge X_1 \text{ mit } \\ &&& \qquad \{X_1 \mapsto \top\} \\ &&& \qquad \{X_1 \mapsto X_0\vee \neg X_0\}\\ & \SemEquiv (\top \vee X_0) \wedge (\neg X_0\vee X_0) && \text{(comm) mit } \{X_0 \mapsto X_0, X_1\mapsto \neg X_0\} \text{ angewendet auf } \\ &&& \quad (\top \vee X_0) \wedge X_1 \text{ mit } \\ &&& \qquad \{X_1 \mapsto X_0 \vee \neg X_0\} \\ &&& \qquad \{X_1 \mapsto \neg X_0 \vee X_0\} \\ & \SemEquiv (\top \wedge \neg X_0) \vee X_0 && \text{(dist) mit } \{X_0\mapsto \top, X_1\mapsto \neg X_0, X_2 \mapsto X_0\} \\ & \SemEquiv (\neg X_0 \wedge \top) \vee X_0 && \text{(comm) mit } \{X_0 \mapsto \top, X_1\mapsto \neg X_0\} \text{ angewendet auf } \\ &&& \quad (X_1) \vee X_0 \text{ mit } \\ &&& \qquad \{X_1 \mapsto \top \wedge \neg X_0\} \\ &&& \qquad \{X_1 \mapsto \neg X_0 \wedge \top\} \\ & \SemEquiv \neg X_0 \vee X_0 && \text{(id) mit } \{X_0 \mapsto \neg X_0\} \text{ angewendet auf } \\ &&& \quad X_1 \vee X_0 \text{ mit } \\ &&& \qquad \{X_1 \mapsto \neg X_0 \} \\ &&& \qquad \{X_1 \mapsto \neg X_0 \wedge \top \} \\ & \SemEquiv X_0 \vee \neg X_0 && \text{(comm) mit } \{X_0 \mapsto \neg X_0, X_1\mapsto X_0\}\\ & \SemEquiv \top && \text{(comp) }\\ \end{aligned}

$~$

Exercise Leiten Sie die Äquivalenz $\neg ((X_0 \rightarrow X_2) \rightarrow X_3) \wedge X_4 \SemEquiv (X_4 \wedge \neg X_3) \wedge (X_0 \rightarrow X_2)$ formal unter Rückgriff auf die Basisaxiome sowie den aussagenlogischen Gesetzen nach den hier gemachten Vorgaben her.



Lösung

\begin{aligned} \neg ((X_0 \rightarrow X_2) \rightarrow X_3) \wedge X_4 & \SemEquiv \neg (\neg (X_0 \rightarrow X_2) \vee X_3) \wedge X_4 & & \text{(rew$\rightarrow$) mit } \{X_0\mapsto (X_0 \rightarrow X_2), X_1\mapsto X_3\} \text{ angewendet auf } \\ & & & \quad \neg (X_0) \wedge X_4 \text{ mit } \\ & & & \qquad \{X_0 \mapsto (X_0 \rightarrow X_2) \rightarrow X_3 \} \\ & & & \qquad \{X_0 \mapsto \neg (X_0 \rightarrow X_2) \vee X_3 \}\\ & \SemEquiv (\neg\neg (X_0 \rightarrow X_2) \wedge \neg X_3) \wedge X_4 & & \text{(demo) mit } \{X_0\mapsto \neg(X_0 \rightarrow X_2), X_1\mapsto X_3\} \text{ angewendet auf } \\ & & & \quad X_0 \wedge X_4 \text{ mit } \\ & & & \qquad \{X_0 \mapsto \neg(\neg (X_0 \rightarrow X_2) \vee X_3) \} \\ & & & \qquad \{X_0 \mapsto \neg\neg (X_0 \rightarrow X_2) \wedge \neg X_3 \}\\ & \SemEquiv ( (X_0 \rightarrow X_2) \wedge \neg X_3) \wedge X_4 & & \text{(done) mit } \{X_0\mapsto (X_0 \rightarrow X_2)\} \text{ angewendet auf } \\ & & & \quad ( X_0 \wedge \neg X_3) \wedge X_4 \text{ mit } \\ & & & \qquad \{X_0 \mapsto \neg\neg (X_0 \rightarrow X_2) \} \\ & & & \qquad \{X_0 \mapsto (X_0 \rightarrow X_2) \}\\ & \SemEquiv (X_0 \rightarrow X_2) \wedge (\neg X_3 \wedge X_4) & & \text{(ass) mit } \{X_0\mapsto (X_0 \rightarrow X_2), X_1 \mapsto \neg X_3, X_2\mapsto X_4\} \\ & \SemEquiv (\neg X_3 \wedge X_4) \wedge (X_0 \rightarrow X_2) & & \text{(comm) mit } \{X_0\mapsto (X_0 \rightarrow X_2), X_1 \mapsto (\neg X_3 \wedge X_4)\} \\ & \SemEquiv (X_4 \wedge \neg X_3) \wedge (X_0 \rightarrow X_2) & & \text{(comm) mit } \{X_0\mapsto \neg X_3, X_1\mapsto X_4\} \text{ angewendet auf } \\ & & & \quad X_5\wedge (X_0 \rightarrow X_2) \text{ mit } \\ & & & \qquad \{X_5 \mapsto \neg X_3 \wedge X_4 \} \\ & & & \qquad \{X_5 \mapsto X_4 \wedge \neg X_3 \}\\ \end{aligned}

$~$

Exercise Leiten Sie eine der beiden Äquivalenzen \begin{align*} \neg\bigwedge_{i=0}^n X_i&\mathrel{=\!\!\!{\vert}{\vert}\!\!\!=}\bigvee_{i=0}^n \neg X_i\\ \neg\bigvee_{i=0}^n X_i&\mathrel{=\!\!\!{\vert}{\vert}\!\!\!=}\bigwedge_{i=0}^n \neg X_i \end{align*} als Verallgemeinerung der De Morganschen Regel (demo) für mehrstellige Junktoren durch Äquivalenzumformungen her. Verwenden Sie dabei nur die Basisaxiome, die De Morgansche Regel (demo) für zweistellige Junktoren, sowie die Regeln zum Umschreiben für mehrstellige Junktoren. Kommentieren Sie dabei jeden Schritt nach den hier gemachten Vorgaben und geben dabei insbesondere die verwendeten Regeln und Substitution an.
Tipp: Leiten Sie die Äquivalen induktiv her.