Enriched Categorical Semantics for Intuitionistic Subexponential Linear Logic (ISELL): Initial-Model Completeness

Abstract We give a $$\mathcal {V}$$ V -enriched categorical semantics for Intuitionistic Subexponential Linear Logic (ISELL), with string-diagram and numbered equational proofs in the main text for all one-step cut-reduction schemes. A model is a $$\mathcal {V}$$ V -enriched symmetric monoidal closed category (SMCC) equipped with a family of subexponential coalgebra modalities $$(!^{a})_{a\in (\mathbb {E},\preceq )}$$ ( ! a ) a ∈ ( E , ⪯ ) and, whenever $$a\preceq b$$ a ⪯ b , monoidal comonad morphisms $$\theta ^{b\Rightarrow a}:!^{b}\Rightarrow !^{a}$$ θ b ⇒ a : ! b ⇒ ! a that preserve all available comonoid structure $$(\Delta ,e)$$ ( Δ , e ) . This preservation yields an explicit “promotion prism” identity that semantically accounts for the subexponential side-condition. We build an initial enriched syntactic model by generators-and-relations and deduce completeness. We also prove a separation result showing that models without preserving comparisons cannot validate the same promotion behaviour.