Adjoint Logic

Origin. Nick Benton, "A mixed linear and non-linear logic: proofs, terms and models" (CSL 1994, LNCS 933, 1995), which presented intuitionistic and linear logic as two judgments related by a monoidal adjunction whose round trip is the exponential !; Jason Reed, "A judgmental deconstruction of modal logic" (2009, unpublished manuscript — the title plays on Pfenning and Davies' "A judgmental reconstruction of modal logic"), which derived □ and the lax ○ from adjoint pairs and parametrized the construction over a preorder of modes; Daniel Licata and Michael Shulman, "Adjoint logic with a 2-category of modes" (LFCS 2016), generalizing the adjoint logics of Benton and Wadler (1994, 1996) and Reed (2009) to many adjunctions between the same modes; Licata, Shulman, and Mitchell Riley, "A fibrational framework for substructural and modal logics" (FSCD 2017); Klaas Pruiksma and Frank Pfenning, "A message-passing interpretation of adjoint logic" (PLACES 2019; journal version in JLAMP 120, 2021).

Models. Logics and type theories parametrized by an adjunction structure between modes. A mode is a judgment with its own structural discipline — cartesian, linear, ordered, lax — and a modality is not a primitive operator but the composite of an adjoint pair F ⊣ U passing between two modes. What modal logics stipulate, the adjunction supplies: a round trip through a stronger mode is a comonad, a round trip through a weaker mode is a monad, and the unit, counit, and triangle identities yield the axioms Hilbert systems postulate. One framework produces !, □, ◇, ○, and the substructural connectives as instances, which makes it the organizing account behind Intuitionistic Linear Logic's exponential and behind the mode theories of Modal Type Theory.

Formalism.

Modes: Every proposition and hypothesis carries a mode; the mode fixes which structural rules its context admits. Reed: a preorder of modes, and for each related pair an adjoint pair F ⊣ U passing between the two judgments.

LNL (Benton 1994): Two judgments: Θ ⊢ X (intuitionistic; weakening and contraction hold) and Θ; Δ ⊢ A (linear; Δ used exactly once). F takes intuitionistic types to linear ones, G linear to intuitionistic; F ⊣ G, and the adjunction is monoidal.

Θ ⊢ X Θ; · ⊢ A ──────────── F ──────────── G Θ; · ⊢ F X Θ ⊢ G A

!A = F(G A): dereliction !A ⊢ A is the counit, digging !A ⊢ !!A comes from the unit, and weakening and contraction for ! come from the cartesian side, where they are free.

Reed's deconstruction (2009): Pfenning–Davies validity is a mode above truth; □A = F(U A), the comonad of that adjunction. The empty-context condition on □I is the discipline of the adjunction, not a stipulation. Lax truth is a mode below truth; ○A = U(F A), the monad of lax logic. The same scheme reaches Pfenning–Davies possibility ◇, linear logic's !, and labelled deduction.

Mode theories as 2-categories (Licata–Shulman 2016): Modes are objects; modalities are 1-cells, each inducing an adjoint pair; 2-cells are the axioms relating modalities. Multiple adjunctions may relate the same two modes — what a preorder cannot say. The motivating instance is cohesive homotopy type theory's adjoint modality pair ♭ ⊣ ♯.

The fibrational framework (Licata–Shulman–Riley 2017): A sequent calculus parametrized by a mode theory: contexts are terms over the modes, and a structural rule holds exactly where the mode theory's equations and 2-cells say so. Two general connectives, one positive and one negative, whose instances are ⊗, ⊸, cartesian product and implication, monads, comonads, adjoint pairs, n-linear variables, and bunched implications. Non-associative, ordered, linear, affine, relevant, and cartesian systems are choices of mode theory, not separate calculi.

Message passing (Pruiksma–Pfenning 2019): Adjoint logic over a mode hierarchy as a session-type system; propositions are protocols, proofs are processes. A semi-axiomatic sequent calculus — noninvertible rules become axioms — makes cut reduction asynchronous communication. Modes with weakening and contraction type replicable services; linear modes type one-use channels.

Symbols.

Symbol	Unicode	Name	Meaning
F	U+0046	Latin capital letter F	The left adjoint, from the stronger mode down
U	U+0055	Latin capital letter U	The right adjoint, from the weaker mode up
G	U+0047	Latin capital letter G	Benton's name for the right adjoint of LNL
⊣	U+22A3	Left tack	F ⊣ U: F is left adjoint to U
!	U+0021	Exclamation mark / Of course	The linear exponential, F∘G
□	U+25A1	White square / Box	Necessity, F∘U
○	U+25CB	White circle	Lax truth, U∘F
◇	U+25C7	White diamond	Possibility, in Reed's extension
♭	U+266D	Music flat sign	Left half of cohesion's adjoint modality pair
♯	U+266F	Music sharp sign	Right half of that pair
⊗	U+2297	Tensor	Multiplicative conjunction at a linear mode
⊸	U+22B8	Linear implication	Implication at a linear mode
∘	U+2218	Ring operator	Composition of the two adjoints
⊢	U+22A2	Turnstile	The judgment, mode by mode
Θ	U+0398	Greek capital theta	LNL's intuitionistic context
Δ	U+0394	Greek capital delta	LNL's linear context
·	U+00B7	Middle dot	The empty linear context
μ	U+03BC	Greek small mu	A 1-cell of the mode theory
LNL	—	Linear/non-linear logic	Benton's founding system

Metatheory. Benton proved the equivalence that made the adjunction the standard model of the exponential: a symmetric monoidal adjunction between a cartesian closed category and a symmetric monoidal closed one induces a linear exponential comonad, and the models in the earlier Benton–Bierman–de Paiva–Hyland sense are exactly these — the LNL presentation and the comonad presentation agree, and the adjoint one is the simpler to state and to check, which is why the Intuitionistic Linear Logic entry records it as the model that stuck. Licata, Shulman, and Riley proved cut and identity admissible independently of the mode theory, so every instance — ordered, linear, affine, relevant, cartesian, bunched, and the modal decompositions — inherits cut elimination at once instead of proving it per system. Reed's result is that Pfenning and Davies' □ and lax ○ are the two composites of adjunctions between judgments of differing strength, so S4's comonad laws — T from the counit, 4 from comultiplication — are theorems about round trips: the comonad reading that Modal Type Theory records is here derived rather than postulated. The decomposition continues to generalize: "A mixed linear and graded logic: proofs, terms, and models" (Vollmer and coauthors, CSL 2025) splits graded modalities by the same adjoint resolution.

Applies to. The exponential of linear logic, wherever it is modelled. Modal type systems in the Pfenning–Davies line. Session types and message-passing concurrency, through the Pruiksma–Pfenning interpretation. Cohesive and multimodal homotopy type theory — MTT's mode theories are this framework carried to dependent types. Graded modal systems by the same resolution. Languages combining several substructural disciplines, with modes mediating between them.

Limitations. The framework is intuitionistic and single-conclusion: the fibrational calculus covers the intuitionistic substructural and modal logics, and classical linear logic's involutive duality has no place in it. The mode theory is an input, not an output — cut elimination holds for whatever 2-category is supplied, but finding the mode theory that yields a given target logic, and proving that the instance coincides with the known system, is work done per system; this is the same situation the Modal Type Theory entry reports for MTT's 2-categorical prelude. And the decomposition reaches only one level down: the shifts F and U are themselves primitive, so an axiom about □ becomes a choice of mode theory rather than a theorem of the framework, and the question of which mode theory is right for a given application is answered outside the logic.