Chapter 74: The Self-Hosting Landscape

the relevant chapter closed with the Gap Declaration (Remark [rem:gap-declaration], I.R17): CIC’s structural rules, type formation rules, and kernel axioms remain unearned — honest starting conditions, not defects. The enrichment ladder E₀ → E₁ → E₂ → E₃

charts a path from external CIC substrate to full self-hosting, where τ reasons about its own proof theory using only resources it has earned. Before traversing that path, one must ask: has any formal system ever achieved full self-hosting at meaningful mathematical strength? This chapter surveys the landscape. The answer is no.

The Self-Hosting Degree Classification (the relevant definition, I.D80) establishes four levels: none, partial, fragment, and full. We then examine the structural wall — G"odel’s incompleteness (1931), L"ob’s theorem (1955), Lawvere’s fixed-point theorem (1969) — that makes full self-hosting structurally impossible in the standard categorical setting. Every one of these impossibility results requires contraction: the diagonal argument uses a hypothesis twice. Without contraction, the constructions fail.

A survey of eight partial approaches — from Willard’s self-verifying arithmetic to Altenkirch–Kaposi’s type theory in type theory, from Feferman’s reflective closure to Girard’s transcendental syntax — shows that the landscape has been thoroughly explored. Approaches that achieve full self-hosting are mathematically trivial. Approaches at meaningful mathematical strength achieve at most a fragment. The Proof-Theoretic Landscape Survey (Remark [rem:landscape-survey], I.R18) tabulates the state of the art.

The chapter does not claim that τ can cross the wall. It identifies precisely where the wall stands and why K5’s linear discipline — confirmed by the Diagonal–Linear Correspondence (the relevant theorem, I.T37) — may offer a structural route that contraction-based frameworks cannot take.