Relational Proof System for Linear and Other Substructural Logics
Relational Proof System for Linear and Other Substructural Logics
复制标题
线性和其他子结构逻辑的关系证明系统
DOI：
10.1093/jigpal/5.5.673
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
W. MacCaull
中科院分区：
文献类型：
--
作者：
W. MacCaull
在本文中，我们给各种直觉子结构逻辑，包括（直觉）线性逻辑与指数的关系语义和相应的关系证明系统。从[13]中讨论的FL的（Kripke风格）语义开始，我们在[11]中开发了一个关系语义和一个完整的Lambek演算的关系证明系统。在这里，我们以此为基础，并推广结果，以处理各种结构规则的交换，收缩，削弱和扩大，也处理一个对合算子和与运营商！然后呢？线性逻辑。为了实现这一点，对于FL的每个扩展X，我们开发了一个Kripke风格的语义，RelKripkeX语义，作为关系语义的桥梁。RelKripkeX语义由一个具有区别元素、三元关系和关系上的条件列表的集合组成。对于每个扩展X，RelKripkeX语义伴随着类似于[13]中的Kripke风格的赋值系统。关于FLX的可靠性和完备性定理对RelKripkeX -模型成立。然后，在Orlowska [16]，[17]和Buszkowski & Orlowska [4]工作的精神下，我们为每个扩展X开发关系逻辑RFLX。形容词关系用于强调RFLX具有将公式解释为关系的语义的事实。本文证明了FLX中的一个π Γ → α是可证明的当且仅当平移t（γ1 ·..· γn α）vu，有一个基本的切割完整证明树。这个结果是构造性的：也就是说，如果对于t（γ1 ·...· γn <$α）的关系型反模型不是基本的，我们可以使用失败证明搜索来为t（γ1 ·.· γn <$α），并由此建立γ1 ·.的RelKripkeX反模型。· γn α。1
In this paper we give relational semantics and an accompanying relational proof system for a variety of intuitionistic substructural logics, including (intuitionistic) linear logic with exponentials. Starting with the (Kripke-style) semantics for FL as discussed in [13], we developed, in [11], a relational semantics and a relational proof system for full Lambek calculus. Here, we take this as a base and extend the results to deal with the various structural rules of exchange, contraction, weakening and expansion, and also to deal with an involution operator and with the operators ! and ? of linear logic. To accomplish this, for each extension X of FL we develop a Kripke-style semantics, RelKripkeX semantics, as a bridge to relational semantics. The RelKripkeX semantics consists of a set with distinguished elements, ternary relations and a list of conditions on the relations. For each extension X , RelKripkeX semantics is accompanied by a Kripke-style valuation system analogous to that in [13]. Soundness and completeness theorems with respect to FLX hold for RelKripkeX -models. Then, in the spirit of the work of Orlowska [16], [17], and Buszkowski & Orlowska [4], we develop relational logic RFLX for each extension X . The adjective relational is used to emphasize the fact that RFLX has a semantics wherein formulas are interpreted as relations. We prove that a sequent Γ → α in FLX is provable iff, a translation, t(γ1 • ... • γn ⊃ α)ǫvu, has a cut-complete proof tree which is fundamental. This result is constructive: that is, if a cut-complete proof tree for t(γ1 • ... • γn ⊃ α)ǫvu is not fundamental, we can use the failed proof search to build a relational countermodel for t(γ1 • ... • γn ⊃ α) and from this, build a RelKripkeX countermodel for γ1 • ... • γn ⊃ α. 1