Hostname: page-component-6bf8c574d5-vmclg Total loading time: 0 Render date: 2025-02-21T06:17:45.574Z Has data issue: false hasContentIssue false

Pontrjagin duality and full completeness for multiplicative linear logic (without Mix)

Published online by Cambridge University Press:  01 April 2000

MASAHIRO HAMANO
Affiliation:
School of Information Science, Japan Advanced Institute of Science and Technology, 1-1 Asahidai, Tatsunokuchi, Ishikawa, 923-1292, JAPAN. Email: hamano@jaist.ac.jp
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We prove a full completeness theorem for MLL without the Mix rule. This is done by interpreting a proof as a dinatural transformation in a *-autonomous category of reflexive topological abelian groups first studied by Barr, denoted [Rscr ][Tscr ][Ascr ]. In Section 2, we prove the unique interpretation theorem for a binary provable MLL-sequent. In Section 3, we prove a completeness theorem for binary sequents in MLL without the Mix rule, where we interpret formulas in the category [Rscr ][Tscr ][Ascr ]. The theorem is proved by investigating the concrete structure of [Rscr ][Tscr ][Ascr ], especially that arising from Pontrjagin's work on duality.

Type
Research Article
Copyright
© 2000 Cambridge University Press