Home
Scholarly Works
Relational proof system for linear and other...
Journal article

Relational proof system for linear and other substructural logics

Abstract

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 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(γ1[sdot ]…[sdot ]γ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[sdot ]…[sdot ]:γn⊃α)εvu is not fundamental, we can use the failed proof search to build a relational countermodel for t(γ1[sdot ]…γn⊃α) and from this, build a RelKripkeX countermodel for γ1[sdot ]…[sdot ]γn⊃α. Keyw ords: Lambek calculus, structural rules, relational semantics, proof theory, ternary relations, Kripke semantics, tableau, countermodel

Authors

MacCaull W

Journal

Logic Journal of IGPL, Vol. 5, No. 5, pp. 673–697

Publisher

Oxford University Press (OUP)

Publication Date

September 1, 1997

DOI

10.1093/jigpal/5.5.673

ISSN

1367-0751

Contact the Experts team