pith. sign in

arxiv: 2605.19112 · v1 · pith:7VSR7G55new · submitted 2026-05-18 · 💻 cs.LO · cs.PL

Ordered Adjoint Logic (Extended Version)

Sophia Roshal , Frank Pfenning This is my paper

Pith reviewed 2026-05-20 07:05 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords ordered logicadjoint modalitiescut eliminationsequent calculusnatural deductionproof checkingstructural ruleslogical frameworks
0
0 comments X

The pith

Adjoint modalities combine ordered logics with varying structural properties while preserving cut elimination.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper generalizes prior work on ordered linear logics by using adjoint modalities to mix fine-grained structural rules including weakening, left and right contraction, and left and right mobility. It establishes that the sequent calculus for the resulting system admits cut elimination. The authors also give a natural deduction formulation that makes structural rules implicit and prove that proof checking remains decidable. This setup aims to support more expressive systems for handling ordered resources in type systems and logical frameworks.

Core claim

By defining adjoint modalities that combine logics with arbitrary combinations of weakening, left/right contraction, and left/right mobility, the sequent calculus for ordered adjoint logic admits cut elimination. A corresponding natural deduction system hides the structural rules, and proof checking is decidable, making it suitable for an expressive adjoint programming language or logical framework.

What carries the argument

Adjoint modalities that combine logics with different structural properties (weakening, left/right contraction, left/right mobility) to preserve cut elimination and decidability.

If this is right

  • The sequent calculus for the combined logic admits cut elimination.
  • A natural deduction formulation exists in which structural rules are implicit.
  • Proof checking for the natural deduction system is decidable.
  • The logic provides a foundation for an expressive adjoint programming language or logical framework.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The framework could be applied directly to model resource management in domains such as memory allocation or security protocols mentioned in the abstract.
  • Similar adjoint constructions might extend to other modal or substructural logics while retaining cut elimination.
  • A prototype implementation of the decidable proof checker could reveal practical performance bounds for the natural deduction system.

Load-bearing premise

Adjoint modalities can be defined for arbitrary combinations of the listed structural rules while still preserving cut elimination and related meta-theoretic properties.

What would settle it

A concrete counterexample consisting of one specific combination of weakening, contractions, and mobilities where the sequent calculus fails to admit cut elimination, or an explicit instance where proof checking in the natural deduction system becomes undecidable.

Figures

Figures reproduced from arXiv: 2605.19112 by Frank Pfenning, Sophia Roshal.

