Z-modules and full completeness of multiplicative linear logic
2001; Elsevier BV; Volume: 107; Issue: 1-3 Linguagem: Inglês
10.1016/s0168-0072(00)00029-4
ISSN1873-2461
Autores Tópico(s)Logic, Reasoning, and Knowledge
ResumoWe 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))).
Referência(s)