Dialectica categories for the Lambek calculus

DOI10.1007/978-3-319-72056-2_16MaRDI QIDQ1709707zbMATH OpenOpenAlexFDO

Authors Harley Eades III, Valeria de Paiva

Publication date 6 April 2018

Full work available at URL https://arxiv.org/abs/1801.06883

zbMATH Keywords

categorical semanticsDialectica modelsLambek calculuslinear logicnon-commutativestructural rulestype theory

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical logic, topoi (03G30)

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.

Recommendations

• On the Lambek calculus with an exchange modality
• scientific article; zbMATH DE number 757643
• Joachim Lambek: the interplay of mathematics, logic, and linguistics
• A Concrete Categorical Model for the Lambek Syntactic Calculus
• Categorical Vector Space Semantics for Lambek Calculus with a Relevant Modality

Cited in

(10)

• Morphisms of open games
• Non-normal modal logics and conditional logics: semantic analysis and proof theory
• Linear logic model of state revisited
• scientific article; zbMATH DE number 757643 (Why is no real title available?)
• Final Dialgebras: From Categories to Allegories
• On the Lambek calculus with an exchange modality
• Modal functional (``Dialectica) interpretation
• Categorical models of the differential λ-calculus
• The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions
• Relational Models for the Lambek Calculus with Intersection and Constants

This page was built for publication: Dialectica categories for the Lambek calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1709707)