Published online by Cambridge University Press: 01 April 2000
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.