The n-Category Café

More specifically, here is a true statement if we assume $x=x$ that I don’t see any way to prove without it: “there is a bijection between isomorphism classes of surjections with domain $A$ and equivalence relations on $A$”. That’s not quite a counterexample to your conjecture as stated, since it involves higher-order constructions, but I would argue that it’s an important part of mathematics.

Mike wrote:

More specifically, here is a true statement if we assume $x=x$ that I don’t see any way to prove without it: “there is a bijection between isomorphism classes of surjections with domain $A$ and equivalence relations on $A$”.

Nice. Here is a simpler statement that also requires $x = x$: “the identity function $id: X \to X$ is a surjection”.

Or, using that other idea: “for any set $X$ there exists a surjection $f : Y \to X$.” If we can find $f$ and $y$ with $f(y) = x$ then something equals $x$, so by symmetry and transitivity $x = x$.

Puzzle. What about proving that identity functions are really functions?

(I’m being a bit loose about what formalism I’m working in here, so this is a bit open-ended…)

Qiaochu wrote:

It seems plausible that there’s no need to use “because $x = x$” as a step in a proof in the most straightforward manner, since it can’t help you deduce (in the most straightforward manner) any equalities you didn’t already know.

Right, that’s the intuition behind my conjecture. My intuition was shaken when I learned on Wikipedia that in a certain formalism you can use $x = x$ to prove

$$x=y \; \implies \; y=x$$

and then use that to prove

$$(x=y \; \& \; y=z) \; \implies \; x=z$$

But that’s because I’d never thought of a setup where symmetry and transitivity weren’t axioms along with reflexivity!

So, I’m still hoping that my conjecture, corrected to take this into account, can be proved by someone who either knows more proof theory or is more patient than me.

But as you know, in category theory the natural categorification of $x = x$ is very important, namely identity morphisms $\text{id}_x : x \to x$ (e.g. in the Yoneda lemma, as universal bundles, etc.)

For me the most fundamental reason for including identity morphisms in category theory is that if we leave them out, the resulting gadgets can be thought of as categories of a special kind, by formally adjoining identity morphisms. And what we get are categories with no invertible morphisms except for the identity.

In other words: if we leave out identity morphisms it becomes impossible — or at least tricky — to define isomorphisms.

And this is somewhat interesting. If you think equations between objects in a category theory are evil, you might say “so let’s leave out identity morphisms, which are a way of expressing equations between objects: let’s only work with isomorphisms”. But without identity morphisms, the usual definition of isomorphism makes no sense!

It’s as if you need a bit of evil to avoid evil.

I would argue that this is really the essence of the importance of reflexivity, even outside HoTT. It is the only axiom that actually requires the relation to be inhabited at all, let alone to be inhabited at all values.

Intuitively, it’s the only non-recursive constructor of an inductively defined object. So while you may not actually use the axiom often, if at all, in practice, you can’t conclude anything at all about your relation without including it in the definition (or something else to serve that purpose).

In fact, by David’s remark above, if you assume symmetry and transitivity, then this formula is equivalent to reflexivity.

Great— this sounds like progress!

So my conjecture is false unless you can derive $x = x$ from first-order logic with an $=$ predicate obeying reflexivity, symmetry, substitution for functions and substitution for formulas.

And I guess the quickest way to prove you can’t do that that is to use Gödel’s completeness theorem and find a model of the above theory in which

$$\not{\forall x \, \exists y \; x = y}$$

holds. Such a model should be easy to find.

If so, my conjecture is false.

And in this case, I need some subtler way to explain the sense in which $x = x$ is useless in first-order logic. You see, this defeat does not feel like much of a defeat. I claim that using $x = x$ to prove

$$\forall x \, \exists y \; x = y$$

is not truly interesting: it’s just ‘another way to say the same thing’.

Hmm, I’ve taught analysis and never done a proof by contradiction like this!

What I have often done is show

$$x \le y \le x$$

