Thread by @TOEwithCurt

Godel's incompleteness theorem (all consistent formal systems aren't "complete" (provided it models arithmetic)) and Turing's theorem (you can't always determine if a program halts) are what you've likely heard of already. There are various other no-go results in philosophy / math, like Cantor's theorem, Rice's, Lob's, Tarski's undefinabilty as well… What most people don't know about is that there's just *one* theorem that underlies all of these: Lawvere's fixed point theorem. 1/13

When a function maps elements from one set to another, Lawvere showed that if you have a "nice" function (technically, a "fixed point operator") that can map elements from a set of functions to another set, you'll *always* find a fixed point (an element that maps to itself). Importantly, we don't assume the existence of this operator. We *derive* it. That's the power of this theorem. 2/13

Fixed points are all over math so you're likely thinking that there's nothing interesting to be found here and this was my initial reaction as well. Lawvere, however, demonstrated that fixed points are what is necessary to understand self-reference itself. It's a way you can mathematically talk about the “I” of the “self.” Let's think about it: a statement that refers to itself, a program that analyzes its own code, a formula that says “If proving me implies I’m true, then I’m proved” …. this is where you have (seemingly) non-sensical assertions. Lawvere's theorem is thus about the birth of paradox. 3/13

Here's an example. Let's say you have a set of all possible descriptions of things. Now, try to describe the set of all things that *don't* describe themselves. Does that description describe itself? If it does, then it shouldn't, and if it doesn't, then it should. Russell's paradox. Yes. Familiar territory. Good padawan. Now let's be specific, rigorous, and (moderately) more advanced. 4/13

A cartesian closed category is, roughly speaking, a context where you can multiply objects (take products), have a terminal object (you can think of this as a “unit”), and for every pair of objects X, Y you can form an “exponential” Y^X. Concretely, this Y^X is the object of “all maps” from X to Y—just like the set Y^X in classical set theory is "all functions" X→Y. Formally, there’s an “evaluation” map ev: (Y^X) × X → Y. This evaluation is "universal" in the sense that, for any *other* object Z and a morphism u: Z × X → Y, there’s a unique factorization u = ev ◦ (ũ × id) via ũ: Z → Y^X. That property is how exponentials generalize “function spaces” from set theory into category theory. You have to go through this rigmarole in category theory because category theorists make great pains to tell you they don't like to look "inside" an object. It's similar to how a vegan will always announce they're veganism. 5/13

Lawvere’s fixed point theorem uses these exponentials to encode self-reference. How? Suppose you have an object X in a cartesian closed category C (defined in previous tweet), and a morphism f: X → X^X. We can interpret f as “assigning a function in X^X to each point of X.” Next, you compose f×id: X → (X^X) × X with the evaluation map ev: (X^X) × X → X to get δ: X → X. Okay. Now we're at something interesting! It's *this* δ that gets called a “diagonal” or “self-application” morphism. 6/13

Lawvere’s theorem says if δ behaves like a fixed point operator (it provides a solution to δ(x) = x for suitable x), you inevitably get an element x ∈ X such that f(x) maps x to itself. In simpler terms, the object “describes” itself through f, and δ almost literally forces the existence of a self-fixing element. 7/13

In set-theoretic language, this recovers diagonal arguments (like Gödel’s or Tarski’s) but from a high-level perspective: once you can treat “morphisms” (what I called “maps” earlier, but I'm appeasing the categorists here even though there are signs to not feed them) like first-class objects (the exponentials), the act of letting an object feed itself into its own “description” can’t be avoided. This is important. The act of letting an object feed itself into its own description is guaranteed by this theorem. The fixed point x with δ(x) = x is precisely the self-referential twist that spawns statements like “I am not provable” or “I do not describe myself.” 8/13

Lawvere’s result consequently shows that any category rich enough to interpret “functions from objects to themselves” will host a diagonal meltdown of some sort… When you say “Here’s a program that decides halting,” you’re implicitly constructing an X→X^X arrow, letting the system interrogate itself. Similarly, Gödel’s “I am not provable” statement amounts to building a morphism that tries to represent its own unprovability. You embed a formal system inside itself, making it chase its own tail. Any attempt to fully capture your own rules in one system must yield a function from X back to X^X… 9/13

Tarski’s undefinability theorem—“Truth can’t be expressed in the same language”—is another spin on the same diagonalism. If you try to define a truth predicate inside your own formal language, you end up referencing the definability of that predicate within itself. Again, that’s effectively building an f: X → X^X that lumps “definable truths” into an object fed back to itself, forcing a Tarski-style contradiction. 10/13

the fixed point phenomenon doesn’t vanish even if you try to slice away parts of your theory. As long as you’re in a cartesian closed universe where exponentials exist, the self-referential “trapdoor” is still there. This is part of why so many results look suspiciously similar, all boiling down to “there’s a statement you can’t tame.” This is what comes from giving pellet feed to categorists. Sometimes it's a worthwhile trade. Sometimes. 11/13

There are of course a varieties of caveats I have to make, such as surjectivity on f is required, and the exponential needs to be defined functorially, not just object-wise. My relationship to these specifics is on and off due to me attempting to keep it as simple as possible while getting the core message across but it does provide me dread to omit details. The real Yoneda Lemma was the existential crisis we had along the way. 12/13

Some people interpret this theorem as reality telling you it doesn’t allow “perfect self-awareness”—there’ll always be some ineffable aspect lurking outside your system’s ability to capture it. Lawvere’s viewpoint just bundles that limitation into a single, sleek categorical argument. 13/13