OK so this is really just another equality post. And an apology to the Imperial 1st years for teaching them badly. Let’s start with two questions.

- Q1) How many binary relations are there on a set with 2 elements?
- Q2) Is
`2 + 2 = 4`

equal to Fermat’s Last Theorem?

Ok so I am voting for “16” with Q1 and “of course not” with Q2. But I now realise that these answers are inconsistent with each other I know this is probably logic-for-computer-scientists 101, but I never did that course so I’m learning it myself now, in an inefficient way. And in some sense the point of these posts is to try and teach these ideas to mathematicians in a way that makes sense to them. Ok so let me assume that the answer to Q1 is 16 and the answer to Q2 is no, and deduce a contradiction.

It’s clear that for integers, and a positive integer, mod is a true/false statement, so for a fixed this gives us a binary relation on the integers — indeed, an equivalence relation — and the equivalence classes are . Happy so far?

Now let be a subset of the integers. This “congruence mod ” equivalence relation induces a binary relation on as well.

OK so now fix , and let’s define to be the binary relation on of being congruent mod 2, and let’s define to be the binary relation on of being congruent mod 3.

And now, because of Q2 above, the statement mod is not *equal* to the statement that mod — they’re definitely equivalent logically because they’re both true — but they have different mathematical content and so are definitely not *equal*. However is *equal* to mod *by definition*, and is *equal* to mod *by definition*, so we are forced to deduce that is not *equal* to which of course implies that is not *equal* to . But when we were answering Q1 we decided that and were *the same binary relation* (because and are both true for all and in ), and if you think of binary relations on as subsets of then of course and *are* equal. So if you think about them one way, they’re equal, and if you think about them in another way, they’re not.

This phenomenon (two logically equivalent true/false statements are *equal*) is called propositional extensionality. It’s an axiom in Lean; note that Lean uses type theory as its foundations. I’m not sure that it can be expressed in set theory (everything is a set in set theory, and propositions are not sets so I’m not 100 percent how to even do mathematics with them in set theory). I surely use propositional extensionality all over the place in my work, it’s related to the law of the excluded middle which I also use all over the place. This is one of these things which, when I first read it with my “proper mathematician” hat on, I just thought “this is silly constructivist computer scientists making a fuss about nothing”. I just checked the perfectoid project and indeed I can confirm that at least one point in our repository Commelin, Massot and I must have assumed it, because our definition of a perfectoid space in Lean relies on this axiom.

Conversely, I *explicitly told* the 1st years in my lectures earlier this month that I was a bit uncomfortable with the idea that `2 + 2 = 4`

*equals* Fermat’s Last Theorem. But both of these things are true, so by propositional extensionality, they’re going to have to be equal, and if you don’t accept this then you have to accept that there are infinitely many binary relations on a set with two elements (or even on a set with one element — for each true statement I can define to be equal to that statement). And what is annoying is that on the test today I asked my students how many binary relations there were on a set with two elements and several of them said that there were infinitely many, and I think that this answer, which I am going to have to mark as wrong, does have its merits. It is, unfortunately, not the answer that a mathematician would give, and I am supposed to be training these people to be mathematicians.

However I think that on this occasion I am not training them very well. I think that I should have made it crystal clear in the lectures that, in mathematics, we say that two binary relations and on a set are *equal* if . Now looking at it this way, it would seem better to say that and were somehow *equivalent*, and hence I should have asked the first years to count the number of binary relations on a set with two elements *up to equivalence*. But pedagogically this seems like a real can of worms because some of them are having a hard enough time wrestling with mathematics this abstract anyway.

## How mathematicians cheat.

Here’s what I think is going on. Mathematicians have an incredibly powerful and fluid notion of equality, and I believe that many of us do not ever really examine it carefully. We know exactly how it works, we have no clue what the axioms for it are, and when we become PhD students we might even start using the = sign to denote canonical isomorphism. We are in good company — Grothendieck does this in EGA, and Milne’s book on etale cohomology explicitly states it as a convention in the introduction; thanks to @TheHigherGeometer who dug out screenshots on Twitter when I was last going on about this stuff. Because we don’t really understand it properly, we don’t teach it properly, and then we wonder why students think that there are infinitely many binary relations on a set with two elements.