and conclude that $x = y$. So apparently I believe the real numbers are totally ordered and therefore obey $x = x$.

(Why are you doing so many proofs by contradiction, anyway? Don’t you know it promotes tooth decay?)

That’s a good question. In intuitionistic logic the contrapositive of a statement is not always equivalent to the original statement. This means that certain very nice methods of proving $\not{Q} \implies \not{P}$ do not always work to prove $P \to Q$. I believe this may be part of why proving the contrapositive can be easier sometimes.

Wow, that’s wild! And what’s ‘1’ — the number of objects that are equal to any fixed object?

It’s really the same as how the empty set is standardly defined in ZF via the separation axiom: given an axiom that ensures the existence of a set, the empty set can be defined as the subset of elements not equal to themselves. By extensionality, the result is independent of the set whose existence is assumed.

It seems like a needless flourish to define the empty set as consisting of elements $x$ of some fixed set for which $x \ne x$, when you could have defined it to consist of elements for which $FALSE$ holds… or whatever is the quickest way you have at your disposal to say ‘$FALSE$’. But what the heck: let’s enjoy ourselves.

This “flourish” is probably an artifact of how $FALSE$ wasn’t considered part of the language of set theory. Boolean logic and truth tables were still rather new-fangled things at the time.

This is not to say that $FALSE$ was positively considered to be foreign to set theory either, merely that truth and falsity were optimistically expected to be properties of formulas in a sufficiently complete and explicit theory, rather than The Propositions of a Very Small theory… and then Gödel his notorious thing.

(I might muse that truth tables finally got their due respect when Gödel invented model theory, in which they became a small model of a particular theory; but for the actual history one should look for books instead of me…)

What’s FALSE? :-) Is it a logical formula?

I’m being slightly facetious here; there are all kinds of ways to set things up. I think most modern logicians would have no qualms admitting “true” and “false” as logical constants, but they could also be introduced in terms of other logical operators, via the formulae $\forall_x x = x$ (“true”) and $\exists_x \neg (x = x)$ (“false”). I’m not sure of the history, but I think maybe at some point those propositional constants were often not explicitly introduced; instead one had binary propositional operators $\vee, \wedge, \to$ and an unary operator $\neg$, and one represented “false” in a Boolean algebra as $p \wedge \neg p$ or some such thing. (Maybe Jesse was saying something like that earlier.) I’d have to check up on that.

I have maybe a slightly more serious point, having to do with the syntax of “pulling back” formulas. If $P(y)$ is a formula with one free variable $y$ of type $Y$, we would like to interpret it as a predicate on $Y$ or subtype of $Y$. Similarly, if $x_1, \ldots, x_n$ are the free variables of a formula $P = P(x_1, \ldots, x_n)$, with $x_i$ of type $X_i$, then the default interpretation would be as a predicate on or subtype of a product type $X_1 \times \ldots \times X_n$. In this way, we use the free variables of a formula to furnish its default context. Of course we might want to “pull back” to a different context – in fact we do this all the time – so that $P(y)$ could also be interpreted as a predicate on $X \times Y$ where $X$ is some given type, e.g., we might typically write $\{(x, y): P(y)\}$. One elegant way to do that, if we want to retain this idea of using free variables to declare the context, is to define the pullback formula $X^\ast P$ to be $P(y) \wedge [x = x]$ where $x$ is a variable of type $X$ not already in use.

So if we take your idea of starting with $FALSE$ (where the context is presumably the empty context) and we pull this proposition back to a predicate on some already introduced type $X$, we would represent it by the formula $FALSE \wedge [x = x]$, which is equivalent to $\neg [x = x]$ if you’ve set up your deductive system right. In that sense this “flourish” actually seems very natural to me (and it looks even better to me when reformulated in terms of Peircean string diagrams).

In other words, if you slight the empty set by excluding the nullary logical operations from your system, then you can make amends by appealing to reflexivity.