TY - JOUR

T1 - A phase semantics for polarized linear logic and second order conservativity

AU - Hamano, Masahiro

AU - Takemura, Ryo

N1 - Funding Information:
Supported by Grant-in-Aid for Scientific Research (C) (19540145) of JSPS. **

PY - 2010/3

Y1 - 2010/3

N2 - 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].

AB - 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].

UR - http://www.scopus.com/inward/record.url?scp=77949821550&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77949821550&partnerID=8YFLogxK

U2 - 10.2178/jsl/1264433910

DO - 10.2178/jsl/1264433910

M3 - Article

AN - SCOPUS:77949821550

SN - 0022-4812

VL - 75

SP - 77

EP - 102

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

IS - 1

ER -