---
title: "Deductive Systems and Categories I. Syntactic Calculus and Residuated Categories"
authors:
  - "Joachim Lambek"
year: 1968
venue: "Mathematical Systems Theory"
arxiv: null
doi: "10.1007/BF01702865"
source: "https://doi.org/10.1007/BF01702865"
topics:
  - category-theory
  - logic
  - linguistics
  - residuation
seed_rank: 161
seed_batch: "prefill-2026-08-13"
reviewed: "2026-08-13"
pool: "maths-foundations"
relevance_score: 9
cites:
  - title: "The Mathematics of Sentence Structure"
    url: "https://doi.org/10.1080/00029890.1958.11991991"
    year: 1958
    arxiv: null
    doi: "10.1080/00029890.1958.11991991"
see:
  - "163-the-mathematics-of-sentence-structure"
---

# Deductive Systems and Categories I. Syntactic Calculus and Residuated Categories

## One-sentence takeaway

Lambek recasts his syntactic calculus as the internal language of residuated categories, so grammatical cancellation is residual adjointness rather than a one-off type-arithmetic trick.

## Why it matters here

NL game-command grammars and Japanese-informed morphology want this: left and right residuals are the two slashes of categorial grammar, and the category is the semantics of “which phrases compose.”

## Key ideas

- The syntactic calculus of types with product and two residuals (\(\backslash\), \(/\)) is given a categorical semantics in residuated monoidal categories.
- A residuated category has a tensor whose left and right residuals are adjoints, matching the introduction and elimination rules of the Lambek calculus.
- Deductive systems are treated as presentations of categories, so cut and composition are the same operation.
- Completeness and coherence results connect provability in the calculus to the existence of morphisms.
- This paper is the categorical companion to the 1958 sentence-structure calculus, not a replacement for it.

## Caveats

## Links

- DOI: [10.1007/BF01702865](https://doi.org/10.1007/BF01702865)