I think that what is really going on is that some students in our classes manage to just “get it”, and see what we’re doing, and then copy it, and those are the ones we think are mathematicians. And those who foolishly believe that `2 + 2 = 4`

is not equal to Fermat’s Last Theorem and hence deduce that there are infinitely many binary relations on a set with two elements — these are people who “don’t get it” and we just mark their answers as incorrect. What is happening is that those people who “get it” are managing to see through the fog and are beginning to understand what we mean when we say that two things are “equal”, or “the same”, or “canonically isomorphic” or whatever way we use to describe the appropriate equivalence relation meaning “the same thing as far as a mathematician is concerned” on the objects we’re looking at.

When I found the EGA example of Grothendieck saying that two canonically isomorphic localisations were equal, even though they are literally not at all equal according to the standard definition of a localisation, I mentioned this to Johan de Jong, someone who has been teaching algebraic geometry for a very long time now. He told me that he had noticed that some students really struggled with this idea in his class — it comes up in the definition of the structure sheaf on a scheme. If is a commutative ring and with, say , then the basic open sets and really are *actually equal* as subsets of , so the rings we assign to these basic open sets when defining the sheaf on the standard basis had better also be *actually equal*, but when you look at what is done in most of the books, we assign to and to and these are *not actually equal*. Our fix as mathematicians is to simply *declare that they are equal anyway*. This is a fudge, but it works, because they are “sufficiently equal” (they are, after all, canonically isomorphic). Students that don’t understand this point are deemed to be not very good at algebra. But there is an explicit issue here. Do we explicitly teach it? No we don’t, we just expect them to get the hang of it. Should we explicitly teach it? Will it confuse people more? Maybe it should be mentioned.

In 2011 I was assigned to teach a basic group theory course at Imperial; the previous lecturer was Prof. Martin Liebeck, a teacher whom I hugely respect. The students had already seen a definition and basic examples of groups in a more general “introduction to bits of algebra” course, but it was my job to start on group theory proper and define things such as homomorphisms, kernels, the first isomorphism theorem and so on. But Prof. Liebeck’s notes (which I was following) introduced the notion of an *isomorphism* of groups before the notion of a homomorphism. At the time I thought this was ludicrous. In any category, an isomorphism is a morphism with a two-sided inverse, and this felt like a natural definition of isomorphism to me; why introduce it before introducing the morphisms? But when I went to the library and looked through the books that Prof Liebeck was recommending, one of them — Fraleigh’s “Abstract algebra” (6th edition) — devoted two paragraphs in his “changes from the 5th edition” explaining that after many years of teaching algebra he had become convinced that doing isomorphisms, carefully and properly, before homomorphisms, was, he believed, pedagogically very important. Because I was young and inexperienced, I decided to believe Liebeck and Fraleigh, and continued to do the same.

What I have realised now though is that this concept — isomorphism of groups — is a great example of showing students how fluid we are when it comes to equality (“there are 2 groups of order 6”), so it’s good to teach it early. However we have already started with this fluidity in the introduction to proof course (with “equality of equivalence relations”) and perhaps this important idea of understanding when two things are “the same to a mathematician” should be introduced even earlier. For example, the fact that equivalence relations biject with partitions relies on this slightly subtle notion of equality of equivalence relations.

In summary then, at least one smart person came out of my course thinking that there are infinitely many binary relations on a set with two elements, and I now believe that this is not because they “don’t get it”, it is simply because I did not explain carefully enough what it means for two binary relations to be “the same”. My bad. Any other lecturer who has seen a student make the same mistake — maybe it is because they have not yet figured out that things can be “the same” without being *equal*, and we probably do not explicitly mention this subtlety in the lecture notes. In my case, this is because it has taken me 20 years of lecturing to notice that I am even doing it.

Pingback: Counting binary relations: an apology - Nevin Manimala's Blog

I have to say I am quite confused by this post. In set theoretic mathematics you can define a binary relation as a subset of the product. You define two sets as equal if they are (extensionally) equal and then there are 16 relations, without question.

If you want to be fancier you define a subset as an equivalence class of a monomorphisms (which works nicely in any topos) and you get the same result so long as you define relations as up to the same type of equivalence.

In type theory there are different notation of relation. For instance I can have a proof-relevant relation on A meaning a dependent type (x y : A) -> Type where each type returned is subsingleton (and so either it is empty or is singleton if we accept excluded middle). This is a very different notion and if it is the one you use then it makes perfect sense that this topic is confusing.

