Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-11-22T06:22:43.822Z 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: [email protected]

Abstract

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

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)