Equational Logic

For the purpose of describing the underpinnings of Eqthy, this document gives some information about equational logic.

Definition

The rules of inference of equational logic are:

• Reflexivity (A=A)
• Symmetry (if A=B then B=A)
• Transitivity (if A=B and B=C then A=C)
• Substitution (if x(A)=y(A) then x(B)=y(B))
• Congruence (if A=B then x(A)=x(B))

TODO: state those more formally

Notes

It took me a relatively long time to wrap my head around equational logic, so I will provide some notes on it here, and links to resources.

I would put it like this: Equational logic is the deductive aspect of universal algebra. It provides the "syntax" where the algebraic structure provides the "semantics".

By itself, it captures only the idea of equating things:

• Equation is a relation which is reflexive, symmetric, and transitive;
• In the manner of elementary algebra, "equals may always be replaced by equals".

But by itself, it cannot prove many theorems of interest. To do that, it needs to be supplemented by extra axioms stipulating exactly which things should, for the sake of argument, be considered equal. These axioms describe an algebraic structure. When the extra axioms are put together with equational logic, this is said to be the equational theory of the structure.

For example, the axioms for a group are:

• Associativity: (x * y) * z = x * (y * z)
• Existence of an Identity Element: x * e = e * x = e
• Existence of Inverse Elements: x * x^-1 = x^-1 * x = e

In the statement of each of these axioms, the variables are implicitly universally quantified. This is standard practice.

The following sections list some of the resources that I banged my head against repeatedly while trying to grasp these concepts.

📝 Wikipedia

As of this writing, Equational logic (Wikipedia) does not contain a very clear explanation. This is because it focuses on a particular equational logic, E, from the second edition of the book "A Logical Approach to Discrete Math" by David Gries and Fred Schneider. While it is a very interesting book (the 1st edition is borrowable from archive.org)), its presentation of equational logic is somewhat unorthodox:

• The axiom they call Leibniz most other sources call Congruence, and some sources describe it in a different fashion. (The book explains how these two descriptions are equivalent.)
• The axiom they call Equanimity is not a part of the equational logic proper, rather, it exists to support the equational theory of equality that E is undergirding, and to bridge it to the equational logic. (If you have an equational logic supporting a different equational theory, for example the equational theory of groups, you don't need Equanimity.)
• They don't have Reflexivity and Symmetry as axioms, but most other sources do. (These are instead axioms of their equational theory of equality, which they can "lift up" to the equational level using Equanimity.)

📝 Wolfram MathWorld

As of this writing, Equational Logic (Wolfram MathWorld) provides a more orthodox, but rather terse, exposition of equational logic.

Its Axiom 4 is often called Congruence elsewhere in the literature, and is equivalent to Gries and Schneider's Leibniz rule; and its Axiom 5 is often called Substitution or Replacement elsewhere.

📝 Dynamic Logic

The book "Dynamic Logic" by David Harel, Dexter Kozen, and Jerzy Tiuryn, which can be borrowed from archive.org, contains a section on Equational Logic (section 3.3), which serves as a very good introduction.

📝 Papers by George F. McNulty

Professor George F. McNulty of USC has written two excellent resources on equational logic:

• Field Guide to Equational Logic (1992)
• Equational Logic course notes (Spring 2017)

These are both somewhat denser than the encyclopedic entries above, and cover the connection between equational logic and universal algebra in more depth, as well as results about equational logic as an object of study in itself.

The course notes have a few highlights definitely worth mentioning here:

• p.13: A stepwise equational proof of a theorem of ring theory
• p.21: Birkhoff's axioms for equational logic (basically the same as those on Wolfram MathWorld)
• also p.21: Tarski's axioms (a more minimal set of axioms; I'm not sure how they work yet)

The field guide lists many results in equational logic, but the most interesting to me is section 6, which describes Tarski's relation algebra and how formulae of first-order logic of up to 3 variables (but no more!) may be translated to it.

"Equational Reasoning"

The phrase "equational reasoning" refers to informally using an equational theory to determine the meaning of (usually) a fragment of a program in a programming language, which is (usually) referentially transparent.

TODO: Add reference to an article that illustrates this

"Modulo an Equational Theory"

The phrase "modulo an equational theory" refers to automatically treating two terms as equal if there is a proof of their equality in an equational theory. This is sometimes employed in theorem provers, etc. to reduce the amount of trivial proof work that is needed to show a result, especially when it comes to "standard" equational axioms such as associativity and commutivity. Instead of going through all the steps to show that a.(b.(c.d)) = ((a.b).c).d (where . is associative), the two terms are automatically considered equal.

TODO: Add reference to a tool that implements this (egg?)