pith. sign in

arxiv: 2606.03369 · v1 · pith:L2FC4XJYnew · submitted 2026-06-02 · 💻 cs.LO · math.CT· math.LO

A calculus of types in Isbell nuclei

Juan Luis Gastaldi (D-GESS , SPHERE UMR 7219) , Samantha Jarvis , Thomas Seiller (CNRS , JFLI , LIPN) , John Terilla This is my paper

Pith reviewed 2026-06-28 08:01 UTC · model grok-4.3

classification 💻 cs.LO math.CTmath.LO
keywords linear logicrealisabilityIsbell dualityLambek calculusorthogonalityexecutiontypesnucleus
0
0 comments X

The pith

Orthogonality-closed types coincide exactly with fixed points of the adjunction from a quantitative relation.

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

The paper equates two type-generation methods that start from an associative execution operation and a real-valued measurement with no further compatibility. One method closes sets under orthogonality defined by the measurement's failure to add; the other takes fixed points of the adjunction induced by the same measurement as a quantitative relation. These two constructions select identical collections of types. The identification yields a product on types that is associative only after the types are made sensitive to both sides of any composite; when execution possesses units the resulting structure carries left and right residuals. The reverse direction shows that each such type itself induces a new quantitative relation whose generated types again coincide with the original collection via the residuals.

Core claim

Given an associative product called execution and a real-valued measurement, the biorthogonally closed subsets obtained by testing interactions via the measurement are precisely the fixed points of the adjunction whose nucleus is formed from that same measurement. This common collection of objects carries a product that fails to be associative under the most direct definition; repairing associativity requires a refined notion of type that records both input and output sides. The refined product is associative and, when units exist for execution, admits two residuals. Each type further generates its own quantitative relation, producing a derived adjunction whose types recover the original col

What carries the argument

The adjunction induced by the measurement whose fixed points are the types; this adjunction is shown to select exactly the same objects as the biorthogonal closure under the orthogonality relation defined by the same measurement.

If this is right

  • The direct product on orthogonality-closed sets is not associative.
  • A refined notion of type, recording both sides of a composite, restores associativity and supplies two residuals when execution has units.
  • Every type induces a further quantitative relation whose generated types coincide with the original collection via the residuals.
  • The threefold arrangements of types, products, and residuals satisfy a coherence theorem.
  • Explicit product formulas exist when the underlying space is finite-dimensional.

Where Pith is reading between the lines

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

  • The emergence of a Lambek calculus from minimal execution-plus-measurement data suggests that similar calculi may appear in any realisability model whose measurement is non-additive.
  • The residual operations could be used to compute types iteratively without enumerating all biorthogonal closures directly.
  • The construction may apply to models in which execution lacks units, yielding a one-sided version of the calculus.

Load-bearing premise

The measurement is not additive, and this single non-additivity simultaneously supplies the orthogonality relation and the quantitative relation whose nucleus is taken.

What would settle it

An explicit associative execution and measurement for which some biorthogonally closed set fails to be a fixed point of the induced adjunction, or vice versa.

read the original abstract

We identify two constructions from different mathematical traditions. In linear logic and realisability, logical types are generated rather than fixed in advance: one begins with a universe of realisers equipped with execution, uses orthogonality to test their interactions, and takes types to be the biorthogonally closed subsets. In enriched Isbell duality, a quantitative relation induces an adjunction whose fixed points form a category, its nucleus. These constructions proceed by different means; we show that, in the present setting, they produce the same objects. The shared datum is minimal: an associative product, called execution, and a real-valued measurement, with no compatibility assumed between them. The failure of the measurement to be additive is at once the relation defining orthogonality and the quantitative relation whose Isbell nucleus we form, and the types cut out by orthogonality are exactly the fixed points of the associated adjunction. The identification pays off in both directions. The most natural product of types fails to be associative; repairing this failure forces a different notion of type, sensitive to both sides of a composite, on which the induced product is associative and, when execution has units, carries two residuals. What emerges is a noncommutative Lambek calculus, derived directly from execution and orthogonality rather than imposed. In the reverse direction, each such type, read on the categorical side, generates a quantitative relation of its own, and with it a derived adjunction and a further generation of types; these derived types are again types of the original situation, computed by the residuals of the Lambek calculus. We also prove a coherence theorem for the threefold arrangements of this construction and, in the finite-dimensional case, give explicit formulas for the product.

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

2 major / 2 minor

Summary. The paper identifies biorthogonal types (closed subsets under orthogonality induced by non-additivity of a real-valued measurement on an associative execution) with the fixed points of the adjunction arising from the enriched Isbell nucleus of the quantitative relation. Under minimal assumptions (only associativity of execution, no compatibility between execution and measurement), these coincide; the identification yields a noncommutative Lambek calculus whose product is associative (with residuals when units exist), a coherence theorem for threefold arrangements, and explicit product formulas in the finite-dimensional case. Derived adjunctions from types generate further types that coincide with residuals of the Lambek calculus.

