Z-modules and full completeness of multiplicative linear logic

研究成果: Article同行評審

1 引文 斯高帕斯(Scopus)


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 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 "Z-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))).

頁(從 - 到)165-191
期刊Annals of Pure and Applied Logic
出版狀態Published - 2001 1月 15

All Science Journal Classification (ASJC) codes

  • 邏輯


深入研究「Z-modules and full completeness of multiplicative linear logic」主題。共同形成了獨特的指紋。