Equational logic

Proof

We explain how the four inference rules are used in proofs, using the proof of $\mathrm{\neg }p\equiv p\equiv \mathrm{\perp }$. The logic symbols $\mathrm{\top }$ and $\mathrm{\perp }$ indicate "true" and "false," respectively, and $\mathrm{\neg }$ indicates "not." The theorem numbers refer to theorems of A Logical Approach to Discrete Math.

$${\displaystyle \begin{array}{lcl}(0)& & \mathrm{\neg }p\equiv p\equiv \mathrm{\perp }\\ (1)& =& ⟨(3.9),\mathrm{\neg }(p\equiv q)\equiv \mathrm{\neg }p\equiv q,\text{with}q:=p⟩\\ (2)& & \mathrm{\neg }(p\equiv p)\equiv \mathrm{\perp }\\ (3)& =& ⟨\text{Identity of}\equiv (3.9),\text{with}q:=p⟩\\ (4)& & \mathrm{\neg }\mathrm{\top }\equiv \mathrm{\perp }& (3.8)\end{array}}$$

First, lines $(0)$–$(2)$ show a use of inference rule Leibniz:

$${\displaystyle (0)=(2)}$$

is the conclusion of Leibniz, and its premise $\mathrm{\neg }(p\equiv p)\equiv \mathrm{\neg }p\equiv p$ is given on line $(1)$. In the same way, the equality on lines $(2)$–$(4)$ are substantiated using Leibniz.

The "hint" on line $(1)$ is supposed to give a premise of Leibniz, showing what substitution of equals for equals is being used. This premise is theorem $(3.9)$ with the substitution $p:=q$, i.e.

$${\displaystyle (\mathrm{\neg }(p\equiv q)\equiv \mathrm{\neg }p\equiv q)[p:=q]}$$

This shows how inference rule Substitution is used within hints.

From $(0)=(2)$ and $(2)=(4)$, we conclude by inference rule Transitivity that $(0)=(4)$. This shows how Transitivity is used.

Finally, note that line $(4)$, $\mathrm{\neg }\mathrm{\top }\equiv \mathrm{\perp }$, is a theorem, as indicated by the hint to its right. Hence, by inference rule Equanimity, we conclude that line $(0)$ is also a theorem. And $(0)$ is what we wanted to prove.