Significance. If the central identification holds, the work unifies two independent traditions (biorthogonality in realizability/linear logic and Isbell nuclei in enriched category theory) and derives a Lambek calculus directly from execution and orthogonality rather than imposing it. The minimal shared datum and the reverse-direction generation of types via residuals are notable strengths; the coherence result and finite-dimensional formulas add concrete value.

major comments (2)
  1. [Abstract (setup and main identification)] The central claim (biorthogonals exactly equal Isbell fixed points) rests on the relation R derived from non-additivity defining a valid enriched profunctor so that the induced adjunction exists and its nucleus matches the biorthogonal closure. With only associativity of execution stated and 'no compatibility assumed,' it is unclear whether the left/right adjoints are guaranteed to exist or whether their fixed points coincide with the biorthogonals without additional implicit structure on the measurement (e.g., monotonicity or boundedness). This is load-bearing for the equivalence and the subsequent Lambek calculus derivation.
  2. [Lambek calculus construction (post-identification)] The derivation of the noncommutative Lambek calculus (associative product on the refined types, residuals when units exist) follows from the identification; if the adjunction/fixed-point equality requires extra axioms not listed among the 'minimal' assumptions, the claim that the calculus 'emerges directly from execution and orthogonality rather than imposed' needs re-examination in the relevant theorem statement.
minor comments (2)
  1. Notation for the execution product and the real-valued measurement should be introduced with explicit symbols and domains before the orthogonality relation is defined.
  2. The coherence theorem for 'threefold arrangements' would benefit from a brief statement of what the three arrangements are before the theorem is stated.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and constructive comments. The two major comments concern the sufficiency of the stated minimal assumptions for the central identification and the subsequent derivation of the Lambek calculus. We respond point by point below.

read point-by-point responses

  1. Referee: [Abstract (setup and main identification)] The central claim (biorthogonals exactly equal Isbell fixed points) rests on the relation R derived from non-additivity defining a valid enriched profunctor so that the induced adjunction exists and its nucleus matches the biorthogonal closure. With only associativity of execution stated and 'no compatibility assumed,' it is unclear whether the left/right adjoints are guaranteed to exist or whether their fixed points coincide with the biorthogonals without additional implicit structure on the measurement (e.g., monotonicity or boundedness). This is load-bearing for the equivalence and the subsequent Lambek calculus derivation.

    Authors: The manuscript proves that the relation R induced by non-additivity of the measurement defines an enriched profunctor under precisely the stated assumptions (associativity of execution alone). The left and right adjoints exist by the standard construction for enriched profunctors in this quantitative setting, and their fixed points are shown to coincide exactly with the biorthogonal closures in Theorem 4.2. No monotonicity, boundedness, or other compatibility between execution and measurement is used or required; the non-additivity supplies the quantitative relation directly. The proofs are self-contained in Sections 3 and 4. revision: no

  2. Referee: [Lambek calculus construction (post-identification)] The derivation of the noncommutative Lambek calculus (associative product on the refined types, residuals when units exist) follows from the identification; if the adjunction/fixed-point equality requires extra axioms not listed among the 'minimal' assumptions, the claim that the calculus 'emerges directly from execution and orthogonality rather than imposed' needs re-examination in the relevant theorem statement.

    Authors: Because the identification of biorthogonals with Isbell fixed points is established under the listed minimal assumptions, the Lambek calculus (associative product and residuals) is derived directly from those objects in Section 5 without introducing further axioms. The relevant theorem statements therefore require no re-examination; the emergence claim is accurate as written. revision: no

Circularity Check

0 steps flagged

No circularity: equivalence of biorthogonals and Isbell nuclei is a proved identification between independent constructions

full rationale

The paper takes an associative execution and a real-valued measurement (with non-additivity defining the relation) as shared minimal inputs, then proves that the resulting biorthogonally closed sets coincide with the fixed points of the induced adjunction. This identification is presented as a theorem to be shown, not as a definitional equivalence or a fitted parameter renamed as a prediction. From the proved equivalence the noncommutative Lambek calculus is derived; the derivation therefore rests on the content of the proof rather than on any of the enumerated circular patterns. No self-citation is invoked as load-bearing justification for the central step, and the constructions originate in distinct traditions. The result is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard assumptions from linear logic, realizability, and enriched category theory. The key inputs are the associative execution product and the real-valued measurement whose non-additivity is used directly.

axioms (2)
  • domain assumption Execution is associative
    Stated explicitly as part of the minimal shared datum in the abstract.
  • domain assumption A real-valued measurement exists whose failure to be additive defines the relations
    The measurement is the shared datum that simultaneously induces orthogonality and the quantitative relation for the Isbell nucleus.

pith-pipeline@v0.9.1-grok · 5869 in / 1443 out tokens · 29163 ms · 2026-06-28T08:01:14.001622+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

