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.
denotes textual substitution of expression
denotes equality, for
, or equivalence, is defined only for
of type boolean.
of type boolean,
[2] We explain how the four inference rules are used in proofs, using the proof of
The logic symbols
indicate "true" and "false," respectively, and
The theorem numbers refer to theorems of A Logical Approach to Discrete Math.
{\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}}}
show a use of inference rule Leibniz:
is the conclusion of Leibniz, and its premise
In the same way, the equality on lines
are substantiated using Leibniz.
The "hint" on line
is supposed to give a premise of Leibniz, showing what substitution of equals for equals is being used.
This premise is theorem
with the substitution
This shows how inference rule Substitution is used within hints.
, we conclude by inference rule Transitivity that
This shows how Transitivity is used.
Finally, note that line
, is a theorem, as indicated by the hint to its right.
Hence, by inference rule Equanimity, we conclude that line
is what we wanted to prove.