Chapter 72: Diagonal Discipline as Linear Logic

the relevant chapter inventoried the meta-logical substrate — CIC’s structural rules that Book I imported but did not earn. One finding stood out: at the object level, τ’s diagonal discipline (K5, the relevant definition, I.D03) refuses contraction and weakening while preserving exchange. This is precisely the structural signature of linear logic. This chapter makes the correspondence precise. The Diagonal–Linear Correspondence Theorem (the relevant theorem, I.T37) establishes that K5’s three constraints map isomorphically onto the !-free fragment of Girard’s linear logic (1987). The program monoid of the relevant chapter (the relevant definition, I.D14) reinterprets as a linear sequent calculus, with NF-Confluence (Lemma [lem:nf-confluence], I.L02) as cut-elimination. Truth4 (the relevant definition, I.D21) acquires a natural explanation as the four resource states of linear logic. The correspondence was not designed — it was discovered. K5 was formulated in the 1st Edition without reference to Girard. That the diagonal discipline independently reproduces the structural core of linear logic is evidence that both frameworks respond to the same underlying constraint.