Z-modules and full completeness of multiplicative linear logic

We prove that the full completeness theorem for MLL+Mix holds by the simple interpretation via formulas as objects and proofs as Z-invariant morphisms in the *-autonomous category of topologized vector spaces. We do this by g eneralizing the recent work of Blute and Scott (Ann. Pure Appl. Logic 77 (1 996) 101-142) where they used the semantical framework of dinatural transfo rmation introduced by Girard-Scedrov-Scott (in: Y. Moschovakis (Ed.), Logic from Computer Science, vol. 21, Springer, Berlin, 1992, pp. 217-241). By o mitting the use of dinatural transformation, our semantics evidently allows the interpretation of the cut-rule while the original Blute-Scott's does n ot. Moreover, our interpretation for proofs is preserved automatically unde r the cut elimination procedure. (In this sense, our semantics is considere d as a denotational semantics.) In our semantics proofs themselves are char acterized by the concrete algebraic notion "Z-invariance", and our denotati onal semantics provides the full completeness. Our semantics is naturally e xtended to the full completeness semantics for CyLL + Mix owing to an elega nt method of Blute-Scott (J. Symbolic Logic 63(4) (1998) 1413-1436) (which is a sequel to (Blute and Scott (Ann, Pure Appl. Logic 77 (1996) 101-142))) . (C) 2001 Elsevier Science B.V. All rights reserved. MSC: 03F07; 03F52; 18 A15; 18B30; 68Q55.