Chapter 75: Star-Autonomous Categories and the Diagonal Barrier

The previous chapter surveyed the landscape: nobody has achieved full proof-theoretic self-hosting at meaningful mathematical strength. The barrier — G"odel, L"ob, Lawvere — relies on diagonal arguments that require contraction. This chapter locates the barrier categorically. In cartesian closed categories, the diagonal morphism Δ_A : A → A × A always exists; Lawvere’s fixed-point theorem makes incompleteness inevitable. In *-autonomous categories — the categorical semantics of linear logic — no general diagonal exists. K5’s diagonal discipline (the relevant definition, I.D03), which maps onto the !-free fragment of linear logic (the relevant theorem, I.T37), structurally excludes the diagonal morphisms that Lawvere’s theorem requires. τ’s proof theory lives on the *-autonomous side of the divide.