Equational logic studies which equalities follow from stated algebraic laws. It gives precise rules for replacing equals by equals, substituting expressions for variables and joining small justified steps into a proof. Its practical value is knowing when two expressions may safely be treated as interchangeable—and recognising when a familiar-looking simplification assumes a law you have not been given.
The gold standard is an equality with a clear contract: the operation symbols, the permitted interpretations, the assumptions and a checkable derivation. This guide develops that contract through original calculations with monoids, involutions and small finite operation tables. We use ordinary single-sorted algebras with nonempty carriers and total operations of finite arity unless a later section explicitly discusses changing that setting.
Use the Gold Standard collection and How X Works hub for the wider map. Universal Algebra explains shared algebraic constructions; Term Rewriting examines directed computation. Here the central task is proving or refuting an equational consequence. The Education guide supplies the learning test: can you rebuild the argument when its assumptions change?
Choose your equational logic route
Chapters 1–3: Read and justify equalities
Chapters 4–6: Prove and refute claims
Chapters 7–9: Understand the logical contract
Chapters 10–12: Compute and test transfer
Chapter index
Read and justify equalities · Chapters 1–3
1. State the language before manipulating the expression
Prove and refute claims · Chapters 4–6
4. Substitute uniformly rather than editing matching letters
5. Build an auditable proof in an idempotent monoid
6. Refute a proposed consequence with a complete small model
Understand the logical contract · Chapters 7–9
7. Understand what soundness and completeness promise
Compute and test transfer · Chapters 10–12
10. Solve a whole equational theory in a small special case
Diagnose and keep learning · Chapters 13–14
CHAPTER 1 OF 14 · Read and justify equalities
1. State the language before manipulating the expression
A symbol needs an arity and an interpretation
Consider a language with one binary operation symbol ⋆ and one constant symbol e. A term is built from variables, e and applications of ⋆ to two previously constructed terms. Thus x⋆e, (x⋆y)⋆z and e are terms. The expression ⋆x is incomplete in this language: the operation requires two inputs. A constant is an operation with no inputs, rather than a variable whose value may change with the assignment.
The symbols alone do not tell us that ⋆ is addition, multiplication or concatenation. An interpretation supplies a nonempty set A, an actual function A×A→A and a designated element interpreting e. On strings, ⋆ could mean concatenation and e the empty string. On nonnegative integers, ⋆ could mean addition and e zero. Both are legitimate interpretations, but their extra properties need not agree.
For example, addition of nonnegative integers is commutative. String concatenation is not: joining “red” to “blue” differs from joining “blue” to “red”. Writing the same abstract symbol for these operations helps us isolate laws they share without accidentally importing laws they do not share.
Syntax is not a value
The terms (x⋆e)⋆y and x⋆y are different pieces of syntax. They might nevertheless evaluate to the same element under every assignment in a suitable algebra. Equational logic explains that second kind of equality; it does not pretend that the two expression trees are literally identical.
Before beginning a proof, write three lines: the signature, the assumed identities and the proposed conclusion. If a later step introduces division, an inverse, a named constant or a new operation, check whether the signature actually permits it. The specialist discussion of term operations and fixed parameters explains why an available element is not automatically a named symbol in the language.
CHAPTER 2 OF 14 · Read and justify equalities
2. Distinguish an identity from an equation to solve
Variables in a law range over every permitted value
An identity such as x⋆e=x says that the two terms agree for every assignment of x in the algebra. It is not a request to find one convenient x. In the integers under ordinary addition, the equation x+2=5 has the solution x=3; it is not an identity in x. Confusing these tasks turns a successful substitution into an unjustified universal claim.
Let E be the three monoid laws: (x⋆y)⋆z=x⋆(y⋆z), e⋆x=x and x⋆e=x. The first is associativity, and the other two make e a two-sided identity. Saying that an algebra satisfies E means all three equations hold under every assignment of their variables. It does not mean merely that someone found one assignment satisfying all three simultaneously.
The notation E ⊨ s=t means that every algebra satisfying E also satisfies s=t. The notation E ⊢ s=t means that there is a formal derivation from E using the equational proof rules. One expression describes models; the other describes proofs. Their connection is a theorem, not a change in the meaning of the symbols.
Three claims with different evidence
For our monoid language, x⋆e=x is an assumption. The equation (x⋆e)⋆(e⋆y)=x⋆y is a consequence we can derive. The equation x⋆y=y⋆x is an additional proposed law that does not follow from the three monoid assumptions.
You can test commutativity in one algebra, prove it for a specific algebra, or ask whether all monoids satisfy it. These are different questions. A complete addition table for one finite monoid answers the first question thoroughly while leaving the third unresolved. Always place the quantifier in words beside the claim: “in this algebra”, “for every assignment”, or “in every model of these assumptions”. That small habit prevents large misunderstandings later.
CHAPTER 3 OF 14 · Read and justify equalities
3. Use the proof rules with explicit reasons
Equality can be transported through a term
The elementary calculus permits an assumed identity, reflexivity t=t, symmetry from s=t to t=s, and transitivity from s=t and t=u to s=u. It also permits uniform substitution of terms for variables and replacement of equal subterms within a larger term. These rules are presented in Burris and Sankappanavar, section II.14.
Replacement is often called congruence. If u=v, then u⋆w=v⋆w because the operation receives the same values in corresponding positions. Likewise w⋆u=w⋆v. Applying this repeatedly lets us replace an occurrence deep inside a term. No cancellation property is needed for this forward direction.
Here is a full small proof from the monoid laws. Start with (x⋆e)⋆(e⋆y). Replace the left subterm x⋆e by x using the right-identity law, leaving x⋆(e⋆y). Replace e⋆y by y using the left-identity law, giving x⋆y. Transitivity connects the starting term to the final term.
Keep the untouched context visible
The first step takes place in the context C[□]=□⋆(e⋆y). The second takes place in D[□]=x⋆□. A context is an expression with a distinguished hole. It records exactly which occurrence changes and which surrounding material remains fixed.
For a learner checking a proof, “simplify” is less informative than “right identity inside the left input of ⋆”. The latter tells another person how to reproduce the step. If a transformation cannot be explained with an assumption, a previously proved equality, a substitution and an occurrence, inspect it before continuing. A plausible final expression does not repair an invalid intermediate step.
CHAPTER 4 OF 14 · Prove and refute claims
4. Substitute uniformly rather than editing matching letters
One variable has one replacement in a substitution
Take associativity (x⋆y)⋆z=x⋆(y⋆z). Substitute x↦p⋆q, y↦e and z↦r. The result is ((p⋆q)⋆e)⋆r=(p⋆q)⋆(e⋆r). Applying the identity laws to both sides gives the same expression (p⋆q)⋆r. This is an instance of associativity, not a newly discovered numerical coincidence.
Now suppose the assumptions include idempotence x⋆x=x. Replacing x by p⋆q produces (p⋆q)⋆(p⋆q)=p⋆q. Replacing just the first occurrence of x by p and the second by q would produce p⋆q=p, which is not a uniform instance. Repeated occurrences are a constraint, not an invitation to choose replacements independently.
Substitution also differs from changing an element assignment in a model. Substitution changes formal terms. An assignment gives variables actual values when evaluating those terms. The two operations cooperate, but recording which one you are performing makes the proof easier to audit.
Simultaneous does not mean repeatedly applying the replacement
Let σ replace x by y and y by e. Applied simultaneously to x⋆y, it gives y⋆e. It does not immediately give e⋆e: the y introduced as the replacement for x is not replaced again during that same simultaneous application. A second application of σ would give e⋆e.
This matters when implementing a symbolic substitution routine. A textual replace-all operation can accidentally behave sequentially, changing material it just inserted. A safer conceptual procedure walks the original expression tree and returns the declared replacement whenever it reaches a variable leaf. Test it on x⋆y with this substitution: the correct one-pass answer is y⋆e. Also test repeated variables and nested terms; both expose bugs that single-letter examples conceal.
CHAPTER 5 OF 14 · Prove and refute claims
5. Build an auditable proof in an idempotent monoid
Derive a useful absorption of a repeated neighbour
Add x⋆x=x to the monoid laws. We want to prove (x⋆y)⋆(y⋆z)=x⋆(y⋆z). We do not assume commutativity. Begin by applying associativity to the outer combination: (x⋆y)⋆(y⋆z)=x⋆(y⋆(y⋆z)). Next apply associativity in the reverse direction inside the right input, obtaining x⋆((y⋆y)⋆z). Idempotence replaces y⋆y by y, giving x⋆(y⋆z).
The derivation uses three local transformations. It never swaps x and y, moves z across another factor or cancels a shared prefix. Its validity therefore extends to every monoid satisfying idempotence, including noncommutative ones. The neighbouring repetition of y is what makes the calculation work.
Try a tempting variation: can x⋆y⋆x be replaced by x⋆y using just these assumptions? Some idempotent monoids satisfy that extra law, but it is not one of the steps we have established here. The disciplined response is to seek a separate proof or countermodel, rather than treating similar typography as a theorem. A proof’s dependency list is part of its result.
Audit by removing an assumption
Remove idempotence and interpret ⋆ as addition on nonnegative integers with e=0. Take x=2, y=3 and z=5. The left side of our proposed equality evaluates to (2+3)+(3+5)=13; the right side evaluates to 2+(3+5)=10. Associativity and the identity laws still hold. The failed equality identifies exactly why the earlier idempotence step was necessary.
This is a useful way to test understanding. Ask which assumption a proof uses, then construct a permitted interpretation after removing that assumption. The answer should name both the broken step and a concrete failed calculation. A dependency audit is more revealing than memorising the final formula.
CHAPTER 6 OF 14 · Prove and refute claims
6. Refute a proposed consequence with a complete small model
A three-element monoid that is not commutative
Consider the carrier {e,a,b}. Let e act as an identity on both sides. For any left input a, define a⋆e=a, a⋆a=a and a⋆b=a. For left input b, define b⋆e=b, b⋆a=b and b⋆b=b. The remaining row is e⋆e=e, e⋆a=a and e⋆b=b. These nine entries specify the operation completely.
Every element is idempotent. Associativity can be checked across all 3³=27 triples, but a short argument explains all cases. If the first input is a or b, both parenthesisations return that first input. If the first input is e, both parenthesisations reduce to the product of the second and third inputs. Therefore this is an idempotent monoid.
Yet a⋆b=a and b⋆a=b, and a and b are distinct. Commutativity fails. This refutes the claim that associativity, a two-sided identity and idempotence together force commutativity. It also shows why checking only familiar numerical examples can make an invalid generalisation feel convincing.
Verify the assumptions before celebrating the counterexample
A countermodel has two jobs: satisfy every assumption and falsify the target. A nonassociative table would not refute a consequence of the monoid laws. A table with no identity would fail for the same reason. Record the entire table, the assumption checks and the specific variable assignment breaking the target.
This extends the school-level method in disproving a false algebraic rule with one counterexample. Here we choose an entire interpretation as well as the inputs. One valid countermodel is decisive; an unsuccessful search for a small countermodel is not a proof. Larger or infinite models may remain outside the search.
Resolve the tempting variation from chapter 5
We can now settle the earlier question about x⋆y⋆x=x⋆y. Use another operation on {e,a,b}: keep e as a two-sided identity, but let a product of two nonidentity elements return its right input. The rows, in column order e,a,b, are e,a,b for row e; a,a,b for row a; and b,a,b for row b.
This operation returns the last nonidentity element in a sequence, or e when every element is e. Consequently either parenthesisation of three inputs returns the same answer, proving associativity. Each element remains idempotent. However, with x=a and y=b, the product x⋆y is b while (x⋆y)⋆x is a. Thus the proposed identity fails even though every assumption of an idempotent monoid holds.
Compare this with the first table, whose product returns the first nonidentity element. That table happens to satisfy x⋆y⋆x=x⋆y, but the second does not. Both satisfy the repeated-neighbour identity proved in chapter 5. This paired construction demonstrates exactly why one friendly model cannot establish a consequence for an entire class. The proof travels to both models because it uses only their shared laws; the tempting shortcut does not.
CHAPTER 7 OF 14 · Understand the logical contract
7. Understand what soundness and completeness promise
A proof must preserve truth in every permitted interpretation
Soundness says that a derived identity is true in every model of the assumptions. The proof rules have a transparent reason: equality is reflexive, symmetric and transitive; actual functions return equal outputs for equal inputs; and a universally valid identity remains valid when its variables are replaced uniformly by terms.
Birkhoff’s completeness theorem supplies the converse: if an identity holds in every algebra satisfying E, it is derivable from E in equational logic. Andreas Abel’s formalisation establishes this connection in a many-sorted setting as well. The single-sorted statement used here is the classical case.
One way to understand the converse is to build an algebra of terms, identifying exactly the terms whose equality is derivable. Compatibility makes its operations well-defined, and substitution makes the assumptions valid under arbitrary assignments. If the target is not derivable, its two terms remain different in this algebra. That supplies a countermodel. This describes the proof’s mechanism, rather than an algorithm for constructing a small counterexample quickly.
Completeness is not a stopwatch
The theorem does not say that a proof is short, that a search program will find it promptly, or that every nonconsequence has a finite countermodel. It also does not say that all identities true in your favourite algebra follow from a weak list of assumptions. The word “every” refers to all models of that list.
Suppose you intend ordinary addition but specify only the monoid laws. Commutativity is true in the intended interpretation, yet false in other models of the specification. Failure to derive it is not a defect of completeness. The specification has admitted more models than your intended one. Repair the assumptions or narrow the claim explicitly; do not silently treat intention as an extra axiom.
CHAPTER 8 OF 14 · Understand the logical contract
8. Keep ground equalities separate from universal laws
Named constants do not behave like universally quantified variables
Let a,b,c,d be constant symbols and f a unary operation. Suppose the ground assumptions are a=b, f(b)=c and f(a)=d. “Ground” means that no variables occur. From a=b, congruence gives f(a)=f(b). Combining the other two equations by symmetry and transitivity yields d=c.
The six relevant terms are a, b, c, d, f(a) and f(b). Their forced equivalence classes are {a,b} and {c,d,f(a),f(b)}. A two-element model shows these two classes need not collapse: interpret a and b as 0, c and d as 1, and f as the constant function returning 1. All three premises hold and 0 differs from 1.
If we additionally require c≠d, the requirements become inconsistent. The proof d=c explains the conflict. This is a tiny example of equality reasoning that produces an explanation, not merely a yes/no answer.
Do not substitute into fixed names
The assumption a=b concerns two designated constants. It does not license replacing a and b independently by arbitrary terms to conclude x=y. Universal identities and ground facts have different roles even when both are printed with an equals sign.
Ground congruence closure is a useful computational special case. Tobias Nipkow’s equational logic course separates it from the general word problem and explains the finite subterm property used for finite ground inputs. The distinction matters when choosing an equality procedure: solving a finite ground problem does not automatically solve an arbitrary theory containing universally quantified equations.
For a complementary finite-algebra construction, see computing the congruence forced by a proposed identification. There the objects being merged are elements of a supplied algebra; here we have been tracking formal terms under stated premises.
CHAPTER 9 OF 14 · Understand the logical contract
9. Know why cancellation and reverse inference need more
Equal inputs force equal outputs; the converse can fail
From u=v we may infer f(u)=f(v). From f(u)=f(v), we cannot generally infer u=v. On {0,1}, let f return 0 for both inputs. Then f(0)=f(1), while 0≠1. The missing property is injectivity of f.
Similarly, x⋆y=x⋆z does not imply y=z in every monoid. On {0,1}, use maximum as ⋆ and 0 as the identity. With x=1, y=0 and z=1, both products equal 1, but y and z differ. This operation is associative, commutative and idempotent. None of those properties supplies cancellation.
This counterexample is particularly useful because the operation has several attractive algebraic laws. Adding more familiar adjectives to a structure does not guarantee the particular implication you need. Check the exact property supporting the proposed inference.
Conditional claims have a different logical shape
Cancellation is naturally expressed as an implication: if x⋆y=x⋆z, then y=z. That is not an unconditional identity between two terms. Conditional equational reasoning is an important extension, but its premises must remain visible. Treating the conclusion as an unconditional identity would change the theory drastically.
Division offers another warning. In ordinary real arithmetic, x/x=1 requires x≠0. Division is not a total real operation with its usual meaning. Our elementary setting assumed total operations, so importing this expression requires a revised contract: restrict the domain appropriately, use a suitable partial-operation framework, or explicitly define a different total operation. Those choices are mathematically different. The correct repair is to name the domain and the condition, not to hide the exceptional input in a footnote after using the rule.
CHAPTER 10 OF 14 · Compute and test transfer
10. Solve a whole equational theory in a small special case
An involution cancels in pairs
Take a signature containing only a unary operation f, with the single identity f(f(x))=x. There are no constant symbols. Every term therefore consists of a variable wrapped in some number of f applications. Write fⁿ(x) for n nested applications, with f⁰(x)=x.
Repeatedly remove two neighbouring f applications. A term with an even number reduces to its variable; one with an odd number reduces to f of that variable. For instance f⁷(x)=f⁵(x)=f³(x)=f(x), using three instances of the assumed equation inside contexts. Likewise f⁶(x)=x after three removals.
These calculations prove equality whenever two terms use the same variable and their exponents have the same parity. To show that this criterion is complete for this particular theory, we must also separate the other cases. Normal-looking answers alone would not establish that no additional equalities are possible.
Build one model that preserves the distinction
For a finite nonempty variable set V, use the carrier V×{0,1}. Define f(v,i)=(v,1−i), and assign variable v to (v,0). Applying f twice returns the original pair, so the model satisfies the assumption. A term fⁿ(v) evaluates to (v,n mod 2).
Different variables give different first coordinates; different parities give different second coordinates. Therefore terms outside our equality criterion can be separated by this model. With three variables p,q,r, the six resulting values are (p,0),(p,1),(q,0),(q,1),(r,0),(r,1).
We now have both halves: explicit proofs for matching cases and a countermodel for nonmatching cases. This is a complete decision method for this restricted signature and axiom. It is not a claim that all equational theories admit such a simple procedure. The absence of binary operations and constants is part of why the classification is so manageable.
CHAPTER 11 OF 14 · Compute and test transfer
11. Turn a specification into a reliable transformation
Preserve the observation that the application cares about
Imagine a service that combines lists of tasks. At the mathematical level, list concatenation is associative and the empty list is an identity. Rebracketing ((A⋆B)⋆C) as A⋆(B⋆C) preserves the resulting list. Swapping A and B generally does not. Deduplicating A⋆A to A also does not preserve the list when repeated tasks are meaningful.
Choose A=[inspect], B=[record] and C=[close]. Both parenthesisations produce [inspect,record,close]. The swapped expression B⋆A produces [record,inspect], and A⋆A produces [inspect,inspect]. An implementation that treats these transformations as interchangeable could alter the intended order or multiplicity of work.
If the application instead stores sets of completed task names and combines them by union, associativity, commutativity and idempotence all hold. Now duplicate removal and reordering preserve the set. This is not a contradiction. The representation and the observation have changed: a set records membership, while a list records order and repetition.
A mathematical model does not settle every implementation question
An equational proof about list values does not by itself establish equal running time, memory use, exception behaviour or external effects. If combining tasks also writes to a log or sends a request, the observations may include those effects. State which behaviour is being preserved before applying a mathematical equality to software.
For a practical review, select one proposed transformation and record its input domain, required laws and observable result. Then test a case with repeated elements, a case with different order and a boundary case involving the identity. These tests can expose a mismatch between the model and the implementation. They support the audit; they do not replace a general proof that the required laws hold.
CHAPTER 12 OF 14 · Compute and test transfer
12. Change the assumptions and rebuild the answer
Exercise: an involution that is also idempotent
Return to the unary language of chapter 10. Keep f(f(x))=x and add f(f(x))=f(x). What further identity follows? Can a two-element swap still be a model? How many distinct term classes remain over three variables p,q,r?
Work from the equations before reading the answer. Both assumptions have the same left side. Symmetry turns the first into x=f(f(x)); transitivity with the second gives x=f(x). Thus f is forced to be the identity function in every model. All terms based on one variable are now equal regardless of the number of f applications.
The two-element swap is excluded: at x=0, f(f(0))=0 but f(0)=1, so the new idempotence law fails. A three-element carrier with f the identity and p,q,r assigned distinct elements separates the three variables. Exactly three term classes remain, one for each variable. The added law has collapsed parity without collapsing distinct variables.
Exercise: idempotence alone
Now remove the involution law and keep only f(f(x))=f(x). Must f(x)=x follow? No. On {0,1}, let f be constantly 0. Then f(f(x))=0=f(x) for every x, but f(1)=0≠1. The earlier derivation needed both assumptions.
Compare the three theories carefully. Involution alone retains a parity distinction. Involution plus idempotence makes f the identity. Idempotence alone allows projections that send several elements to the same fixed point. Memorising the word “idempotent” does not supply these distinctions; deriving consequences and checking countermodels does.
As a further independent task, explain why every value f(x) is fixed by f under idempotence alone. The answer is exactly the axiom f(f(x))=f(x). It says something about values in the image of f, not that every element of the carrier lies in that image.
CHAPTER 13 OF 14 · Diagnose and keep learning
13. Diagnose common failures and questions
Is equational logic just ordinary algebra?
It formalises an important part of algebraic reasoning while making the underlying assumptions explicit. A school calculation may take the real-number laws for granted. Equational logic lets you ask which laws were actually needed and whether the derivation survives in a different algebra. It is especially useful when the operation symbol does not stand for ordinary numerical multiplication.
Does a successful simplifier prove that two different outputs are unequal?
Not automatically. A sound sequence of transformations proves equality between its input and output. To infer inequality from distinct final forms, you need a completeness guarantee for the chosen procedure and theory. Chapter 10 supplied its own separating-model argument. General rewriting requires additional analysis; follow the Term Rewriting guide for termination, confluence and normal forms.
Can equations alone force two constants to be different?
In our ordinary setting, any collection of unconditional equations has a one-element model: interpret every constant and every operation value as the sole element. Every equality then holds. To require a≠b you need an additional kind of constraint or a restricted class of structures. A theory can still have rich nontrivial models; the point is that unconditional equations alone do not exclude the one-element interpretation.
Does failure to find a proof establish nonconsequence?
No. It may reflect an incomplete method, a resource limit or an unsuccessful search. A verified countermodel establishes nonconsequence. A complete decision procedure can also establish it within its stated scope. Keep “not found”, “refuted” and “proved impossible by a complete method” separate in reports.
What should a correction record contain?
Save the first unjustified step, the missing assumption and a repaired argument or countermodel. For a nonuniform substitution, write the replacement map explicitly. For cancellation, test injectivity or the relevant cancellation law. For a false universal claim, supply a model satisfying all premises. This turns an error into a reusable diagnostic instead of merely replacing one answer with another.
CHAPTER 14 OF 14 · Diagnose and keep learning
14. Build a learning route from calculation to proof
Practise with two kinds of evidence
Begin with short chains using only identity and associativity. Name the law and the changed occurrence at every step. Then add one new axiom, such as idempotence, and mark the first step that genuinely needs it. After that, construct a small operation table that satisfies the old laws but defeats a proposed new one.
A productive exercise pair uses the same assumptions in two different ways. First prove (x⋆e)⋆(e⋆y)=x⋆y for every monoid. Then refute the assertion that every monoid is commutative using the three-element table in chapter 6. The first task builds a chain of reasons; the second builds a complete admissible interpretation. Together they explain both what the assumptions guarantee and what they leave open.
For computational practice, implement the nine-entry table and check all 27 associativity triples. Report the input domain and the exact properties tested. Separately implement unary-term normalisation by parity and compare it with evaluation in the six-element tagged model. These are small enough that a learner can independently inspect every result and explain why the algorithm agrees with the mathematics.
Continue into the relevant neighbouring subject
Use Universal Algebra to study the algebras themselves, their homomorphisms and quotients. Follow generated congruences when identifications force further identifications. Use fixed parameters and term operations when an expression quietly introduces a named value. These routes answer distinct questions that often meet in one proof.
For formal reference, consult A Course in Universal Algebra, section II.14 for equational deduction, Nipkow’s course materials for the boundary between general equational problems and computational special cases, and Abel’s formalised completeness proof for a machine-checked development. These sources support the formal framework; the finite tables, task-list case and transfer exercises above are teaching constructions developed here.
The final learning check is practical: given unfamiliar symbols, can you state the signature, identify the assumptions, justify a substitution, derive one consequence and build a countermodel to one tempting overclaim? That is a stronger achievement than recognising a familiar formula. It gives you a method for deciding what an equality genuinely permits.