Z-modules and full completeness of multiplicative linear logic

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)

Abstract

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

Original languageEnglish
Pages (from-to)165-191
Number of pages27
JournalAnnals of Pure and Applied Logic
Volume107
Issue number1-3
DOIs
Publication statusPublished - 2001 Jan 15

All Science Journal Classification (ASJC) codes

  • Logic

Fingerprint

Dive into the research topics of 'Z-modules and full completeness of multiplicative linear logic'. Together they form a unique fingerprint.

Cite this