Laws of propositional logic

From Learning Logic for Computer Science

The algebraic properties of the boolean functions give rise to equivalences between propositional formulas. They are called laws when they are fundamental.

Example We have $$\text{and}(b_0, b_1) = \text{and}(b_1, b_0)$$ for all $b_0, b_1 \in \{0,1\}$. From this, we can conclude $$X_0 \wedge X_1 \SemEquiv X_1 \wedge X_0\enspace$$ as follows. Let $\beta$ be any variable assignment. Then \begin{align} [ [X_0 \wedge X_1] ]_\beta & = \text{and}(\llbracket X_0\rrbracket_\beta, \llbracket X_1\rrbracket_\beta) && \text{semantics of $\wedge$}\\ & = \text{and}(\llbracket X_1\rrbracket_\beta, \llbracket X_0\rrbracket_\beta) && \text{above property of and}\\ & = \llbracket X_1 \wedge X_0\rrbracket_\beta && \text{semantics of $\wedge$} \enspace. \end{align}

The same reasoning can be applied to formulas $\varphi$ and $\psi$ instead of $X_0$ and $X_1$, respectively. So we obtain $$\varphi \wedge \psi \SemEquiv \psi \wedge \varphi$$ for all $\varphi, \psi \in F_\text{PL}$. This is called "law of commutativity".

List of laws of propositional logic

A list of laws of propositional logic, classified and named accordingly, follows.

Base axioms (or laws)

All equivalences between propositional formulas only involving $\wedge$, $\vee$, $\neg$, $\top$ and $\bot$ follow from the following eight laws. None of these axioms is indispensable in the sense that is does not follow from the other ones.

Commutativity (comm) \begin{aligned} X_0 \vee X_1 & \SemEquiv X_1 \vee X_0 & X_0 \wedge X_1 & \SemEquiv X_1 \wedge X_0 \end{aligned}

Distributivity (dist) \begin{aligned} (X_0 \wedge X_1) \vee X_2 & \SemEquiv (X_0 \vee X_2) \wedge (X_1 \vee X_2) & (X_0 \vee X_1) \wedge X_2 & \SemEquiv (X_0 \wedge X_2) \vee (X_1 \wedge X_2) \end{aligned}

Identity (id) \begin{aligned} X_0 \vee \bot & \SemEquiv X_0 & X_0 \wedge \top & \SemEquiv X_0 \end{aligned}

Complementarity (comp) \begin{aligned} X_0 \wedge \neg X_0 & \SemEquiv \bot & X_0 \vee \neg X_0 & \SemEquiv \top \end{aligned}

Important derived laws

Associativity (ass) \begin{aligned} (X_0 \wedge X_1) \wedge X_2 & \SemEquiv X_0 \wedge (X_1 \wedge X_2) & (X_0 \vee X_1) \vee X_2 & \SemEquiv X_0 \vee (X_1 \vee X_2) \end{aligned}

Annihilator (ann) \begin{aligned} X_0 \wedge \bot & \SemEquiv \bot & X_0 \vee \top & \SemEquiv \top \end{aligned}

Double negation (done) \begin{aligned} \neg \neg X_0 \SemEquiv X_0 \end{aligned}

De Morgan (demo) \begin{aligned} \neg (X_0 \wedge X_1) & \SemEquiv \neg X_0 \vee \neg X_1 & \neg (X_0 \vee X_1) & \SemEquiv \neg X_0 \wedge \neg X_1 \end{aligned}

Duality (dual) \begin{aligned} \neg \bot & \SemEquiv \top & \neg \top & \SemEquiv \bot \end{aligned}

Absorption (abs) \begin{aligned} X_0 \wedge (X_0 \vee X_1) & \SemEquiv X_0 & X_0 \vee (X_0 \wedge X_1) & \SemEquiv X_0 \end{aligned}

Idempotence (Idem) \begin{aligned} X_0 \vee X_0 & \SemEquiv X_0 & X_0 \wedge X_0 & \SemEquiv X_0 \end{aligned}

Contraposition (cont) \begin{aligned} X_0 \rightarrow X_1 \SemEquiv \neg X_1 \rightarrow \neg X_0 \end{aligned}

