François G. Dorais

Research in Logic and Foundations of Mathematics

HoTT Math 2: More on equational logic

Last time, I promised we would look at fields. I have to delay this by one or two installments of HoTT Math since there is so much to say and I am struggling to keep these short. This edition of HoTT Math is a continuation of the first. The main lesson of HoTT Math 1 was that equational logic still works, provided you’re careful enough. As I was working through some algebra, I realized that I should have been more precise and nuanced. To make things more precise, I will briefly recall some basic universal algebra and then I will talk a little about Birkhoff’s soundness and completeness theorem for equational logic.

A signature is a sequence of sets indexed by natural numbers. The elements of the set are intended to be symbols for -ary operations (-ary operations are simply constants). For example, the signature for rings can be thought as

It is generally assumed that the sets are mutually disjoint so that each symbol has a definite arity. In the end, only the cardinality of the sets matters since the particular symbols used for the operations is mostly a matter of taste.

The logic of universal algebra is equational logic. The symbols from the signature can be strung together to form terms. In addition to the symbols from , we need an infinite set of variable symbols. Formally, terms are defined inductively using the two rules:

Equational logic deals with identities of the form where and are terms. The rules for equational logic are reflexivity, symmetry, transitivity

together with substitution and replacement

where denotes the act of replacing every occurrence of the variable symbol with the term . We write to signify that the identity follows using a combination of these rules from the identities in .

An algebra (with signature ) is a type together with an interpretation

If is a symbol for an -ary operation in , then the interpretation is

These interpretations can be used to evaluate any term starting from a variable assignment in the usual recursive manner:

The satisfaction relation for the algebra and the identity is then the type

If the carrier is a set then each identity type has at most one element and hence is a proposition with the usual meaning. In the general case, can carry substantial path information.

The fact that equational logic is sound and complete for the semantics is called Birkhoff’s Theorem:

Clasically, the right hand side means that every algebra with signature , whose carrier is a set, that satisfies all equations in also satisfies . In HoTT, this translates to the type

where the outer product is over all set-based algebras with signature . An alternate interpretation is

where the outer product is over algebras with signature based on any type. Consequently there are two possible ways to interpret Birkhoff’s Theorem in HoTT!

The first is closest to the classical version:

Weak Birkhoff Theorem. is equivalent to .

The vertical lines indicate that one should take the propositional truncation of (§3.7). Indeed, when translated into HoTT, is the type of all proofs of from in equational logic. The propositional truncation agglomerates all these proofs into one and simply asserts the unqualified existence of such a proof. This is necessary since the right hand side is a proposition so the backward implication, without propositional truncation, would amount to a canonical choice of proof with basically no information.

On the other hand, is much more expressive because of all the possible identity paths. With all that information on hand, it is not so unlikely that we could reconstruct a proof. This suggests another interpretation of Birkhoff’s Theorem:

Strong Birkhoff Theorem. is equivalent to .

As I stated it just now, this is unlikely to be true. However, I suspect it becomes true with some tweaking of to only allow proofs that are normalized in some sense or to formally identify proofs that are trivial variations of each other. I haven’t had much time to think about this so I’ll leave it as an open conjecture for now and hope that I can come back to it later…

The soundness part (forward implication) of both forms are true. Last time, I emphasized the usefulness of the weak soundness theorem but I forgot to talk about substitution and replacement! We did talk about how paths could be reversed and composed to get symmetry and transitivity; details are in §2.1 of the book. Since I think it’s important to know what goes on behind the scenes, let’s talk about the remaining two rules. Unfortunately, and this explains the earlier omission, neither is particularly pleasant.

Substitution works exactly as you expect. An element is a function that maps each variable assignment to a path . Given a term and a variable , the corresponding element of is the composition of with the function that sends each variable assignment to the assignment where all values stay the same except that the value of is changed to . Verifying that the result really is an element of is a tedious computation which is best performed under a rug.

The trick behind replacement is revealed in §2.2: functions are functors. The identity types give each type a higher groupoid structure and functions act functorially in the sense that with any comes with more functions which translate paths into paths . The details for soundness of the replacement rule are gory but they are essentially the same as in the classical proof. There is some work needed to single out the variable and interpret the term as a function where all other variables are fixed. Then, can be used to transform paths into paths . Thus, we obtain

Since each rule of equational logic is sound, we therefore have the strong soundness . To get weak soundness, we compose this with the obvious implication and we conclude that from the fact that is a proposition. The completenesss part of Birkhoff’s theorem uses syntactic algebras and HoTT has a really neat way to construct these that we will talk about in a later HoTT Math post.

In conclusion, equational logic works just fine in HoTT. In general, because of proof relevance, it is best to keep track of the equational proofs in order to keep track of the identity paths. The strong soundness map

guarantees that equational proofs will lead to identities, but different proofs can lead to different identity paths! When the carrier is a set, less care is necessary, the weak soundness map

shows that the mere existence of an equational proof leads to the desired identities. This is exactly how algebra and equational logic are used classically.

CC0 Originally posted on by François G. Dorais. To the extent possible under law, François G. Dorais has waived all copyright and neigboring rights to this work.