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").^[1]

The terms of equational logic are built up from variables and constants using function symbols (or operations).

Here are the four inference rules of logic. ${\textstyle P[x:=E]}${\textstyle P[x:=E]} denotes textual substitution of expression ${\textstyle E}${\textstyle E} for variable ${\textstyle x}${\textstyle x} in expression ${\textstyle P}${\textstyle P}. Next, ${\textstyle b=c}${\textstyle b=c} denotes equality, for ${\textstyle b}${\textstyle b} and ${\textstyle c}${\textstyle c} of the same type, while ${\textstyle b\equiv c}${\textstyle b\equiv c}, or equivalence, is defined only for ${\textstyle b}${\textstyle b} and ${\textstyle c}${\textstyle c} of type boolean. For ${\textstyle b}${\textstyle b} and ${\textstyle c}${\textstyle c} of type boolean, ${\textstyle b=c}${\textstyle b=c} and ${\textstyle b\equiv c}${\textstyle b\equiv c} have the same meaning.

^[2]

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

$${\displaystyle {\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}}}$${\displaystyle {\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 ${\textstyle (0)}${\textstyle (0)}–${\textstyle (2)}${\textstyle (2)} show a use of inference rule Leibniz:

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

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

The "hint" on line ${\textstyle (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 ${\textstyle (3.9)}${\textstyle (3.9)} with the substitution ${\textstyle p:=q}${\textstyle p:=q}, i.e.

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

This shows how inference rule Substitution is used within hints.

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

Finally, note that line ${\textstyle (4)}${\textstyle (4)}, ${\textstyle \lnot \top \equiv \bot }${\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 ${\textstyle (0)}${\textstyle (0)} is also a theorem. And ${\textstyle (0)}${\textstyle (0)} is what we wanted to prove.^[2]

• Theory of pure equality

• Sakharov, Alex. "Equational Logic." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein.

• Mathematical logic

• Webarchive template wayback links
• Articles with short description
• Short description matches Wikidata
• All Wikipedia articles needing clarification
• Wikipedia articles needing clarification from November 2021