Z-modules and full completeness of multiplicative linear logic Original Research Article

We prove that the full completeness theorem for MLL+Mix holds by the simple interpretation via formulas as objects and proofs as View the MathML source-invariant morphisms in the ∗-autonomous category of topologized vector spaces. We do this by generalizing the recent work of Blute and Scott (Ann. Pure Appl. Logic 77 (1996) 101–142) where they used the semantical framework of dinatural transformation introduced by Girard–Scedrov–Scott (in: Y. Moschovakis (Ed.), Logic from Computer Science, vol. 21, Springer, Berlin, 1992, pp. 217–241). By omitting the use of dinatural transformation, our semantics evidently allows the interpretation of the cut-rule, while the original Blute–Scottʹs does not. Moreover, our interpretation for proofs is preserved automatically under the cut elimination procedure. (In this sense, our semantics is considered as a denotational semantics.) In our semantics proofs themselves are characterized by the concrete algebraic notion “View the MathML source-invariance”, and our denotational semantics provides the full completeness. Our semantics is naturally extended to the full completeness semantics for CyLL+Mix owing to an elegant 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))).