Dialectica Categories for the Lambek Calculus
Valeria de Paiva, Harley Eades III

TL;DR
This paper revisits dialectica models for the Lambek Calculus, extends it with modalities to recover classical logic features, and proves categorical semantics with key properties like normalization.
Contribution
It completes the dialectica models for the Lambek Calculus, introduces modalities to recover classical logic features, and establishes soundness, completeness, and key type system properties.
Findings
Dialectica models for Lambek Calculus are completed and verified.
Extended calculus with ppa and ! modalities supports classical logic features.
Proved subject reduction, Church-Rosser, and normalization for the extended calculus.
Abstract
We revisit the old work of de Paiva on the models of the Lambek Calculus in dialectica models making sure that the syntactic details that were sketchy on the first version got completed and verified. We extend the Lambek Calculus with a \kappa modality, inspired by Yetter's work, which makes the calculus commutative. Then we add the of-course modality !, as Girard did, to re-introduce weakening and contraction for all formulas and get back the full power of intuitionistic and classical logic. We also present the categorical semantics, proved sound and complete. Finally we show the traditional properties of type systems, like subject reduction, the Church-Rosser theorem and normalization for the calculi of extended modalities, which we did not have before.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
