Article contents
Pontrjagin duality and full completeness for multiplicative linear logic (without Mix)
Published online by Cambridge University Press: 01 April 2000
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
- Information
- Copyright
- © 2000 Cambridge University Press
- 4
- Cited by