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).

Syllogism

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

Substitution	If ${\textstyle P}$  is a theorem, then so is ${\textstyle P[x:=E]}$ .	$${\displaystyle \vdash P\qquad \rightarrow \qquad \vdash P[x:=E]}$$
Leibniz	If ${\textstyle P=Q}$  is a theorem, then so is ${\textstyle E[x:=P]=E[x:=Q]}$ .	$${\displaystyle \vdash P=Q\qquad \rightarrow \qquad \vdash E[x:=P]=E[x:=Q]}$$
Transitivity	If ${\textstyle P=Q}$  and ${\textstyle Q=R}$  are theorems, then so is ${\textstyle P=R}$ .	$${\displaystyle \vdash P=Q,\;\vdash Q=R\qquad \rightarrow \qquad \vdash P=R}$$
Equanimity	If ${\textstyle P}$  and ${\textstyle P\equiv Q}$  are theorems, then so is ${\textstyle Q}$ .	$${\displaystyle \vdash P,\;\vdash P\equiv Q\qquad \rightarrow \qquad \vdash Q}$$

^[2]

Proof

We explain how the four inference rules are used in proofs, using the proof of ${\textstyle \lnot p\equiv p\equiv \bot }$ ^[clarify]. 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.^[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}}}$$ 

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

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

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

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

$${\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)}$  and ${\textstyle (2)=(4)}$ , we conclude by inference rule Transitivity that ${\textstyle (0)=(4)}$ . This shows how Transitivity is used.

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

See also

• Theory of pure equality

References

1. equational logic. (n.d.). The Free On-line Dictionary of Computing. Retrieved October 24, 2011, from Dictionary.com website: http://dictionary.reference.com/browse/equational+logic
2. Gries, D. (2010). Introduction to equational logic . Retrieved from https://www.cs.cornell.edu/home/gries/Logic/Equational.html Archived 2019-09-23 at the Wayback Machine

External links

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