Moreover ,when we speak of 2 + 2 = 4 equaling FLT, again it is necessary to say what the actual question here is. There are proof carrying types where the first is the identity type of two terms in the natural numbers and the second is some complicated dependent type and we can only ask if these are equal in a universe of types at which point this seems like a very subtle question (and the answer is dependent on our type theory). We could equally ask if the propositional truncation of these two types is equal and indeed it is because they are both true and we have an excluded-middle style axiom in our type theory that says all singleton types are in fact equal. In general though, a type theory should be only allowed to ask if two things are equal if we say both what the types of the things we are asking equality about and also what we are asking for equality with respect to (or some combination of both of these questions). Each of the natural numbers is equal if we take the propositional truncation of the natural numbers for example but this does not mean there is a single natural number!

LikeLike

Here’s what’s going on. I spent 30 years of my life believing that I was doing mathematics in ZFC, and this made me understand mathematics “in a certain standard way”. I had a very fluid notion of equality, other people would say the construction was canonical and I would just nod sagely or even agree, and the answer to the question “is Fermat’s Last Theorem equal to the statement that two add two is four” was “that’s not a mathematical question, it’s just foundational logic nonsense and is completely uninteresting: the use of the word “equal” in the question does not come under the remit of mathematical equality and hence the question is of no interest to a mathematician.” That response is absolutely the correct mathematical response, in my opinion. That response is *my* response to the question, as a mathematician. It’s just a *stupid question*.

It has only more recently occurred to me that in dependent type theory it is actually possible to *formally ask this kind of question* and it has made me think more carefully about what I as a mathematician mean by “equal”.

Now I am doing mathematics in dependent type theory, and I am on a hunt for mathematical equality. For example, the natural number game http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ is an exercise in a certain very precise kind of equality, an equality defined as an inductive type in Lean’s type theory. One thing I am 100% sure of now is that no type theory of any kind is offering me mathematical equality. I finally have a sufficiently good understanding of sufficiently many of the options to see that none of them are anywhere near mathematical equality. However in attempting to understand the difference between mathematical equality — that wonderful realisation when a mathematician defines two different things X and Y, draws a picture (e.g. a torus, or a commutative diagram) and then says that these two different things are “the same”) and you just *understand* how to think of them properly. You then spend the rest of your life rewriting with this “mathematical equality”, however far-removed it has become from any of the type theory rewrite systems that I know of.

LikeLike

Hi Kevin,

I’ve just been to some lectures on the Philosophy of Mathematics with Thomas Forster, and something he said reminded me of this post. He discussed the difference between an intensional (yes, that is the correct spelling – it is a logical term, distinct from “intentional”) and an extensional definition of something. To paraphrase him: intension is about meaning, extension is about “extent” or perhaps value. A statement in intension has meaning, but a statement in extension is just true or false. So as a statement in intension: “if 1+1=2, then Fermat’s Last Theorem is true” is a very uncomfortable statement, and we would probably not accept is as we cannot make the deduction, but as a statement in extension, it is “if true, then true”, which is true.

So what functional extensionality is saying is that we consider two functions to be the same if they have the same domain and same value at each input in their domain. For example, working mod p (with p prime), the functions and are the same function. But with an intensional understanding of functions, f and g are distinct – changing their domains to be , for example, would result in two different functions.

Propositional extensionality is similar: if two propositions imply each other, then they are equal (they are either both true or both false). But their intensional meaning may well differ. If I understand it correctly, this is why the `Prop` type in Lean only understands the values `true` and `false`: it throws away all intensional content.

The same would apply to relations: there are only distinct relations on a two-point set from an extensional perspective, but infinitely many from an intensional perspective.

I think this distinction may help to clear up some of the confusion in this – it certainly did for me.

LikeLike

Oh many thanks for this! In fact since I wrote this post in 2019 this distinction has become clearer to me. I even told my 1st years this year that sets and functions were extensional objects as far as mathematicians were concerned, although I don’t think I told them that binary relations were too! I think that as an undergraduate it is completely reasonable to be confused by this issue — as you probably know well, this difference is certainly not something stressed in mathematics departments at all, even though it sounds like it has been well-understood by philosophers forever 🙂

LikeLike