Laws of propositional logic

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.