- Type Theory
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:
- Every variable symbol is a term.
- If are terms and is an element of , then is also a term.
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.
Toby Bartels wrote
So you can prove weak soundness and weak completeness (which you had better be able to do, since these are classical results), and these combine into weak equivalence (automatically, since we are dealing with mere propositions). Also, you can prove strong soundness, but strong equivalence (as you have stated) is probably not true.
Do you suspect that strong completeness is also false as you have stated it? Or do you think that strong completeness is also true, but the two directions are not quasi-inverses?
I’m not sure but I can explain why I believe there ought to be some Strong Birkhoff Theorem in HoTT. The basic idea is that the classical proof of completeness has a deliberate information loss, specifically a set truncation. My gut feeling is that the propositional truncation and the set truncation actually get rid of a lot of common information. Consequently, we should be able to truncate less on both sides. Here is the basic idea…
The classical proof uses a term model. In HoTT, it makes more sense to use a higher inductive type. We have a bunch of Henkin constructors (just some anonymous constants to make sure has enough elements). For every -ary operator in our signature, we have a constructor . To get a model of , we need to add some path constructors. Basically, we need to make sure that if is an identity in then we have . There’s a few variations that can be used here and I’m not sure whether it makes a difference to pick one over the other.
At this point, we have an algebra that, by definition, satisfies all identities in . To get a set-based algebra, as in the classical completeness proof, we would then take the set-truncation of and this would be used to establish the weak completeness theorem for equational logic. If we skip that step, then paths obtained by different proofs retain their distinctness to some extent. To get the strong completeness, all we need is to figure out how much is retained and how much is lost, and appropriately revise the definition of . Note that essentially all trivial variations are lost. For example, whenever , the resulting algebra is a set-based, though technically has more than one proof.
I worked through a bunch of this today. I’m pretty confident I have a normal form for equational proofs that gives the right thing. Details are a bit of a pain but they are much cleaner than I had anticipated. I’m typing a note about this but it won’t be a blog post because of all the proof trees and such (and typing will be slow for the same reason). Stay tuned!