Lecture
First-order equational logic (equivalential logic) consists of the quantifier-free terms of ordinary first-order logic, where the only predicate symbol is equality.
The model theory of this logic was developed into universal algebra by Birkhoff, Grätzer, and Cohn.
Later, it was transformed by Lawvere into a branch of category theory («algebraic theories»).
Terms of equational logic are built from variables and constants using functional symbols (or operations).
Here are the four inference rules of the logic.
denotes the textual substitution of the expression 
for the variable x in the expression 
. Next, 
denotes equality, since 
and 
are of the same type, while 
, or equivalence, is defined only for and of type boolean. For and of type boolean, and have the same meaning.
| Substitution | If is a theorem, then so is . |
 |
|---|---|---|
| Leibniz | If  is a theorem, then so is  . |
 |
| Transitivity | If and  are theorems, then so is  . |
 |
| Equanimity | If and  are theorems, then so is  . |
 |
We explain how the four inference rules are used in proofs, using the proof of 
.
The logical symbols 
and 
denote «true» and «false» respectively, and ¬ means «not».
The theorem numbers refer to theorems from the book «A Logical Approach to Discrete Math».
First, lines (0)–(2) show the use of the Leibniz inference rule: (0)=(2)
is the Leibniz conclusion, and its premise 
is given on line (1).
In the same way, the equality on lines (2)–(4) is justified using Leibniz.
The «hint» on line (1) is assumed to be the Leibniz premise, showing which substitution of equals for equals is used. This premise is theorem (3.9) with the substitution 
, that is
Here it is shown how the «Substitution» inference rule is used in hints.
From (0)=(2) and (2)=(4), we conclude by the Transitivity inference rule that (0)=(4). This shows how transitivity is used.
Finally, note that this line (4), 
, is a theorem, as indicated in the hint on the right.
Therefore, by the «Equanimity» inference rule we conclude that line (0) is also a theorem. And (0) is what we wanted to prove
Comments