Dialectica Categories for the Lambek Calculus

In Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS 2018). Deerfield Beach, FL, USA: (2018)

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 κ 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.
Keywords Lambek calculus  categorical semantics  dialectica category
Categories (categorize this paper)
Buy the book Find it on Amazon.com
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 60,992
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

A Note on the Lambek-van Benthem Calculus.Wojciech Buszkowski - 1984 - Bulletin of the Section of Logic 13 (1):31-35.
Language-Theoretic and Finite Relation Models for the (Full) Lambek Calculus.Christian Wurm - 2017 - Journal of Logic, Language and Information 26 (2):179-214.
A Brief Survey of Frames for the Lambek Calculus.Kosta Došen - 1992 - Mathematical Logic Quarterly 38 (1):179-187.
The Lambek Calculus Enriched with Additional Connectives.Makoto Kanazawa - 1992 - Journal of Logic, Language and Information 1 (2):141-171.
On the Recognizing Power of the Lambek Calculus with Brackets.Makoto Kanazawa - 2018 - Journal of Logic, Language and Information 27 (4):295-312.
Syntactic Calculus with Dependent Types.Aarne Ranta - 1998 - Journal of Logic, Language and Information 7 (4):413-431.

Analytics

Added to PP index
2020-05-10

Total views
0

Recent downloads (6 months)
0

How can I increase my downloads?

Downloads

Sorry, there are not enough data points to plot this chart.

My notes