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

We give a 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 V V -enriched symmetric monoidal closed category (SMCC) equipped with a family of subexponential coalgebra modalities (!ᵃ)a∈ (E, ) ( ! a ) a ∈ ( E , ⪯ ) and, whenever a b a ⪯ b , monoidal comonad morphisms θ b⇒ a:!ᵇ⇒ !ᵃ θ b ⇒ a : ! b ⇒ ! a that preserve all available comonoid structure (Δ ,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.