How the snake comes to bite its own tail
Lawvere's theorem asks for one thing: a system that can name all of its own operations. The Kernel assumed that power; this is how it is built. Nothing in ordinary grammar lets a sentence point at itself or a program read its own text — and yet, by a single construction repeated in four settings, both become not merely possible but forced. The arithmetisation of syntax, the diagonal function, the recursion theorem, the combinatory algebras, and the reflexive object are not four tricks. They are one move: a section of evaluation.
component II of the diagonal · the machinery of reflexivity, isolated and deepened — representability and the coding of syntax, the diagonal lemma derived from the diagonal function, the s‑m‑n and recursion theorems with a running quine, partial combinatory algebras and combinatory completeness, the reflexive object D ≅ DD, and the single structural fact beneath all four
Before reflexivity can be built it must be understood why it is not free. Nothing in the surface syntax of a language lets an expression refer to itself — and the precise shape of that obstruction is exactly what the mechanism must overcome.
the sentence that is not yet written "This sentence is unprovable" sounds like a definition, but read as one it is circular in a way that does not obviously bottom out. To write it formally we would need a sentence S equal to ¬Prov(⌜S⌝) — yet ⌜S⌝, the code of S, cannot be supplied until S exists, and S cannot be written until ⌜S⌝ is known. Substitution, the one tool the grammar offers, makes this worse rather than better: substituting a formula's code into the formula yields a longer formula, never one that contains its own, completed code. The fixed point we want is a fixed point of substitution itself, and the surface grammar provides no such thing.
the same wall, in three rooms The obstruction is not peculiar to arithmetic. A program that wishes to print its own text faces it squarely: a program is a finite string, but the string is not available to the program as it runs unless it was somehow built in — and building in the full string seems to require a string strictly larger than itself, which then must contain that, and so on. A set that contains exactly the things satisfying a property would let any predicate name a set — but {x : x ∉ x} shows the naïve version cannot be coherent. And a space that contained all of its own self‑maps would let every map be a point — but Cantor forbids it for plain sets. In each room the same wall: the surface structure does not close on itself, and naïvely forcing it to either fails to terminate or collapses. The mechanism is whatever lets the structure close without either.
State the requirement exactly and the path forward appears. We do not need a sentence that literally contains its own code — that is the impossible object. We need a sentence S and a substitution operation sub such that S is provably equivalent to the result of applying the target predicate to ⌜S⌝, where ⌜S⌝ is reached not by containment but by computation — by running sub on a smaller seed. The whole mechanism, in every guise, is the construction of a fixed point of a substitution (or application) operator: in arithmetic the operator is the diagonal function; in computation it is program‑specialisation; in the λ‑calculus it is self‑application. The inward turn is achieved not by grammar but by a coded operation whose own fixed point the grammar can then name. Everything below is four ways of building that operator and taking its fixed point.
The first and decisive step is to make a theory of numbers able to talk about its own formulas. Once syntactic operations are arithmetic functions the theory can represent, the system has gained the power to name itself — and the rest is the diagonal.
coding Assign to every symbol a number, to every finite string of symbols a number built from its parts — by prime exponents, or any effective pairing — and to every formula and every proof its Gödel number. The assignment is mechanical and invertible: from a number one recovers the string, and one can decide whether a number codes a well‑formed formula, a sentence, a proof. What matters is not the particular scheme but its effect: finite syntactic objects are now numbers, and operations on syntax are now functions on numbers. The act of substituting one formula into another, the act of checking that a sequence of formulas is a valid derivation — each becomes an arithmetic function of the corresponding codes.
representability — the bridge that bears the weight Coding alone is bookkeeping; the load is carried by representability. A function f : ℕ → ℕ is represented in a theory T by a formula F(x, y) when T not only gets every value right but knows it does so uniquely:
Two functions do the real work, and both are primitive recursive, hence represented in any sufficiently strong arithmetic. Substitution sub(⌜φ(x)⌝, n) = ⌜φ(n̄)⌝ takes the code of a formula and a number and returns the code of the formula with that numeral plugged in. The diagonal function d(⌜θ⌝) = ⌜θ(⌜θ⌝)⌝ — the special case that substitutes a formula's own code into itself — is built from sub in one line. Represent these and the inward turn is mechanically available: the theory can speak of "the formula obtained by feeding θ its own quotation," and can prove the basic equalities that govern it. The provability predicate Prov(x) — "x codes a provable sentence" — is then a Σ₁ formula built over the represented "is a proof of" relation. Everything the limitative theorems need is assembled from these few represented operations.
With substitution represented, the inward turn is one short construction. It is the precise mechanism by which "this sentence" acquires a referent — and it has exactly one moving part.
the one moving part Recall the diagonal function d(⌜θ(x)⌝) = ⌜θ(⌜θ⌝)⌝ — given the code of a one‑variable formula, return the code of that formula applied to the numeral of its own code. It is primitive recursive (it is just sub with both arguments tied together), so the theory represents it. The diagonal lemma is what this single represented operation buys: for any predicate ψ(x), a sentence equivalent to ψ applied to itself.
the construction — how the tail is caught
The reference is intensional: S contains the code of θ, not of S, and only after substitution does θ(⌜θ⌝) provably coincide with ψ(⌜S⌝). Contrast the λ‑calculus, where self‑application x x is literal and "the term is its own name" needs no coding. Same fixed point, two grades of literalness — and the intensional grade is exactly the one that had to await Gödel, because it presupposes the discovery that syntax can be arithmetised at all. Gödel's true innovation was not the diagonal, which Cantor already had, but the coding that lets a theory of numbers become a reflexive object. Choose ψ = ¬Prov and S is Gödel's sentence; ψ = ¬True and it is the Liar; ψ = Prov → φ and it is the key to Löb — the same fixed point, built once, hostile or harmless by the choice of ψ alone.
Computation makes the same fixed point tangible and runnable. Two theorems do it: the s‑m‑n theorem, which specialises programs computably, and Kleene's recursion theorem, which hands every program transformation a fixed point.
s-m-n — substitution, computed The computational analogue of sub is the s‑m‑n theorem: there is a total computable function s that hardwires inputs into programs. Given a program e of two arguments and a value x, s(e, x) is a program of one argument with φs(e,x)(y) = φe(x, y). Specialising a program to a fixed input is itself something a program can do — the stored‑program principle in its sharpest form. This is exactly the represented substitution of §III, now an effective operation on code rather than on formulas.
the purest case — a quine Take f to be the transformation "given a code c, return a program that ignores its input and prints c." Its fixed point e is a program that prints e — its own source, reconstructed from itself, reading no file and naming itself by no variable. A quine is the recursion theorem made to run. The example below is one, and it is the diagonal lemma in executable form: a string that is first quoted — the analogue of ⌜θ⌝ — and then printed into a copy of itself — the analogue of θ(⌜θ⌝). Run it; the output is the program, character for character.
Strip arithmetic and machines away and the bare algebraic essence of reflexivity remains: a set with a single operation, rich enough that every operation it can define is already one of its own elements.
a partial combinatory algebra Take a set A with one partial operation — application a · b — and two distinguished elements k and s obeying k·a·b = a and s·a·b·c = (a·c)·(b·c) (with the usual definedness caveats). That is a partial combinatory algebra, and it is the whole structure. From k and s alone one recovers a bracket abstraction λ*x. t — a syntactic procedure that, for any expression t built from variables and application, produces an element behaving as the function x ↦ t. This is combinatory completeness, and it is point‑surjectivity in its most distilled form.
Partial combinatory algebras are not exotic; the canonical one is the foundation of computability itself. Kleene's first model takes A = ℕ with application n·m = φn(m) — apply the n‑th program to m — and its combinatory completeness is the s‑m‑n theorem, its fixed‑point combinator is the recursion theorem. The term model of the untyped λ‑calculus is another; Scott's D∞ and the graph model are reflexive‑object realisations of more. Cockett and Hofstra's Turing categories are the categorical home: a partial combinatory algebra generates a category of "computable maps" — assemblies, or partial equivalence relations — in which the algebra appears as a reflexive object, and "the recursion theorem" becomes a structural feature of that category rather than a fact about ℕ. Self‑reference in arithmetic and self‑reference in computation are therefore not cousins but a single theorem read in two combinatory algebras — one through Gödel‑coding, the other through s and k.
The geometric culmination of reflexivity is a single object isomorphic to its own function space. Plain sets can never be one — that is Cantor — but domains can, and there self‑reference becomes total.
D ≅ DD The most extreme form of "a system names its own operations" is an object whose elements are its own self‑maps: a reflexive object, one with an isomorphism D ≅ DD. There the naming φ is the isomorphism itself — every point is already a function and every function already a point — so point‑surjectivity is automatic and Lawvere's theorem runs in its positive direction without qualification: every endomorphism has a fixed point, and a fixed‑point combinator exists. The untyped λ‑calculus is the syntactic reflexive object, where every term applies to every term; its models are the semantic ones.
how Scott escaped Cantor For plain sets the object is impossible: by Cantor |DD| > |D| whenever |D| ≥ 2, so no set is its own full function space. Scott's insight (1969–72) was to change what "function" means. Build D∞ as the inverse limit of D₀, D₁ = [D₀ → D₀], D₂ = [D₁ → D₁], … — but with [− → −] the continuous maps between domains, threaded by embedding–projection pairs. The limit satisfies D∞ ≅ [D∞ → D∞] on the nose. The Cantorian obstruction is dissolved because the continuous function space is vastly smaller than the full one: restricting to maps that respect the order and limits lets the space rejoin its own function space without the diagonal forcing a strict jump. By Lambek's lemma the isomorphism is genuine — D∞ is a true fixed point of the functor X ↦ [X → X], not a one‑way map.
This is where the Mechanism rejoins the Kernel exactly. The Kernel showed that the universal fixed‑point property is never owned by a non‑trivial codomain in Set — it is conferred by a point‑surjective naming. The reflexive object is that naming pushed to its limit: an object that confers the property on itself by literally containing its own maps. And the trick that makes it possible — passing from all functions to continuous functions — is the same move that gives domains a least element ⊥ and hence the order‑theoretic fixed‑point operator. So the two fixed‑point theorems meet here once more: the reflexive object hands the diagonal a fixed point of every endomap (Lawvere), and its order hands the same map a least one (Knaster–Tarski), and in D∞ they coincide. Reflexivity, built to its extreme, is the object whose existence the whole positive theory presumed.
Coding, the recursion theorem, the combinators, the reflexive object — they are not four mechanisms but one, seen four times. Each provides the same single thing: a section of evaluation.
what reflexivity is, exactly Evaluation ev : BA × A → B applies a name to an argument; it always exists in a cartesian closed universe. What does not always exist is a way to turn the system's operations into such names from the inside — a section of evaluation, a point‑surjective A → BA that packages operations as objects the system can hold and feed back to ev. Reflexivity is precisely the existence of that section. And the four constructions of this fascicle are four ways to build it.
the section of evaluation — what each guise provides
the four sections, named Read each construction as the section it builds. Gödel‑numbering is the section for arithmetic: the quotation ⌜·⌝ turns formulas — operations on syntax — into numbers the theory quantifies over, so operations become internal data. The s‑m‑n theorem is the section for computation: a program is already a datum, and specialisation packages any parametrised computation as a single program. Bracket abstraction λ* is the section for a combinatory algebra: it sends each definable operation to an element ⟨t⟩ of the algebra itself. And the reflexive object is the section made into geometry: the isomorphism D ≅ DD identifies operations with objects outright, the section and its evaluation becoming mutually inverse. Code becomes number, computation becomes datum, operation becomes element, map becomes point — one move, four notations.
The naïve fifth case is the one that fails, and its failure is the whole negative theory. Naïve comprehension would be the section for sets: every predicate φ already names a set {x : φ(x)}, so the power object would be a retract of the universe and every operation internal. Cantor's theorem is exactly the proof that plain sets refuse this section — no A → 𝒫(A) is point‑surjective, because the fixed‑point‑free swap on {0,1} would otherwise be forced to rest. Russell's paradox is the same refusal, felt as contradiction the moment the section is assumed anyway. So the entire landscape is one question asked of one arrow: does a section of evaluation exist? Where it does — arithmetic, computation, the λ‑calculus, a reflexive object — self‑reference is built, and the diagonal forces its fixed points. Where it cannot — plain sets, full truth, a total halting predicate — the attempt to build it is the impossibility proof. The Kernel proved what the section delivers; the Mechanism is the catalogue of how it is, and is not, made.
One requirement underlies every self‑referential phenomenon: that a system turn its own operations into objects it can hold. That requirement is a section of evaluation, and it is built four ways — by coding syntax into number, by storing programs as data, by abstracting operations into combinators, by an object that is its own function space. Each is the same arrow climbing back from values to names; each makes the inward turn that grammar forbids; and each hands the diagonal exactly what it needs to force a fixed point. The sentence that names itself, the program that prints itself, the term that applies to itself, the space that contains its own maps — four faces of the single act by which a system comes to speak of itself. Beneath them all: φ : A → Bᴬ, point‑surjective — the section that makes the mirror, after which every fixed point the rest of the fascicle studies is already inevitable.