Subexponential Logic

Origin. Danos, Joinet, Schellinx (1993). Nigam and Miller (2009). Multiple exponential modalities. Fine-grained resource control. Foundation for logic programming semantics.

Models. Family of !ₐ modalities. Preorder on subexponentials. Controls which structural rules apply. Modular specification of behaviors.

Formalism.

Subexponential signature: Σ = (I, ≤, U) where:

I: set of indices (subexponential labels)
≤: preorder on I
U ⊆ I: unbounded subexponentials

Multiple exponentials: !ₐA for a ∈ I Each !ₐ has its own behavior.

Structural rules per modality: If a ∈ U: weakening and contraction for !ₐ If a ∉ U: linear (no structural rules)

Promotion: !ᵦ₁A₁, ..., !ᵦₙAₙ ⊢ B ────────────────────────── !ₐ-promotion !ᵦ₁A₁, ..., !ᵦₙAₙ ⊢ !ₐB (requires a ≤ βᵢ for every i — everything in the context must sit at or above the index being introduced)

Dereliction: Γ, A ⊢ B ──────────── der Γ, !ₐA ⊢ B

Absorption: If a ≤ b: !ᵦA ⊸ !ₐA — an immediate consequence of promotion, since the singleton context !ᵦA satisfies a ≤ b. So the modalities get weaker as the index goes down the preorder.

Example (linear logic programming): !_∞: classical (unlimited) !0: linear (one use) Program clauses in !∞, queries linear.

Symbols.

Symbol	Unicode	Name	Meaning
!	U+0021	Exclamation mark / Bang	Written !ₐ, the modality at index a
≤	U+2264	Less-than or equal / Preorder	Ordering on subexponential indices
Σ	U+03A3	Greek capital sigma / Signature	The triple (I, ≤, U) fixing the modalities
⊆	U+2286	Subset of or equal to	U ⊆ I, the unbounded indices
∈	U+2208	Element of	Membership of an index in I or U
⊸	U+22B8	Multimap / Lollipop	Linear implication; absorption is !_bA ⊸ !ₐA
⊢	U+22A2	Turnstile	Derivability
Γ	U+0393	Gamma	A context
I	—	Index set	Labels of the subexponentials
U	—	Unbounded indices	Those admitting weakening and contraction
der	—	Dereliction	Rule discharging !ₐA to A

Metatheory. Nigam and Miller (2009) showed that cut elimination holds for every subexponential signature, provided the preorder and the unbounded set are compatible — U must be upward closed under ≤ — and that the resulting calculi admit a complete focused proof system, so the entire family shares one focusing theorem rather than requiring a separate proof per signature. Subexponentials are not definable in ordinary linear logic: two indices with the same structural rules need not be provably equivalent, which is the same non-canonicity that ! already has, here made explicit and put to work. The gain is expressive rather than deductive — a signature encodes locations, phases or security levels directly in the modality, so that proof search in the subexponential calculus simulates systems that would otherwise need an external scheduler. Chaudhuri established that the classical and intuitionistic presentations agree on provability for the fragments used in logic programming.

Applies to. Linear logic frameworks and specification logics. Encoding sequent calculi and proof systems inside a logical framework. Linear logic programming (Lolli, Forum) and proof search. Concurrent constraint programming. Modelling location, phase, time and security level as modalities.

Limitations. The logic supplies no modalities of its own: every result is relative to a signature, and a signature that is not upward closed breaks cut elimination, so the calculus does not by itself guarantee that a chosen family of modalities is coherent. Promotion is the bottleneck — !ₐ can be introduced only when every formula in the context sits at an index above a — so formulas at incomparable indices cannot be combined, and there is no rule that moves a formula between indices except along the preorder. Adding bounded and unbounded indices in the same signature inherits the undecidability of full propositional linear logic, so provability is undecidable in general and the complexity of any particular family depends on the signature rather than on the framework. Absorption runs only downward: !ₐA does not entail !_bA for a ≤ b, so information cannot be promoted to a stronger modality.