Relational proof system for linear and other substructural logics

Logic Journal of the IGPL 5 (5):673-697 (1997)
  Copy   BIBTEX

Abstract

In this paper we give relational semantics and an accompanying relational proof system for a variety of intuitionistic substructural logics, including linear logic with exponentials. Starting with the 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 RelKripke 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 if, a translation, t<εvu, has a cut-complete proof tree which is fundamental. This result is constructive: that is, if a cut-complete proof tree for tεvu is not fundamental, we can use the failed proof search to build a relational countermodel for t and from this, build a RelKripkeX countermodel for γ1[sdot ]…[sdot ]γn⊃α

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 104,706

External links

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

Through your library

Analytics

Added to PP
2015-02-04

Downloads
10 (#1,546,824)

6 months
3 (#1,181,901)

Historical graph of downloads
How can I increase my downloads?