A phase semantics for polarized linear logic and second order conservativity

Masahiro Hamano, Ryo Takemura

研究成果: Article同行評審

2 引文 斯高帕斯(Scopus)

摘要

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

原文English
頁(從 - 到)77-102
頁數26
期刊Journal of Symbolic Logic
75
發行號1
DOIs
出版狀態Published - 2010 3月

All Science Journal Classification (ASJC) codes

  • 哲學
  • 邏輯

指紋

深入研究「A phase semantics for polarized linear logic and second order conservativity」主題。共同形成了獨特的指紋。

引用此