27 extracted references · 1 canonical work pages · 1 internal anchor

  1. [1]

    12, 306--347

    Tom Avery and Tom Leinster, Isbell conjugacy and the reflexive completion, Theory and Applications of Categories 36 (2021), no. 12, 306--347

    2021

  2. [2]

    2, 174--185

    Tai‑Danae Bradley, Juan Luis Gastaldi, and John Terilla, The structure of meaning in language: Parallel narratives in linear algebra and category theory, Notices of the American Mathematical Society 71 (2024), no. 2, 174--185

    2024

  3. [3]

    2, 551--580

    Tai-Danae Bradley, John Terilla, and Yiannis Vlassopoulos, An enriched category theory of language: From syntax to semantics, La Matematica 1 (2022), no. 2, 551--580

    2022

  4. [4]

    37, 1256--1281

    Tai-Danae Bradley and Juan Pablo Vigneaux, The magnitude of categories of texts enriched by language models, Theory and Applications of Categories 44 (2025), no. 37, 1256--1281

    2025

  5. [5]

    Mike Develin and Bernd Sturmfels, Tropical convexity, Documenta Mathematica 9 (2004), 1--27

    2004

  6. [6]

    thesis, University of Sheffield, Sheffield, UK, 2017

    Jonathan Arthur Elliott, On the fuzzy concept complex, Ph.D. thesis, University of Sheffield, Sheffield, UK, 2017

    2017

  7. [7]

    Soichiro Fujii, Enriched categories and tropical mathematics, arXiv e-prints (2019)

    2019

  8. [8]

    1, 1--101

    Jean-Yves Girard, Linear logic, Theoretical Computer Science 50 (1987), no. 1, 1--101

    1987

  9. [9]

    , Locus solum: From the rules of logic to the logic of rules, Mathematical Structures in Computer Science 11 (2001), no. 3

    2001

  10. [10]

    , Theoretical Computer Science 412 (2011), 1860--1883

    Jean-Yves Girard, Geometry of interaction V : Logic in the hyperfinite factor. , Theoretical Computer Science 412 (2011), 1860--1883

    2011

  11. [11]

    Juan Luis Gastaldi, Samantha Jarvis, Thomas Seiller, and John Terilla, Projective metric geometry of tropical nuclei: gap matrices, event loci, and order chambers, arXiv e-prints (2026), arXiv:2601.07900

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  12. [12]

    St \'e phane Gaubert and Yiannis Vlassopoulos, Directed metric structures arising in large language models, arXiv e-prints (2024)

    2024

  13. [13]

    J. R. Isbell, Adequate subcategories, Illinois Journal of Mathematics 4 (1960), no. 4, 541--552

    1960

  14. [14]

    Jarvis, A novel closed monoidal structure on the nucleus of a profunctor, Ph.D

    Samantha K. Jarvis, A novel closed monoidal structure on the nucleus of a profunctor, Ph.D. thesis, The Graduate Center, City University of New York, June 2025, Doctoral dissertation (Ph.D.), Mathematics; advisor: John Terilla

    2025

  15. [15]

    Max Kelly, Basic concepts of enriched category theory, London Mathematical Society Lecture Note Series, vol

    G. Max Kelly, Basic concepts of enriched category theory, London Mathematical Society Lecture Note Series, vol. 64, Cambridge University Press, 1982, Reprinted in: Reprints in Theory and Applications of Categories, No. 10, 2005

    1982

  16. [16]

    Kleene, On the interpretation of intuitionistic number theory, Journal of Symbolic Logic 10 (1945)

    Stephen C. Kleene, On the interpretation of intuitionistic number theory, Journal of Symbolic Logic 10 (1945)

    1945

  17. [17]

    Co., 1959, pp

    Georg Kreisel, Interpretation of analysis by means of constructive functionals of finite types, Constructivity in mathematics (Arend Heyting, ed.), North-Holland Pub. Co., 1959, pp. 101--128

    1959

  18. [18]

    Jean-Louis Krivine, Realizability in classical logic, Panoramas et synth \`e ses 27 (2009), 197--229

    2009

  19. [19]

    3, 154--170

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

    1958

  20. [20]

    F. William Lawvere, Metric spaces, generalized logic, and closed categories, Rendiconti del Seminario Matematico e Fisico di Milano 43 (1973), 135--166, Reprinted in Reprints in Theory and Applications of Categories, No. 1 (2002), pp. 1--37

    1973

  21. [21]

    Thomas Seiller, Interaction graphs: Multiplicatives, Annals of Pure and Applied Logic 163 (2012), 1808--1837

    2012

  22. [22]

    Thomas Seiller, Interaction graphs: Additives, Annals of Pure and Applied Logic 167 (2016), 95 -- 154

    2016

  23. [23]

    thesis, Sorbonne Paris Nord University, 2024, Habilitation thesis

    Thomas Seiller, Mathematical I nformatics , Ph.D. thesis, Sorbonne Paris Nord University, 2024, Habilitation thesis

    2024

  24. [24]

    Jaap van Oosten, Realizability, volume 152: An introduction to its categorical side, Elsevier Science, San Diego, CA, USA, 2008

    2008

  25. [25]

    22, 696--732

    Simon Willerton, Tight spans, I sbell completions and semi-tropical modules , Theory and Applications of Categories 28 (2013), no. 22, 696--732

    2013

  26. [26]

    , Galois correspondences and enriched adjunctions, February 2014, Blog post

    2014

  27. [27]

    , The L egendre- F enchel transform from a category theoretic perspective , arXiv e-prints (2015)

    2015