Figure 1
Figure 1. Figure 1: Ordered Adjoint Sequent Calculus (structural rules in subsection 2.1) [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Ordered Natural Deduction (explicit structural rules in subsection 3.1) [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Implicit Natural Deduction [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
read the original abstract

Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most formulations, ordered types are also linear, requiring each resource to be used exactly once. Prior work by Kanovich et al. has investigated calculi that relax this constraint through subexponentials within a linear ordered logic. We generalize their work by using adjoint modalities to combine logics with varying fine-grained structural properties, including weakening, left contraction, right contraction, left mobility, and right mobility. We show that the resulting sequent calculus admits cut elimination. We further provide a natural deduction formulation in which structural rules are implicit, and show that proof checking for this system is decidable. This makes it a suitable foundation for an expressive adjoint programming language or logical framework.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper introduces Ordered Adjoint Logic, generalizing Kanovich et al.'s subexponential approach in linear ordered logic by employing adjoint modalities to combine logics with arbitrary combinations of weakening, left/right contraction, and left/right mobility. It presents a sequent calculus for which cut elimination is claimed, along with a natural deduction formulation where structural rules are implicit, and proves that proof checking in this system is decidable.

Significance. If the meta-theoretic results hold, the framework offers a modular way to mix ordered and substructural logics with fine-grained control over resource management and ordering, supporting applications in computational linguistics, security protocols, and logical frameworks. The cut elimination and decidability results provide a solid foundation for an adjoint programming language or type system.

major comments (1)
  1. [§4] §4 (Cut Elimination): The induction for cut elimination must handle all interactions between adjoint modalities and the five structural properties (weakening, left/right contraction, left/right mobility). The manuscript does not enumerate the 32 combinations or supply explicit side-condition lemmas for mixed cases such as left-mobility combined with right-contraction; without these, it is unclear whether every redex is covered by the reduction rules.
minor comments (2)
  1. [Abstract] The abstract and introduction could more explicitly state the precise number of structural combinations supported and reference the corresponding lemmas.
  2. [§2] Notation for adjoint modalities and context splitting should be introduced with a small example derivation in §2 to aid readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading and constructive feedback on the manuscript. We appreciate the recognition of the framework's potential for modular combinations of ordered and substructural logics. We address the major comment below.

read point-by-point responses

  1. Referee: [§4] §4 (Cut Elimination): The induction for cut elimination must handle all interactions between adjoint modalities and the five structural properties (weakening, left/right contraction, left/right mobility). The manuscript does not enumerate the 32 combinations or supply explicit side-condition lemmas for mixed cases such as left-mobility combined with right-contraction; without these, it is unclear whether every redex is covered by the reduction rules.

    Authors: We agree that greater explicitness would strengthen the presentation of the cut-elimination argument. The proof in §4 proceeds by induction on the cut formula and derivation height, with the adjoint modalities ensuring that structural properties are preserved under the defined reductions. The general lemmas for each modality already compose to cover mixed cases. Nevertheless, to remove any ambiguity, we will revise the manuscript to add an appendix that enumerates the principal combinations of the five structural properties and supplies explicit side-condition lemmas for representative mixed cases, including left-mobility combined with right-contraction. This addition will confirm that all redexes are covered without changing the underlying proof strategy. revision: yes

Circularity Check

0 steps flagged

No significant circularity; meta-theoretic proofs are independent

full rationale

The paper's central claims consist of a cut-elimination theorem for the sequent calculus and a decidability result for proof checking in the natural deduction formulation. These are established directly from the definitions of adjoint modalities combining weakening, contraction, and mobility rules, using standard induction techniques on derivations rather than any reduction to fitted parameters, self-definitions, or load-bearing self-citations. Prior work is referenced for context and generalization, but the new results for arbitrary combinations of structural properties do not reduce to those references by construction and remain self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard sequent calculus rules for ordered and linear logics plus the novel adjoint modality definitions. No free parameters are fitted to data as this is pure theory. Axioms include standard properties of adjoints and cut elimination lemmas.

axioms (2)
  • domain assumption Adjoint modalities preserve the structural rules of the combined logics (weakening, contraction, mobility).
    Invoked when defining the combined system in the sequent calculus.
  • standard math The sequent calculus formulation satisfies the standard cut elimination theorem conditions.
    Background result from prior logic literature used to establish the main theorem.

pith-pipeline@v0.9.0 · 5687 in / 1330 out tokens · 26856 ms · 2026-05-20T07:05:06.024649+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

32 extracted references · 32 canonical work pages

  1. [1]

    Substructural parametricity

    C.B.Aberlé,KarlCrary,ChrisMartens,andFrankPfenning. Substructural parametricity. In M. Fernández, editor,10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), pages 4:1–4:21, Birmingham, UK, July 2025. LIPIcs 337

    work page 2025

  2. [2]

    Michele Abrusci and Paul Ruet

    V. Michele Abrusci and Paul Ruet. Non-commutative logic I: The multi- plicative fragment.Annals of Pure and Applied Logic, 101(1):29–64, 1999

    work page 1999

  3. [3]

    P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and mod- els. In L. Pacholski and J. Tiuryn, editors,Selected Papers from the 8th International Workshop on Computer Science Logic (CSL’94), pages 121– 135, Kazimierz, Poland, September 1994. Springer LNCS 933. An extended versionappearsasTechnicalReportUCAM-CL-TR-352,UniversityofCam- bridge

    work page 1994

  4. [4]

    Cutler, Christopher Watson, Emeka Nkurumeh, Phillip Hilliard, Harrison Goldstein, Caleb Stanford, and Benjamin C

    Joseph W. Cutler, Christopher Watson, Emeka Nkurumeh, Phillip Hilliard, Harrison Goldstein, Caleb Stanford, and Benjamin C. Pierce. Stream types. Proceedings of the ACM on Programming Languages, 8(PLDI):1412–1436, 2024

    work page 2024

  5. [5]

    Thestructureof exponentials: Uncovering the dynamics of linear logic proofs

    VincentDanos,Jean-BaptisteJoinet,andHaroldSchellinx. Thestructureof exponentials: Uncovering the dynamics of linear logic proofs. InKurt Gödel Colloquium, pages 159–171, Brno, Czech Republic, August 1993. Springer LNCS 713

    work page 1993

  6. [6]

    PhD thesis, Carnegie Mellon University, December 2020

    Henry DeYoung.Session-Typed Ordered Logical Specifications. PhD thesis, Carnegie Mellon University, December 2020. Available as Technical Report CMU-CS-20-133

    work page 2020

  7. [7]

    Substructural proofs as automata

    Henry DeYoung and Frank Pfenning. Substructural proofs as automata. In A. Igarashi, editor,14th Asian Symposium on Programming Languages and Systems (APLAS’16), pages 3–22, Hanoi, Vietnam, November 2016. Springer LNCS 10017. Invited talk

    work page 2016

  8. [8]

    Untersuchungen über das logische Schließen.Mathema- tische Zeitschrift, 39:176–210, 405–431, 1935

    Gerhard Gentzen. Untersuchungen über das logische Schließen.Mathema- tische Zeitschrift, 39:176–210, 405–431, 1935. English translation in M. E. Szabo, editor,The Collected Papers of Gerhard Gentzen, pages 68–131, North-Holland, 1969

    work page 1935

  9. [9]

    Linear logic.Theoretical Computer Science, 50:1–102, 1987

    Jean-Yves Girard. Linear logic.Theoretical Computer Science, 50:1–102, 1987

    work page 1987

  10. [10]

    Security reasoning via substructural dependency tracking.Proceedings of the ACM on Pro- gramming Languages, 10 (POPL):777–805, January 2026

    Hemant Gouni, Frank Pfenning, and Jonathan Aldrich. Security reasoning via substructural dependency tracking.Proceedings of the ACM on Pro- gramming Languages, 10 (POPL):777–805, January 2026

    work page 2026

  11. [11]

    Combining dependency, grades, and adjoint logic

    Peter Hanukaev and Harley Eades, III. Combining dependency, grades, and adjoint logic. In8th Workshop on Type-Driven Development (TyDe 2023), pages58–70,Seattle,Washington,2023.ACM. URL:https://arxiv.org/ abs/2307.09563

    work page arXiv 2023

  12. [12]

    Ad- joint natural deduction

    Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka. Ad- joint natural deduction. In Jakob Rehof, editor,9th International Confer- Ordered Adjoint Logic 17 ence on Formal Structures for Computation and Deduction (FSCD 2024), pages 15:1–15:23, Tallinn, Estonia, July 2024. LIPIcs 299. Extended version available ashttps://arxiv.org/abs/2402.01428

    work page arXiv 2024

  13. [13]

    A log- ical framework with commutative and non-commutative subexponentials

    Max Kanovich, Stepan Kuznetsov, Vivek Nigam, and Andre Scedrov. A log- ical framework with commutative and non-commutative subexponentials. InInternational Joint Conference on Automated Reasoning (IJCAR 2018), pages 228–245. Springer LNAI 10900, 2018

    work page 2018

  14. [14]

    Subexponentials in non-commutative linear logic.Mathematical Structure in Computer Science, 29(8):1217–1249, 2019

    Max Kanovich, Stepan Kuznetsov, Vivek Nigam, and Andre Scedrov. Subexponentials in non-commutative linear logic.Mathematical Structure in Computer Science, 29(8):1217–1249, 2019

    work page 2019

  15. [15]

    The mathematics of sentence structure.The American Mathematical Monthly, 65(3):154–170, 1958

    Joachim Lambek. The mathematics of sentence structure.The American Mathematical Monthly, 65(3):154–170, 1958

    work page 1958

  16. [16]

    Licata and Michael Shulman

    Daniel R. Licata and Michael Shulman. Adjoint logic with a 2-category of modes. InInternational Symposium on Logical Foundations of Computer Science (LFCS), pages 219–235. Springer LNCS 9537, January 2016

    work page 2016

  17. [17]

    Non-commutative logic III: Focusing proofs

    Roberto Maieli and Paul Ruet. Non-commutative logic III: Focusing proofs. Information and Computation, 185(2):233–262, 2003

    work page 2003

  18. [18]

    An extended framework for specifying and reasoning about proof systems.Journal of Logic and Computation, 26(2):539–576, 2016

    Vivek Nigam, Elaine Pimental, and Giselle Reis. An extended framework for specifying and reasoning about proof systems.Journal of Logic and Computation, 26(2):539–576, 2016

    work page 2016

  19. [19]

    Substructural logics, Fall 2023

    Frank Pfenning. Substructural logics, Fall 2023. Course materials includ- ing lecture notes available athttps://www.cs.cmu.edu/~fp/courses/ 15836-f23/

    work page 2023

  20. [20]

    Frank Pfenning and Robert J. Simmons. Substructural operational seman- tics as ordered logic programming. InProceedings of the 24th Annual Sym- posium on Logic in Computer Science (LICS 2009), pages 101–110, Los Angeles, California, August 2009. IEEE Computer Society Press

    work page 2009

  21. [21]

    PhD thesis, Depart- ment of Computer Science, Carnegie Mellon University, August 2001

    Jeff Polakow.Ordered Linear Logic and Applications. PhD thesis, Depart- ment of Computer Science, Carnegie Mellon University, August 2001

    work page 2001

  22. [22]

    Natural deduction for intuitionistic non- commutative linear logic

    Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non- commutative linear logic. In4th International Conference on Typed Lambda Calculi and Applications (TLCA’99), pages 295–309, L’Aquila, Italy, April

    work page

  23. [23]

    Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic

    Jeff Polakow and Frank Pfenning. Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. In Andre Scedrov and Achim Jung, editors,Proceedings of the 15th Conference on Mathemat- ical Foundations of Programming Semantics, pages 449–466, New Orleans, Louisiana, April 1999. Electronic Notes in Theoretical Computer Sci...

    work page 1999

  24. [24]

    Properties of terms in continuation- passing style in an ordered logical framework

    Jeff Polakow and Frank Pfenning. Properties of terms in continuation- passing style in an ordered logical framework. In Joëlle Despeyroux, editor, 2nd Workshop on Logical Frameworks and Meta-languages (LFM’00), Santa Barbara, California, June 2000. Proceedings available as INRIA Technical Report

    work page 2000

  25. [25]

    PhD thesis, Carnegie Mellon University, 2024

    Klaas Pruiksma.Adjoint Logic with Applications. PhD thesis, Carnegie Mellon University, 2024. Available as Technical Report CMU-CS-24-103. 18 S. Roshal and F. Pfenning

    work page 2024

  26. [26]

    Adjoint logic

    Klaas Pruiksma, Willow Chargin, Frank Pfenning, and Jason Reed. Adjoint logic. Unpublished manuscript, April 2018. URL:http://www.cs.cmu. edu/~fp/papers/adjoint18b.pdf

    work page 2018

  27. [27]

    A message-passing interpretation of adjoint logic.Journal of Logical and Algebraic Methods in Programming, 120(100637), 2021

    Klaas Pruiksma and Frank Pfenning. A message-passing interpretation of adjoint logic.Journal of Logical and Algebraic Methods in Programming, 120(100637), 2021

    work page 2021

  28. [28]

    A judgmental deconstruction of modal logic

    Jason Reed. A judgmental deconstruction of modal logic. Unpub- lished manuscript, May 2009. URL:http://www.cs.cmu.edu/~jcreed/ papers/jdml2.pdf

    work page 2009

  29. [29]

    Non-commutative logic II: Sequent calculus and phase seman- tics.Mathematical Structures in Computer Science, 10(2):277–312, 2000

    Paul Ruet. Non-commutative logic II: Sequent calculus and phase seman- tics.Mathematical Structures in Computer Science, 10(2):277–312, 2000

    work page 2000

  30. [30]

    Simmons.Substructural Logical Specifications

    Robert J. Simmons.Substructural Logical Specifications. PhD thesis, Carnegie Mellon University, November 2012. Available as Technical Report CMU-CS-12-142

    work page 2012

  31. [31]

    A mixed lin- ear and graded logic: Proofs, terms, and models

    Victorial Vollmer, Danielle Marshall, and Harley Eades, III. A mixed lin- ear and graded logic: Proofs, terms, and models. In33rd Conference on Computer Science Logic (CSL 2025), pages 32:1–32:21, Amsterdam, The Netherlands, February 2025. LIPIcs 326

    work page 2025

  32. [32]

    David N. Yetter. Quantales and (noncommutative) linear logic.The Journal of Symbolic Logic, 55(1):41–64, 1990

    work page 1990