A phase semantics for polarized linear logic and second order conservativity

Journal of Symbolic Logic 75 (1):77-102 (2010)
  Copy   BIBTEX

Abstract

This paper presents a polarized phase semantics, with respect to which the linear fragment of second order polarized linear logic of Laurent [15] is complete. This is done by adding a topological structure to Girard's phase semantics [9]. The topological structure results naturally from the categorical construction developed by Hamano—Scott [12]. The polarity shifting operator ↓ (resp. ↑) is interpreted as an interior (resp. closure) operator in such a manner that positive (resp. negative) formulas correspond to open (resp. closed) facts. By accommodating the exponentials of linear logic, our model is extended to the polarized fragment of the second order linear logic. Strong forms of completeness theorems are given to yield cut-eliminations for the both second order systems. As an application of our semantics, the first order conservativity of linear logic is studied over its polarized fragment of Laurent [16]. Using a counter model construction, the extension of this conservativity is shown to fail into the second order, whose solution is posed as an open problem in [16]. After this negative result, a second order conservativity theorem is proved for an eta expanded fragment of the second order linear logic, which fragment retains a focalized sequent property of [3]

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,075

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

The Semantics and Proof Theory of Linear Logic.Arnon Avron - 1988 - Theoretical Computer Science 57 (2):161-184.
Second-order logic and foundations of mathematics.Jouko Väänänen - 2001 - Bulletin of Symbolic Logic 7 (4):504-520.
Linear logic in computer science.Thomas Ehrhard (ed.) - 2004 - New York: Cambridge University Press.
On the membership problem for non-linear abstract categorial grammars.Sylvain Salvati - 2010 - Journal of Logic, Language and Information 19 (2):163-183.
Phase semantics and Petri net interpretation for resource-sensitive strong negation.Norihiro Kamide - 2006 - Journal of Logic, Language and Information 15 (4):371-401.

Analytics

Added to PP
2010-09-12

Downloads
17 (#870,460)

6 months
7 (#433,721)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Natural Deduction: A Proof-Theoretical Study.Richmond Thomason - 1965 - Journal of Symbolic Logic 32 (2):255-256.
A categorical semantics for polarized MALL.Masahiro Hamano & Philip Scott - 2007 - Annals of Pure and Applied Logic 145 (3):276-313.

Add more references