Laws for rewriting other connectives (rewrite rules)

Conditional and biconditional (rew$\rightarrow$, rew$\leftrightarrow$) \begin{aligned} X_0 \rightarrow X_1 & \SemEquiv \neg X_0 \vee X_1 & X_0 \leftrightarrow X_1 & \SemEquiv (\neg X_0 \vee X_1) \wedge (X_0 \vee \neg X_1) \end{aligned}

Nand and Nor (rew$\bar\land$, rew$\bar\lor$) \begin{aligned} X_0 \mathrel{\bar\wedge} X_1 & \SemEquiv \neg (X_0 \wedge X_1) & X_0 \mathrel{\bar\vee} X_1 & \SemEquiv \neg (X_0 \vee X_1) \end{aligned}

Exclusive or (rew$\not\leftrightarrow$, rew$\dot\vee$, rew$\oplus$) \begin{aligned} X_0 \not\leftrightarrow X_1 & \SemEquiv (X_0 \wedge \neg X_1) \vee (\neg X_0 \wedge X_1)\\ X_0 \dot\vee X_1 & \SemEquiv (X_0 \wedge \neg X_1) \vee (\neg X_0 \wedge X_1)\\ X_0 \oplus X_1 & \SemEquiv (X_0 \wedge \neg X_1) \vee (\neg X_0 \wedge X_1) \end{aligned}

Connectives with multiple arities (rew$\bigwedge$, rew$\bigvee$, rew$\dot{\bigvee}$, rew$\bigoplus$) \begin{aligned} \bigwedge _ {i < n} X _ i & \SemEquiv (\dots ((X _ 0 \wedge X_1) \wedge X_2) \dots \wedge X _ {n-1}) \\ \bigvee _ {i < n} X _ i & \SemEquiv (\dots ((X _ 0 \vee X_1) \vee X_2) \dots \vee X _ {n-1}) \\ \dot{\bigvee} _ {i < n} X _ i & \SemEquiv \bigvee_{i<n} X_i \wedge \bigwedge_{i<n} \bigwedge_{j<i} (\neg X_i \vee \neg X_j)\\ \bigoplus _ {i < n} X _ i & \SemEquiv (\dots ((X _ 0 \oplus X_1) \oplus X_2) \dots \oplus X _ {n-1}) \end{aligned} In these laws, $n \geq 2$. For $n = 0$ and $n = 1$, there are simple ways to rewrite the four connectives. \begin{aligned} \bigwedge(X_0) & \SemEquiv X_0 & \bigwedge() \SemEquiv \top \\ \bigvee(X_0) & \SemEquiv X_0 & \bigvee() \SemEquiv \bot\\ \dot{\bigvee}(X_0) & \SemEquiv X_0 & \dot\bigvee() \SemEquiv \bot\\ \bigoplus(X_0) & \SemEquiv X_0 & \bigoplus() \SemEquiv \bot \end{aligned}

Laws with substitution involved

Case distinction (cd$\vee$, cd$\wedge$) \begin{aligned} \varphi \; & \SemEquiv (X_i \wedge \varphi\{X_i \mapsto \top\}) \vee (\neg X_i \wedge \varphi\{X_i \mapsto \bot\})\\ \varphi \; & \SemEquiv (X_i \vee \varphi\{X_i \mapsto \bot\}) \wedge (\neg X_i \vee \varphi\{X_i \mapsto \top\}) \end{aligned} This law holds for every $i \in \mathbf N$.

Substitution principle

Often, a law such as (ass$\wedge$) is not stated as \begin{aligned} (X_0 \wedge X_1) \wedge X_2 & \SemEquiv X_0 \wedge (X_1 \wedge X_2) \end{aligned} but rather as \begin{aligned} (\varphi_0 \wedge \varphi_1) \wedge \varphi_2 & \SemEquiv \varphi_0 \wedge (\varphi_1 \wedge \varphi_2) \enspace, \end{aligned} where, in addition, it is mentioned that this holds for all choices of $\varphi_0, \varphi_1, \varphi_2$ of propositional formulas.

That this is true is an immediate consequence of the substitution lemma.