# Equational logic

First-order equational logic consists of quantifier-free terms of ordinary first-order logic, with equality as the only predicate symbol. The model theory of this logic was developed into universal algebra by Birkhoff, Grätzer, and Cohn. It was later made into a branch of category theory by Lawvere ("algebraic theories").
The terms of equational logic are built up from variables and constants using function symbols (or operations).

## Syllogism

Here are the four inference rules of logic. P[x:=E]{\textstyle P[x:=E]} denotes textual substitution of expression E{\textstyle E} for variable x{\textstyle x} in expression P{\textstyle P}. Next, b=c{\textstyle b=c} denotes equality, for b{\textstyle b} and c{\textstyle c} of the same type, while b≡c{\textstyle b\equiv c}, or equivalence, is defined only for b{\textstyle b} and c{\textstyle c} of type boolean. For b{\textstyle b} and c{\textstyle c} of type boolean, b=c{\textstyle b=c} and b≡c{\textstyle b\equiv c} have the same meaning.
| Substitution | If P{\textstyle P} is a theorem, then so is P[x:=E]{\textstyle P[x:=E]}. | $\vdash P\qquad \rightarrow \qquad \vdash P[x:=E]$ |
| Leibniz | If P=Q{\textstyle P=Q} is a theorem, then so is E[x:=P]=E[x:=Q]{\textstyle E[x:=P]=E[x:=Q]}. | $\vdash P=Q\qquad \rightarrow \qquad \vdash E[x:=P]=E[x:=Q]$ |
| Transitivity | If P=Q{\textstyle P=Q} and Q=R{\textstyle Q=R} are theorems, then so is P=R{\textstyle P=R}. | $\vdash P=Q,\;\vdash Q=R\qquad \rightarrow \qquad \vdash P=R$ |
| Equanimity | If P{\textstyle P} and P≡Q{\textstyle P\equiv Q} are theorems, then so is Q{\textstyle Q}. | $\vdash P,\;\vdash P\equiv Q\qquad \rightarrow \qquad \vdash Q$ |

## Proof

We explain how the four inference rules are used in proofs, using the proof of ¬p≡p≡⊥{\textstyle \lnot p\equiv p\equiv \bot }. The logic symbols ⊤{\textstyle \top } and ⊥{\textstyle \bot } indicate "true" and "false," respectively, and ¬{\textstyle \lnot } indicates "not." The theorem numbers refer to theorems of A Logical Approach to Discrete Math.
${\begin{array}{lcl}(0)&&\lnot p\equiv p\equiv \bot \\(1)&=&\quad \left\langle \;(3.9),\;\lnot (p\equiv q)\equiv \lnot p\equiv q,\;{\text{with}}\ q:=p\;\right\rangle \\(2)&&\lnot (p\equiv p)\equiv \bot \\(3)&=&\quad \left\langle \;{\text{Identity of}}\ \equiv (3.9),\;{\text{with}}\ q:=p\;\right\rangle \\(4)&&\lnot \top \equiv \bot &(3.8)\end{array}}$
First, lines (0){\textstyle (0)}– (2){\textstyle (2)} show a use of inference rule Leibniz:
$(0)=(2)$
is the conclusion of Leibniz, and its premise ¬(p≡p)≡¬p≡p{\textstyle \lnot (p\equiv p)\equiv \lnot p\equiv p} is given on line (1){\textstyle (1)}. In the same way, the equality on lines (2){\textstyle (2)}– (4){\textstyle (4)} are substantiated using Leibniz.
The "hint" on line (1){\textstyle (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){\textstyle (3.9)} with the substitution p:=q{\textstyle p:=q}, i.e.
$(\lnot (p\equiv q)\equiv \lnot p\equiv q)[p:=q]$
This shows how inference rule Substitution is used within hints.
From (0)=(2){\textstyle (0)=(2)} and (2)=(4){\textstyle (2)=(4)}, we conclude by inference rule Transitivity that (0)=(4){\textstyle (0)=(4)}. This shows how Transitivity is used.
Finally, note that line (4){\textstyle (4)}, ¬⊤≡⊥{\textstyle \lnot \top \equiv \bot }, is a theorem, as indicated by the hint to its right. Hence, by inference rule Equanimity, we conclude that line (0){\textstyle (0)} is also a theorem. And (0){\textstyle (0)} is what we wanted to prove.