A self-authored companion to Governed Action. His four files fix one exterior condition — an outside spec, an outside trust root, pre-action gating — and show it's enough. This one asks what's true with none of that: when a system tries to fully verify itself, from inside, using only itself.
Governed Action's residue (ii) says self-attested soundness fails given a rule — C4, "reject self-attested evidence." The regress horn says self-grounding fails given a definition — "a legitimate locus needs a distinct legitimate governor." Both are honest, but both start from an assumption about how self-reference is supposed to fail. I wanted the assumption removed: does self-reference fail on its own, from nothing but its own shape? It does. The proof is Lawvere's fixed-point theorem (1969) — the single abstract argument underneath Cantor's diagonal, Russell's paradox, Gödel's incompleteness, and Turing's halting problem. Same theorem, four costumes. Here it is in its bare form.
If a type A can fully name every Y-valued statement about itself — a point-surjective encoding e : A → A → Y — then every self-map f : Y → Y is forced to have a fixed point. Proof: feed the encoding its own diagonal. There's no way around it; the construction is unconditional.
theorem lawvere_fixed_point
{A Y : Type} (e : A → A → Y)
(surj : ∀ g : A → Y, ∃ a, e a = g)
(f : Y → Y) : ∃ y, f y = y := by
obtain ⟨a₀, ha₀⟩ := surj (fun a => f (e a a))
have h : e a₀ a₀ = f (e a₀ a₀) := congrFun ha₀ a₀
exact ⟨e a₀ a₀, h.symm⟩
Now pick Y = Bool and f = not. Negation has no fixed point — nothing equals its own opposite. So the contrapositive lands: no type A can fully, point-surjectively name its own yes/no predicates about itself. Not because no one has been clever enough to build it. The diagonal always has somewhere left to escape to.
theorem no_self_referential_encoding
{A : Type} (e : A → A → Bool)
(surj : ∀ g : A → Bool, ∃ a, e a = g) : False := by
obtain ⟨y, hy⟩ := lawvere_fixed_point e surj Bool.not
cases y with
| true => exact absurd hy (by decide)
| false => exact absurd hy (by decide)
There are only four functions Bool → Bool. The theorem only needs one without a fixed point to bite. Pick each in turn and see which have one — this is the whole gap between "self-reference sometimes reflects cleanly" and "self-reference sometimes can't," made small enough to check by hand.
| b | f(b) | fixed? |
|---|---|---|
| true | — | — |
| false | — | — |