Introduction to equational logic

Equational propositional logic E is a product of researchers in the field of the formal development of algorithms. (Click here to see a short history.) E is sound and complete. The emphasis in proofs is on substitution of equals for equals, instead of modus ponens. Equality, or equivalence, assumes an important role instead of being a bit player, as in most propositional logics.

In our notation, b = c denotes equality, for b and c of the same type, while b == c, or equivalence, is defined only for b and c of type boolean. For b and c of type boolean, b = c and b == c have the same meaning.

One reason for having two symbols for equality over the booleans is that equality = is usually viewed as being conjunctional:

    b = c = d is an
    abbreviation for b = c /\ c = d
while b == c can be used associatively, which is of great importance for us:
    b == c == d is equal to b == (c == d) and to (b == c) == d.

Below is a typical proof in equational logic. The line numbers are present only for later discussion. This example is chosen because it is simple but shows all aspects of the formal proof system (as discussed later). The theorem numbers refer to theorems of A Logical Approach to Discrete Math. Here, we use "~" for "not". Associativity and symmetry of operators are treated transparently, without mention; this results in a large reduction in the number of theorems to be presented and simplifies manipulation. Finally, note that the style is just a formalization of the style of calculation used in high school algebra, and indeed by many scientists in their work --that is why the style is so useful. Return to table of contents

Here is a proof of ~p == p == false.

    (0)     ~p == p == false
(1) = < (3.9), ~(p == q) == ~p == q, with q:= p >
(2) ~(p == p) == false
(3) = < Identity of == (3.9), with q:= p >
(4) ~true == false --(3.8)

Inference rules of equational logic

Here are the four inference rules of logic E. (P[x:= E] denotes textual substitution of expression E for variable x in expression P):

Explanation of proof format

We explain how the four inference rules are used in proofs, using the proof of ~p == p == false.

    (0)     ~p == p == false
(1) = < (3.9), ~(p == q) == ~p == q, with q:= p >
(2) ~(p == p) == false
(3) = < Identity of == (3.9), with q:= p >
(4) ~true == false --(3.8)
First, lines (0)-(2) show a use of inference rule Leibniz:
 (0) = (2)
is the conclusion of Leibniz, and its premise ~(p == p) == ~p == p is given on line (1). In the same way, the equality on lines (2)-(4) are substantiated using Leibniz.

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

  (~(p == q) == ~p == q)[p:=q]
This shows how inference rule Substitution is used within hints.

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

Finally, note that line (4), ~true == false, is a theorem, as indicated by the hint to its right. Hence, by inference rule Equanimity, we conclude that line (0) is also a theorem. And (0) is what we wanted to prove.

This proof format has several advantages.

Return to table of contents