The Mirror · movement II of VI
Five lines, and not a single choice made in any of them. Out of the mirror alone this movement builds the forced fixed point — one point carried by the maps until it returns as its own image — and shows the argument uses no negation, no infinity, and no excluded middle. That austerity is why it survives translation into every setting, and why its limits are constructive facts rather than classical residue.
The fixed point is the value the self-name takes on itself. The whole argument is the diagonal — apply a thing to its own name, then twist.
Before the point is built, it is worth fixing precisely what is claimed and precisely what is assumed — for the theorem is at once stronger and cheaper than its usual telling. It is stronger in asking nothing whatever of the twist: α need not be continuous, monotone, or structured in any way, and B need not be a set. It is cheaper in not requiring the mirror to reflect everything — only the single map it is about to construct.
Two refinements sharpen the hypothesis to its true floor. First, there is a proof-specific weakening for a fixed α: the proof invokes the naming property for one map only — the diagonal g it is about to write — and even then only at a single point, so the conclusion survives where φ faithfully names no other map at all. The mirror need not be onto; it need only fail to forbid the one map that turns on it. Second, a point is here a global element 1 → X, the notion that separates morphisms in a well-pointed category such as Set; where global points are too coarse to tell maps apart, one replaces them throughout by generalized elements S → X at a varying stage S and reads the proof in the category’s internal language, which is intuitionistic. The statement and the argument do not change — only the ambient logic loosens. Everything below is written with points, for legibility; the cell-by-cell chase will show that not one of them was load-bearing.
Here is the key, shown. Fix any twist α on the answers B; out of the mirror alone we will build a point the twist leaves unmoved. Reveal the proof a line at a time.
The five lines have a shape. Drawn, the proof is nothing but objects and arrows — the categorical home where it actually lives, and the reason it survives translation into every other setting. Read it along the bottom, left to right: a single point, carried by the maps, comes back to itself.
The diagram asserts that a square commutes; here is the assertion discharged, every equality named, and — the whole point of doing it this way — not one element of A or B mentioned beyond the single point a the hypothesis hands over. Write g = α ∘ ev ∘ ⟨φ, 1⟩ : A → B for the diagonal, and let a : 1 → A name it, φ ∘ a = ⌜g⌝. Put s = ev ∘ ⟨φ, 1⟩ ∘ a. Then, reading downward, each line is a single universal property:
Look at what the justifications were. Line 2 is the universal property of the product; line 3 is the hypothesis; line 4 is the universal property of the exponential; the rest are the definitions of g and s and the bare associativity of composition. No step inspected an element of B, asked what A contains, or split into cases. That is exactly why the result is not about sets: replace the terminal object 1 by an arbitrary stage S and the point a by a generalized element S → A, and the identical six equalities prove a fixed point at stage S — internally, intuitionistically, in any cartesian closed category. The points in the five-line telling were scaffolding; the chase shows the building stands without them. And the very first arrow already carries the whole mechanism: ⟨φ, 1⟩ = (φ × 1) ∘ Δ, where Δ = ⟨1, 1⟩ : A → A×A is the diagonal, so the construction opens by copying a — one copy through the mirror, one kept as argument. A merely monoidal-closed setting, lacking that diagonal, cannot even form the map; contraction is the cartesian gift the proof spends first.
No line of it makes a choice. The map g is forced by α and φ; the point a is handed over by the mirror; the value s is simply whatever φ(a)(a) already was, and α(s) = s falls out by substitution — not by search, not by construction, not by any appeal to what B happens to contain. That total absence of choice is why the conclusion cannot be dodged, and why the same forced point returns one level up in the Ascent and one level down in the Descent: nothing was settled here that could have been settled otherwise.
And there is more in the formula than existence. The fixed point is not merely shown to be — it is written: s = φ(a)(a), with a whatever names g = α ∘ ev ∘ ⟨φ, id⟩. Every occurrence of α stands in plain view, so the point is a uniform expression in the twist — change α and the same expression tracks it, re-deciding nothing. That uniformity is the whole distance between a fixed-point theorem and a fixed-point operator. In a reflexive object, where φ may be taken to be the identity, the expression contracts to a single closed term — the combinator Y — that returns a fixed point of any map handed to it. The proof does not exhibit one fixed point; it is a machine that manufactures them on demand. Recursion is that machine, switched on.
The formula’s uniformity was just claimed; here it is cashed out to the last symbol. Take the most self-referential object there is — a reflexive D ≅ [D → D], the carrier of the untyped λ-calculus, where application app : D × D → D is the evaluation ev and every term is at once a function and an argument. Now the mirror φ may be taken to be the identity: a term names itself. The diagonal g the proof builds, for a twist α, is the term that copies its argument and feeds it to itself under α:
So Y = λα. (λx. α(xx))(λx. α(xx)) — Curry’s combinator — is not analogous to Lawvere’s construction; it is it, read in the one object where the mirror is the identity. The point a that names the diagonal is δ; the forced value s = φ(a)(a) is δ δ = Y α; the equation α(s) = s is the lone β-reduction Y α = α(Y α). The theorem that forbids — Cantor, Gödel, Turing — and the operator that builds — Y, the engine inside every recursive definition — are the same five lines, separated only by whether the object admits the mirror or refutes it. Here it admits it, and the forced point is a running program; flip to an object that reflects every map yet carries a twist with no fixed point, and the identical construction demands instead a point that cannot exist. Power and limitation are not two proofs but one, evaluated at two objects.
Notice what the proof used and what it did not. Its first act is the diagonal of §I made flesh: the step ⟨φ, id⟩ is (φ × id) ∘ Δ, so before anything else the construction copies a — one copy to be read as a function, the other to be its argument. Take that copy away and the proof cannot start. After it, only evaluation, currying, and one named map are used; no negation, no infinity, no numbers — and, worth stating precisely, no logic: no excluded middle, no choice. The argument is intuitionistically valid, which is why it holds verbatim inside every elementary topos, and why its limitative conclusions are constructive facts rather than classical residue. There is a stubborn folklore that Cantor's diagonal needs the excluded middle; it does not. The missing element is exhibited — g(a) = α(φ(a)(a)) — not inferred from the failure of its presence; the whole work is the equational chain α(s) = α(φ(a)(a)) = g(a) = φ(a)(a) = s, and an equation needs no bivalence to hold. The diagonal is not a trick about sets or sentences, and not an artifact of classical reasoning. It is what self-reference is — assembled from the one operation any cartesian setting performs for free: using a thing twice.
Everything ahead is a single conditional read in one of its two equivalent directions. Forwards, as proved: a mirror onto B forces a fixed point of every α : B → B — power. Its contrapositive is not a second theorem but the very same one: if some α : B → B has no fixed point, there can be no mirror onto B — limitation. Cantor, Gödel, and Turing are this contrapositive evaluated at a single fixed-point-free twist. To call power and limit two sides understates the bond: they are P ⟹ Q and ¬Q ⟹ ¬P — one arrow, and you may enter it from whichever end the world hands you.
The contrapositive is not an abstraction awaiting instances; one substitution turns it into the oldest limitative theorem there is, in its most general form. Work in any elementary topos — the natural home of the internal logic the chase already inhabits — and take B = Ω, the subobject classifier, the object of truth-values, with α = ¬, internal negation. Then Bᴬ = Ωᴬ is the power object P(A), and a point-surjective φ : A → P(A) would be an enumeration of every subobject of A by the points of A.
In any non-degenerate topos, ¬ : Ω → Ω has no fixed point: a global ω with ¬ω = ω would assert ω ↔ ¬ω, and ¬(P ↔ ¬P) is a theorem of intuitionistic logic — so the topos would collapse to 1 ≅ 0. By the contrapositive, then, no object point-surjects onto its own power object, A ↛ P(A). That is Cantor’s theorem, and it has spent neither cardinality nor the excluded middle — only the missing fixed point of negation. The diagonal subobject it forbids is the explicit { x : x ∉ φ(x) }, exhibited, not inferred.
Russell’s paradox is the very same diagram with one premise stipulated rather than examined. Assume naïve comprehension — that membership ∈ : V → P(V) is point-surjective, every predicate cutting out a set. The diagonal g for α = ¬ is then the set R = { x : x ∉ x }; the point a naming it is R itself; and the forced value s = (R ∈ R) satisfies s = ¬s. Where Cantor reads the impossibility as there is no such surjection, Russell — having legislated that the surjection exists — reads it as there is no such system. One diagonal, pointed two ways; the difference is only which premise the world declined to surrender. It is the absent-versus-paradox split of §III, here settled at the level of the topos.
Five lines, then, carry a remarkable freight. They are constructive, so they hold in every topos; point-free, so they hold without elements; uniform, so they yield not a fixed point but the operator that makes them; and reversible, so the same arrow that builds recursion forbids the perfect set, the complete truth predicate, the total decider. Everything this corpus files under power and everything it files under limit is this one construction, walked in one direction or the other. What remains — the four fates, the dial, the costumes — only asks, case by case, which direction a given world will allow.
A movement of The Mirror, the keystone of Quodlibet. The theorem and its five-line proof are Lawvere’s (1969); the synthesis is the author’s.