nexoncn.com

文档资料共享网 文档搜索专家

文档资料共享网 文档搜索专家

当前位置：首页 >> >> Relational proof system for linear and other substructural logics, Logic

Relational Proof System for Linear and Other Substructural Logics

WENDY MACCAULL, Department of Mathematics, Computing and Information Systems, St. Francis Xavier University, PO Box 5000, Antigonish, NS, B2G 2W5, Canada. E-mail: wmaccaul@juliet.stfx.ca 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 F L 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 F L 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 F LX hold for RelKripkeX -models. Then, in the spirit of the work of Orlowska [16], [17], and Buszkowski & Orlowska [4], we develop relational logic RF LX for each extension X. The adjective relational is used to emphasize the fact that RF LX has a semantics wherein formulas are interpreted as relations. We prove that a sequent Γ → α in F LX is provable i?, 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 Keywords : Lambek calculus, structural rules, relational semantics, proof theory, ternary relations, Kripke semantics, tableau, countermodel

1

Introduction

Substructural logics are currently of great interest as the logics for analysing information ?ow (see [5], [8] and [21]). Thinking of premises as resources, and by adding or deleting di?erent structural rules, we can make the logic dependent on which resources are used, how many times each resource is used and the order in which the resources are used. Here we develop a tableau-style theorem prover for a variety of intuitionistic substructural logics. When the algorithm terminates as a fundamental tree, the formula is a theorem of the logic; when it terminates as a nonfundamental tree, information on a branch of the tableau allows us to construct a countermodel, so the formula is not a theorem of the logic. The strategy is to use relational semantics for the logics. Basic motivation for

1 Full version of a paper presented at the 3rd Workshop on Logic, Language, Information and Computation (WoLLIC’96 ), May 8–10, Salvador (Bahia), Brazil, organised by UFPE and UFBA, and sponsored by IGPL, FoLLI, and ASL.

L. J. of the IGPL, Vol. 5 No. 5, pp. 673–697 1997

673

c Oxford University Press

674 Relational Proof System for Linear and Other Substructural Logics this approach may be found in [15]–[18] and [4] (see also [1], [3], [7] and [19] for semantics using ternary relations). In relational semantics, formulas are interpreted as relations. In this case, we use ternary relations. Logical symbols include special symbols denoting ternary relations and distinguished constants, and the axioms are then conditions on the relations and the constants. Connectives are de?ned so as to build new ternary relations from old ones. Each connective gives rise to two decomposition rules, and each condition gives rise to a speci?c rule. We start with the logic F L, (full Lambek calculus) which is the basic substructural logic. The relational semantics for F L was developed in [11]. Here we develop extensions of the proof theory dealing with a whole spectrum of substructural logics. By adding one (or a combination of) condition (s) we can add in one (or more) of the structural properties of exchange, weakening, contraction and expansion. By adding new accessibility relations, subject to a set of rules (relational analogues of those in [13]) we extend F L to deal with Linear Logic with the modal operators ! and ?. F L can be further extended by adding an operator to deal with involution, and thence the logic of quantales with involution, as discussed in [12], can be dealt with. The last logic is of importance in describing the speci?cation of programs in the case where the behaviour of the machine is quantized. We use three di?erent semantics to achieve our goal. The ?rst is the (Kripke) semantics for F L and various extensions as de?ned in [13] and [14]. Using this semantics, we develop a Kripke-style semantics, which we call RelKripkeX semantics, for various extensions, X (including the trivial, i.e., the empty, extension) of F L. (The name was chosen to indicate the fact that this semantics acts as a bridge between the semantics in [13] and the relational semantics.) Ternary accessibility relations are used to provide interpretations of connectives and modal operators. The relations are subject to a list of conditions and soundness and completeness for RelKripkeX models with respect to F LX follows. RelKripke semantics plays the same role in the develoment of relational semantics as the Routley-Meyer [19] semantics for relevance logic plays in Orlowska’s development of relational semantics for relevance logic (see [16]). Then relational logic RF LX is described. A Rasiowa-Sikorski style deduction system for RF LX is presented with deduction rules that ensure tableaustyle of proofs. (That is, proofs are trees, called decomposition trees). To de?ne the RF LX -models, formulas of the logic are interpreted as ternary relations (hence the term relational semantics). Validity in the class of RelKripkeX -models is equivalent to validity in the class of RF LX -models. We prove that a sequent Γ → α of F LX is provable if and only if (a translation of) the sequent has a cut-complete proof tree which is fundamental. Moreover the result is constructive: a failed proof search may be used to build a countermodel which is a RelKripkeX -model. Thus, this method accomplishes, using a di?erent semantics and proof method, the goal outlined in [5] of providing a constructive theorem prover for the additive (as well as the multiplicative) fragment of substructural logics, as well as for linear logic with exponentials. This is the ?rst theorem prover for the full propositional fragment of these logics for which a nonfundamental branch (or, in the terms of other tableau methods, an open branch) guarentees that we may construct a countermodel. The relational semantics and relational proof theory for the basic substructural logic, F L, is contained in [11]. So that this paper is self contained, the following section will be a recap of de?nitions and results from [11] upon which these extensions

2. KRIPKE AND RELKRIPKE MODELS

675

are based. We write out the axioms and rules of inference for basic F L, the de?nition from [13] of semantics for F L and the de?nitions of RelKripke-model and RF Lmodel from [11] and we state the main results from [11]. In the next sections we consider in turn the extensions to other substructural logics, including linear logic with exponentials, and the logic of involutive quantales. We close with some open problems and further directions for research.

2

Kripke and RelKripke models

The language of F L consists of propositional constants 1, 0 ,? and ⊥ and of connectives ∨, ∧, ? and ?. Formulas are built in the usual way. A sequent of F L is an expression of the form Γ → α where Γ is a ?nite sequence of formulas, γ1 , γ2 , ..., γn, and α is a formula. Γ and/or α may be empty. Capital Greek letters denote ?nite (possibly empty) sequences of formulas. Initial sequents are of the following form: (i) α → α; (ii) → 1; (iii) 0 → ; (iv) Γ → ?; and, (v) Γ, ⊥, ? → θ. Rules of inference are the following: Γ→α ?, α, Σ → θ ?, Γ, Σ → θ (0w) (cut) Γ, ? → θ Γ, 1, ? → θ (1w)

Γ→ Γ→0

Γ, α, ? → θ Γ, β, ? → θ Γ, α ∨ β, ? → θ Γ→β Γ → α∨β (→ ∨2 )

(∨ →)

Γ→α Γ→α∨β

(→ ∨1 )

Γ, α, ? → θ Γ, α ∧ β, ? → θ Γ→α

(∧1 →)

Γ, β, ? → θ Γ, α ∧ β, ? → θ (→ ∧)

(∧2 →)

Γ→β Γ → α∧β

Γ, α, β, ? → θ Γ, α ? β, ? → θ

(? →)

Γ→α Γ, ? → α ? β Γ, α → β Γ→α?β (→?)

?→β

(→ ?)

Γ→α ?, β, Σ → θ ?, α ? β, Γ, Σ → θ

(?→)

In [13] we ?nd the following de?nition for Kripke model. Definition 2.1 A structure D = D, ∩, ?, ?, ω is a semilattice-ordered monoid (abbreviated so-monoid) if: (1) D, ∩ is a meet-semilattice with greatest element ω; (2) D, ?, ? is a monoid with identity that satis?es x ? ω = ω for every x ∈ D; (3) z ? (x ∩ y) ? w = (z ? x ? w) ∩ (z ? y ? w) for every x, y, z, w ∈ D.

676 Relational Proof System for Linear and Other Substructural Logics Remark 2.2 The meet operation ∩ induces a partial order on D; we write x ≤ y i? x ∩ y = x. Using (3) of the above de?nition, it is easy to show that if x ≤ y then for all z, both x ? z ≤ y ? z and z ? x ≤ z ? y. We call this last property the monotonicity of ?. For every so-monoid, D, a subset, A, of D, is a ?lter of D if, for every x, y ∈ A and every z ∈ D, x ∩ y ≤ z implies z ∈ A. Let F (D) be the set of nonempty ?lters of D. Definition 2.3 A Kripke model is a pair, D, g , consisting of an so-monoid, D, and a mapping, g, from the set of propositional variables and the constant 0 to F (D). For a given Kripke model D, g , the relation x |= α, for an element x ∈ D and a formula α, is de?ned inductively as follows: (1) x |= p i? x ∈ g(p), if p is a propositional variable or 0; (2) x |= 1 i? x ≥ ?; (3) x |= ? for every x; (4) x |=⊥ i? x = ω; (5) x |= α ? β i? for every y and z, if y |= α and x ? y ≤ z then z |= β; (6) x |= α ∨ β i? there exists y and z such that y ∩ z ≤ x and (y |= α or y |= β) and (z |= α or z |= β); (7) x |= α ∧ β i? x |= α and x |= β; (8) x |= α ? β i? there exists y and z such that y ? z ≤ x and y |= α and z |= β. The symbol |= is called a valuation on D determined by g . Using an induction argument, one can show that for every formula α, the set {x ∈ D | x |= α} ∈ F (D). We say that the formula α is true in a Kripke model D, g i? x |= α for every x ≥ ?, and α is valid in a class, K, of Kripke models i? α is true in each Kripke model in K. A sequent Γ → θ is valid in a class K of Kripke models i? the formula γ1 ? γ2 ? ... ? γn ? θ is valid in K. (Note, by γ1 ? γ2 ? ... ? γn we mean ((...((γ1 ? γ2 ) ? γ3 )...) ? γn ).) Proposition 2.4 (Soundness and completeness [13]) Let Γ be a sequence of formulas of FL and let α be a formula of FL. Then Γ → α is provable in FL i? Γ → α is valid in all Kripke models. We now describe a Kripke-style semantics for F L which uses a set with two ternary relations and distinguished elements as models, rather than so-monoids. We have ternary relations R and I, and write Rxyz (or Ixyz) to imply that (x, y, z) is a three tuple in R (or I). Let us explain the role of R and I. When we assert Rxyz we are articulating for the new semantics, a condition corresponding to x ? y ≤ z in the somonoid. When we assert Ixyz, we are articulating for the new semantics, a condition corresponding to x ∩ y ≤ z in the so-monoid. Thus the conditions on the two relations articulate conditions on the operations ? and ∩ and on the relation ≤, that we need in order to prove the soundness of F L. We make the following de?nition: Definition 2.5 ([11]) A RelKripke model M is a 6-tuple S, ω, ?, R, I, g , such that: S is a nonempty set, whose elements are called states; ω and ? are distinguished elements of S; R and I are ternary relations on S; and g is a meaning function that assigns (nonempty) sets of states to propositional variables, and 0, so that ω is a member of each set, and the following condition, called the valuation condition, is satis?ed:

2. KRIPKE AND RELKRIPKE MODELS if x ∈ g(p) and y ∈ g(p) and Ixyz, then z ∈ g(p). Moreover the following conditions are satis?ed for any a, b, c, t, u ∈ S:

677

(c1) R??x and R??y and Ixyz imply R??z; (c2) Iωωz implies R?zω and R?ωz; (c3) Iabx and Rxcd imply ?q1 , q2(Racq1 , and Rbcq2 and Iq1 q2 d); (c4) Iabc implies Ibac; (c5) Ia1 a2 a and Ib1 b2 b and Iabx imply ?q1 , q2(Ia1 b2 q1 and Ia2 b1 q2 and Iq1 q2 x); (c6) Ib1 b2 b and Iabx imply ?q(Iab1 q and Iqb2 x); (c7) Ra1 a2 a and Rb1 b2 b and Iabx imply ?q1 , q2(Ia1 b1 q1 and Ia2 b2 q2 and Rq1 q2 x); (c8) R?ab implies Iaab; (c9) Raωb implies R?bω and R?ωb; (c10) R?aa; (c11) Ra?b implies R?ab; (c12) R?ab and Rtbu imply Rtau; (c13) R?ab and Rbtu imply Ratu; (c14) Raxb and Icdx imply ?q1 , q2 (Racq1 and Radq2 and Iq1 q2 b); (c15) Razb and Rcdz imply ?q(Racq and Rqdb); (c16) Rabz and Rzde imply ?q(Rbdq and Raqe); (c17) Ra1 a2 a and Ra3 a4 a2 and Ra5 a6 a3 implies ?q1 , q2(Ra6 a4 q1 and Ra5 q1 q2 and Rq2 a2 a). We say that in the RelKripke model M, state x satis?es formula α, and write x |= α, i? the following conditions are satis?ed: (1) x |= p i? x ∈ g(p) for each propositional variable p or 0; (2) x |= 1 i? R??x; (3) x |= ? for every x; (4) x |=⊥ i? x = ω; (5) x |= α ? β i? for every y and z, if y |= α and Rxyz then z |= β; (6) x |= α ∨ β i? there exists y and z such that Iyzx and (y |= α or y |= β) and (z |= α or z |= β); (7) x |= α ∧ β i? x |= α and x |= β; (8) x |= α ? β i? there exists y and z such that Ryzx and y |= α and z |= β. A formula α is true in the RelKripke model M i? for all x ∈ S, if R??x, then x |= α. Theorem 2.6 (Soundness theorem for FL [11]) If the sequent Γ → θ is provable in FL, then it is true is all RelKripke models. Remark 2.7 The full proof is in [11]; the reader can check that conditions (c1) to (c7) are used to establish the assertion that for all formulas α, if x |= α and y |= α and Ixyz then z |= α, and that conditions (c8) to (c17) (along with the above assertion) are used to show that the initial sequents are valid and that the rules of inference preserve validity. Since F L is a Gentzen-style presentation of the Lambek calculus, with few axioms and many rules, rather than a Hilbert-style presentation with few rules and

678 Relational Proof System for Linear and Other Substructural Logics many axioms, we cannot associate directly an axiom with a condition as done in [16] for relevant logics. An alternative procedure would have been to start with a Hilbertstyle presentation and derive the conditions on R and I; the conditions would be di?erent in some cases, but as a set, they would be equivalent to the set given here. To help the reader get the feel of what the conditons are saying, we use (c12) and (c13) when we need to articulate the monotonicity of ? (note that (c12) articulates the condition ? ? a ≤ b and t ? b ≤ u implies t ? a ≤ u) and we use (c15) and (c16) to articulate the associativity properties of ?. Remark 2.8 From the assertion if x |= α and y |= α and Ixyz then z |= α and (c8), we can deduce that if x |= α and R?xy, then y |= α. Thus formula α is true in the RelKripkemodel M i? ? |= α. These observations facilitate many proofs. Note also that if x |= (α1 ? α2 ) ? α3 , then, using (c14), we can show that x |= α1 ? (α2 ? α3 ). Note 2.9 The use, by Ono, of the adjective Kripke for the semantics described in de?nitions 2.1 and 2.3 is somewhat inappropriate. The general characteristic of Kripke semantics is the feature that the frames (or models) are equipped with certain accessibility relations interpreting some connectives (often modal connectives). The semantics in de?nitions 2.5 and 2.12 have this feature. Theorem 2.10 (Correspondence theorem [11]) For every Kripke model, D, g , of FL there is a RelKripke model, M, of FL such that, if θ is not true in D, g , then θ is not true in M. Proof. Suppose θ is not true in the Kripke model D, g . Then there is x ∈ D such that x |= θ in D, g . De?ne the model M= S, ω, ?, R, I, g such that the set S consists of the elements of D, the distinguished elements ω and ? are the same as in D, the relations R and I are de?ned as: Rxyz (in M) i? x ? y ≤ z (in D, g ) and Ixyz (in M) i? x ∩ y ≤ z (in D, g ), and, ?nally, such that g is the same as for D, g . It is straightforward (and sometimes trivial) to show that the 17 conditions of de?nition 2.5 hold (see [11]). Then, use induction on the length of the formula, θ, to prove that for ?x ∈ S, if x |= θ in M, (write x |=M θ) then x |= θ in D, g (write x |=D θ). The contrapositive of this last statement gives us the result we seek. We give a brief example. Suppose D, g is a Kripke model for which contraction does not hold. Thus, we cannot demonstrate ? |=D α ? α ? α; consequently, there exist y, z such that ? ? y ≤ z and y |=D α and z |=D α ? α. Let M be the RelKripkemodel associated to D, g . Suppose now that ? |=M α ? α ? α holds. Thus for any y, z, if y |=M α and R?yz then z |=M α ? α. By the theorem above, this tells us that ? ? y ≤ z and y |=D α and z |=D α ? α. This gives a contradiction. Theorem 2.11 (Completeness theorem for FL [11]) Suppose the sequent Γ → α is valid in all RelKripke models. Then Γ → α is provable in FL. We now de?ne a logic RF L which is the relational logic corresponding to F L. We provide a so-called relational semantics for RF L; by this, we mean that all formulas are interpreted as (ternary) relations.

2. KRIPKE AND RELKRIPKE MODELS

679

Definition 2.12 Expressions of the language RF L are constructed with symbols from the following sets: V o (object variables); C (ternary relational constants); { ?, ω } (object constants); { R, I } (ternary relational constants (neither in C)); {∧, ∨, ?, ?} (binary relational operations); and ? (unary relational operation). The set, Eo, of object expressions is the set consisting of the elements of V o and the elements ? and ω; the set, Er, of relational expressions, is the smallest set such that: C ? Er, and if A, B ∈ Er, then each of ?A, A ∧ B, A ∨ B, A ? B and A ? B ∈ Er. The set, F M , of formulas, is the smallest set such that: if x, y, z ∈ Eo, and A ∈ Er, then Axyz ∈ F M , and Rxyz, ?Rxyz, Ixyz and ?Ixyz ∈ F M. Before we list the deduction rules for RF L, we discuss the relational models. First, we need ?ve relational operations to correspond to the logical connectives. Note that the operation ∨ di?ers from the relational operation ∨ used in [16]. Definition 2.13 Let U be a nonempty set, let R and I be distinguished ternary relations on U , and let A and B be ternary relations. De?ne ?ve relational operations on the family of ternary relations on U as follows: A ∨ B = {(a, b, c) | ?y, z such that (y, z, a) ∈ I and ((y, b, c) ∈ A or (y, b, c) ∈ B) and ((z, b, c) ∈ A or (z, b, c) ∈ B)}. A ? B = {(a, b, c) | ?y, z if (y, b, c) ∈ A and (a, y, z) ∈ R, then (z, b, c) ∈ B}. A ∧ B = {(a, b, c) | (a, b, c) ∈ A and (a, b, c) ∈ B}. A ? B = {(a, b, c) | ?y, z such that (y, z, a) ∈ R and (y, b, c) ∈ A and (z, b, c) ∈ B}. ?A = {(a, b, c) | (a, b, c) ∈ A} Definition 2.14 A relation A ? U × U × U is called an ideal relation if it is of the form X × U × U for some X ? U . Remark 2.15 The set of ideal relations on U is closed under the ?ve operations de?ned above. Definition 2.16 By a model of the relational language RFL (also called an RFL-model) we mean a 6-tuple M = (U, ω, ?, R, I, m), such that: U is a nonempty set, ω and ? are distinguished elements of U ; R and I are ternary relations on U; and m is a meaning function which assigns ternary relations to relational expressions. (Note we shall use the same symbol to designate an operation (or a distinguished ternary relational constant or a distinguished constant symbol) in the language and its respective interpretation in a model.) The meaning function m is de?ned as follows: m(R) = R, and m(I) = I, and each formula A ∈ Er is mapped by m to a ternary relation in such a way that: m(?A) = ?m(A), m(A ∧ B) = m(A) ∧ m(B), m(A ∨ B) = m(A) ∨ m(B),

680 Relational Proof System for Linear and Other Substructural Logics m(A ? B) = m(A) ? m(B) and m(A ? B) = m(A) ? m(B). Note, since the connective on the right of each equality denotes a relational operator as de?ned in de?nition 2.13, each formula is, indeed, mapped to a ternary relation. Moreover, m satis?es the following condition: if P ∈ C then m(P ) = X × U × U for some X ? U . Finally, R and I satisfy condition (c1) -(c17) from de?nition 2.5. When discussing relational models we sometimes use the more conventional relational notation; thus, for example, for (c1), we write: if (?, ?, x) ∈ R and (?, ?, y) ∈ R and (x, y, z) ∈ I, then (?, ?, z) ∈ R. We also assume that for all P ∈ C, if (x, t, u) ∈ m(P ) and (y, t, u) ∈ m(P ) and (x, y, z) ∈ I then (z, t, u) ∈ m(P ); we shall refer to this condition as (c0). Definition 2.17 By a valuation, we mean a function v : Eo → U , such that v(?) = ? and v(ω) = ω. We say that in the RFL-model M, the valuation satis?es the relational formula Axyz, (and write (M, v sat Axyz)) i? (v(x), v(y), v(z)) ∈ m(A), where A is R, or ?R, or I, or ?I, or a relational expression from Er. Formula Axyz is true in the RFL-model M if (M, v sat Axyz), for every valuation v, and ?nally, the formula Axyz is valid if it is true in all the RFL-models. Remark 2.18 For the remainder of this section, validity will refer to validity in RF L-models. We shall present deduction rules using a shorthand notation, and write: F ormulas1 F ormulas2 to represent: K, F ormulas1 , H K, F ormulas2 , H and write F ormulas1 F ormulas21 to represent: K, F ormulas1 , H K, F ormulas21 , H F ormulas22 ... F ormulas23

K, F ormulas22, H

... K, F ormulas23, H

here, K and H represent ?nite sequences of formulas. Definition 2.19 A sequence of formulas is said to be valid if at least one of the formulas in the sequence is valid. A rule of the form K/H is said to be admissible if the sequence K is valid if and only if the sequence H is valid. A rule of the form K/(H1 H2 ) is said to be admissible if the sequence K is valid if and only if both the sequences H1 and H2 are valid. A similar de?nition follows for admissibility of a rule of the form K/(H1 H2 ... Hj ).

2. KRIPKE AND RELKRIPKE MODELS Decomposition Rules: ? (A ? B)xtu ?Aytu, ?Rxyz, Bztu ? ? (Tagged) ?(A ? B)xtu Aytu, ?(A ? B)xtu ∧ (A ∧ B)xtu Axtu Bxtu ?∧ ?(A ∧ B)xtu ?Axtu, ?Bxtu ? (Tagged) (A ? B)xtu Ryzx, (A ? B)xtu

681

Rxyz, ?(A ? B)xtu

?Bztu, ?(A ? B)xtu

Aytu, (A ? B)xtu

Bztu, (A ? B)xtu

?? ?(A ? B)xtu ?Ryzx, ?Aytu, ?Bztu ∨ (Tagged) (A ∨ B)xtu Iyzx, (A ∨ B)xtu ?∨ ?(A ∨ B)xtu

?Ixyz,?Aytu,?Aztu ?Ixyz,?Bytu,?Aztu ?Ixyz,?Aytu,?Bztu ?Ixyz,?Bytu,?Bztu

Aytu, Bytu, (A ∨ B)xtu

Aztu, Bztu, (A ∨ B)xtu

In each tagged rule, y, z ∈ Eo; otherwise, y, z ∈ V o, and furthermore, neither y nor z occurs in any formula above the line. A rule is tagged when it is necessary that the rule be applied for each object expression on the branch, even for those object expressions generated after the tagged rule was ?rst applied. Speci?c Rules: There are 19 speci?c rules to write out, one for the condition on the meaning function m, and one for each of the conditions (c0) to (c17) on R and I. We shall list a representative sample of them: the reader can show that each of the others follow a pattern similar to one listed below. The form the rules take will be motivated by the fact that we need to have the sequence of formulas above the line valid if and only if the sequence of formulas below the line is valid, and that this needs to occur if and only if the corresponding condition is valid; in fact it helps to focus on the validity of the contrapositive of the corresponding condition. Note that whenever we have ∧ in the second part of the contrapositive, we have a branching rule.

682 Relational Proof System for Linear and Other Substructural Logics Condition on m (the meaning function): P atu P azw (z, w ∈ Eo)

Condition (c0): If P xtu and P ytu and Ixyz then P ztu. P ztu P xtu, P ztu P ytu, P ztu Ixyz, P ztu (x, y ∈ Eo) Condition (c2): Iωωz implies R?zω and R?ωz. ?Iωωz ?Iωωz, ?R?zω, ?R?ωz Condition (c3): Iabx and Rxcd imply ?q1 , q2 (Racq1 , and Rbcq2 and Iq1 q2 d). ?Iabx, ?Rxcd ?Iabx, ?Rxcd, ?Racq1, ?Rbcq2, ?Iq1 q2 d Condition (c4): Iabc implies Ibac Ibac Ibac, Iabc Condition (c10): R?aa. ?R?aa (a ∈ Eo) (q1 , q2 ∈ V o, not in the line above)

Speci?c rules for conditions (c1), (c12) and (c13) follow a pattern similar to that for condition (c0); speci?c rule for condition (c9) follows a pattern similar to that for condition (c2); speci?c rules for conditions (c5), (c6), (c7), (c14), (c15) (c16) and (c17) follow a pattern similar to that for condition (c3), and ?nally, speci?c rules for (c8) and (c11) follow a pattern similar to that for condition (c4). Definition 2.20 A sequence of formulas is said to be fundamental i? it includes formulas Aatu, and ?Aatu, for some A ∈ F M and some a, t, u ∈ Eo. Proposition 2.21 (1) Decomposition rules are admissible. (2) Speci?c rules are admissible. (3) Fundamental sequences are valid. Definition 2.22 A decomposition tree for a formula F is a tree growing downward with F at its apex and branches generated by applying appropriate decomposition or speci?c rules, one at a time. Definition 2.23 A branch of a decomposition tree is said to be fundamental if it contains a fundamental sequence. A decomposition tree is said to be fundamental if all its branches are fundamental.

2. KRIPKE AND RELKRIPKE MODELS Proposition 2.24 (Tableau Correctness) If a decomposition tree of a formula F is fundamental, then F is valid.

683

Proof. This result follows directly from the facts that each rule is admissible, and fundamental sequences are valid. Definition 2.25 A decomposition tree is complete if it satis?es the following: For every vertex v of the tree and for every formula F occurring in v and for every branch br containing v, either br is fundamental or: (1) for every tagged rule applicable to F , and for every object expression z which occurs in the formulas of v, formulas obtained from F by application of that rule with z as a new object expression, occur in some vertex of br (in other words, a tagged rule must have been applied for each object expression on br); (2) the other applicable decomposition rules have been applied to F ; (3) applicable speci?c rules have been applied to br; (for example, for speci?c rule corresponding to (c0), if P ztu occurs on br, then for some x and y, either P xtu or P ytu or Ixyz occurs on br). We must add two more speci?c rules, which are cut-rules, before getting the desired completeness result. (cut ? R) Rxyz ?Rxyz Ixyz ?Ixyz Proposition 2.26 The rules (cut-R) and (cut-I) are admissible. Proof. The sequence K, H is valid i? both sequences K, Rxyz, H and K, ?Rxyz, H are valid. A similar result holds if we replace R by I. Definition 2.27 A decomposition tree is cut-complete i? it is complete and for every branch br and every x, y, z ∈ Eo occuring on br, both (cut-R) and (cut-I) have been applied. Remark 2.28 Without the cut-rules, we cannot be guarenteed that we can generate a (counter)model from a nonfundamental branch on the tableau for F . As we shall see, a countermodel will give rise to a RelKripke model for which the formula F is not true. With such a countermodel, we can conclude that F is not derivable. Definition 2.29 A formula is said to be nondegenerate if it is not a member of the set {Rxyz, ?Rxyz, Ixyz, ?Ixyz}. Proposition 2.30 (Tableau Completeness [11]) If a cut-complete decomposition tree of a nondegenerate formula F is not fundamental, then there is an RF L-model in which F is not true. We shall give the outline of the proof of this theorem so the reader may see how to construct a countermodel. (cut ? I)

684 Relational Proof System for Linear and Other Substructural Logics Proof. [Sketch] Suppose a cut-complete decomposition tree for the formula F has at least one nonfundamental branch br. We shall use it to build an RF L-countermodel for F : that is, we construct an RF L-model in which F is not true. Let IND be the set of indecomposable formulas on br and let BR be the set of formulas on br. De?ne the model as follows: Mbr = (E, ω, ?, R′, I ′ , mbr ), where: E is the set of object expressions on the branch; ω, and ? are constants from the language; R′ is de?ned as: (x, y, z) ∈ R′ i? Rxyz ∈ BR; I ′ is de?ned as: (x, y, z) ∈ I ′ i? Ixyz ∈ BR; mbr P = {(x, y, z) | P xyz ∈ IN D}; mbr R = R′ ; and, ?nally, mbr I = I ′ . We can show that in Mbr , every constant is an ideal relation and the conditions of RF L-models all hold. Consider, for example, condition (0). Suppose (x, t, u) ∈ mbr P and (y, t, u) ∈ mbr P and (x, y, z) ∈ I ′ but (z, t, u) ∈ mbr P . Then P ztu ∈ IN D and P xtu ∈ IN D and P ytu ∈ IN D and Ixyz ∈ BR. Since the tree is complete, the fact that P ztu ∈ IN D implies either P xtu ∈ IN D or P ytu ∈ IN D or Ixyz ∈ BR. Thus we have a contradiction, so we must conclude (z, t, u) ∈ mbr P . We use the cut rules to guarentee truth of the conditions containing existential quanti?ers – that is, conditions (c3), (c5), (c6), (c7), (c14), (c15), (c16) and (c17). We illustrate by considering (c15). Suppose (a, z, b) ∈ R′ and (c, d, z) ∈ R′ but for every q, either (a, c, q) ∈ R′ or (q, d, b) ∈ R′ . Then Razb ∈ BR and Rcdz ∈ BR. Since the tree is cut-complete, ?Razb ∈ BR and ?Rcdz ∈ BR. Then since the tree is complete, ?Razb ∈ BR, ?Rcdz ∈ BR, ?Racq ∈ BR, and ?Rqdb ∈ BR. Thus for some element z ∈ E, (a, z, b) ∈ R′ and (c, d, z) ∈ R′ , (a, c, q) ∈ R′ and (q, d, b) ∈ R′ . This gives a contradiction. Finally, one can show that the formula F is not true in this model (This follows by assuming the negation and proving a contradiction - the argument is identical to that for relevant logics found in [16]). Remark 2.31 To implement the algorithm there must be some strategies for termination of the algorithm in cases where there are an in?nite number of variables, but the application of rules like the tagged rules or cut rules or rules like (c0) or (c10) will not yield a fundamental sequence. We have not yet worked out the details of rules for termination (and of course we are not assurred of termination for arbitrary formula). However, as we shall show in an example at the end of this section, there are formulas for which it is clear that there is at least one nonfundamental branch. Each sequent of F L has a translation to a ternary relational expression. To make this translation, we start with a one to one mapping of the propositional variables to the constants, assigning constants di?erent from ? and ω to propositional variables. Then the map is extended to formulas in the usual way; that is: t(A∨B) = t(A)∨t(B), etc. A sequent Γ → α is translated as t(γ1 ? ... ? γn ? α)?vu. If Γ is empty, it is translated as some formula, which is a theorem of F L such as α ∨ α ? α; when α is empty, it is translated as some formula which is a nontheorem of F L. The proofs of the following two lemmas are analogous to those found in [16]. Lemma 2.32 For each RelKripke-model M there is a RF L-model M′ such that formula F is true in M i? t(F )?vu is true in M′ , for all v, u. Lemma 2.33 For each RF L-model M there is a RelKripke-model M′ such that formula F is true

3. STRUCTURAL RULES FOR F L 685 in M′ i? t(F )?vu is true in M, for all v, u. Thus we may conclude: Lemma 2.34 The formula F is valid in the class of RelKripke-models i? t(F )?vu is valid in the class of RF L-models. Theorem 2.35 ([11]) (1) A sequent Γ → α of F L is provable (in F L) if there is a fundamental decomposition tree for t(γ1 ? ... ? γn ? α)?vu. (2) (a) A sequent Γ → α of F L is not provable (in F L) if a cut-complete decomposition tree for t(γ1 ? ... ? γn ? α)?vu is not fundamental. (b) In this case we can construct a RelKripke-model of F L in which γ1 ? ... ? γn ? α is not true. Example 2.36 We now show that the formula α ? β ? β ? α is not a theorem of F L. In what follows, we let S denote the sequence ?Rwvz, (?α)wtu, (?β)vtu, ?Rxyz. (α ? β ? β ? α)xtu ?(α ? β)ytu, ?Rxyz, (β ? α)ztu ?Rwvy, (?α)wtu, (?β)vtu, ?Rxyz, (β ? α)ztu ?Rwvz, (?α)wtu, (?β)vtu, ?Rxyz, (β ? α)ztu S, Rvwz, (β ? α)ztu S, (β)vtu, (β ? α)ztu S, (α)wtu, (β ? α)ztu In the above proof, we ?rst applied the decomposition rule (?), then the decomposition rule (??), then the speci?c rule (c0), and ?nally, the tagged decomposition rule (?). The last rule was applied using elements which were on this branch, and once applied, yields three branches. Since we selected v and w, the second and third of the branches are fundamental, but the ?rst is not. If we had not selected these two variables (in that order) the second and third branches would not be fundamental. We would be able to reapply the tagged rule and apply speci?c rule (c0), but we always get a nonfundamental branch. No application of cut ? R (or any other applicable rule) allow us to conclude that the tree is fundamental.

3

Structural rules for F L

The substructural logics F Le , F Lc , F Lw and F Lexp are obtained from F L by adding the following rules of inference: the exchange rule (e, →), the contraction rule (c →) the weakening rules (w →) and (→, w), and the expansion rule (exp →), respectively, (see below). Γ, α ? β → θ Γ, β ? α → θ Γ, ? → θ Γ, α, ? → θ (e →) Γ, α ? α → θ Γ, α → θ Γ→ Γ→θ (c →)

(w →)

(→, w)

686 Relational Proof System for Linear and Other Substructural Logics Γ, α, ? → θ Γ, α, α, ? → θ (exp →)

Let D, g be a Kripke-model; D, g is a Kripkee -model if D is a commutative so-monoid; it is a Kripkew -model if g(0) = ω, x ≤ x ? y and x ≤ y ? x; it is a Kripkec model if x?x ≤ x, and it is a Kripkeexp -model if x ≤ x?x. Let σ denote a subset from the set {e, c, w, exp} and let F Lσ denote F L extended with the rules corresponding to the letters in σ. Completeness theorems hold for F Lσ with respect to Kripkeσ models (that is, the so-monoids which satisfy the requirements corresponding to σ (see [13])). Definition 3.1 A RelKripke-model will be called a RelKripkee -model if it satis?es the condition: (c18) Rabc implies Rbac; a RelKripke-model will be called a RelKripkec -model if it satis?es the condition: (c19) Raaa; a RelKripke-model will be called a RelKripkew -model if it satis?es the conditions: (c20) Rb1 b2 b and Rb3 b4 b1 imply ?q, q1, q2 (R?b3 q1 and R?b2 q2 and Rq1 q2 q); and x |= 0 if and only if R?xω and R?ωx; and ?nally, a RelKripke-model will be called a RelKripkeexp -model if it satis?es the condition: (c21) Rb1 b2 b and Rb3 b4 b1 and Rb5 b6 b3 imply ?q1 q2 (Ib6 b4 q1 and Rb5 q1 q2 and Rq2 b2 b). Theorem 3.2 (Soundness theorem for F Lσ ) If a sequent Γ → α is provable in F Lσ , then it is valid in all RelKripkeσ -models; in particular: (i) If we add condition (c18) to the list of conditions in de?nition 2.5, then we can prove the validity of the exchange rule, (e →). (ii) If we add condition (c19) to the list of conditions in de?nition 2.5, then we can prove the validity of the contraction rule, (c →). (iii) If we add the condition (c20) to the list of conditions in de?nition 2.5, we can prove the validity of the weakening rule, (w →); and if we add the condition x |= 0 if and only if x = ω to the list of conditions in de?nition 2.5, we can prove the validity of the weakening rule, (→ w). (iv) If we add condition (c21) to the list of conditions in de?nition 2.5, we can prove the validity of the expansion rule, (exp →). Proof. We shall prove that augmenting the de?nition of RelKripke-model by adding condition (c20) allows us to prove the validity of the weakening rule (w →). The reader can provide the details of the other assertions of this theorem. Assume that the sequent γ ? δ → θ is valid and assume R??x and Rxyz and y |= γ ? α ? δ. We must demonstrate that z |= θ. From the assumptions, we know ?y1 , y2 , y3 , y4 , such that (Ry1 y2 y and Ry3 y4 y1 ), and y2 |= δ, y3 |= γ and y4 |= α. Using (c20) we know ?z, z1 , z2 such that (R?y3 z1 and R?y2 z2 and Rz1 z2 z). Then remark 2.8 allows us to conclude z1 |= γ and z2 |= δ. Thus, z |= γ ? δ. R??? is true so ? |= γ ? δ ? θ. Since R?zz is true, we conclude z |= θ.

3. STRUCTURAL RULES FOR F L 687 Theorem 3.3 (Correspondence theorem) For every Kripke model D, g of F Lσ there is a RelKripke model M of F Lσ such that: if θ is not true in D, g , then θ is not true in M. Proof. Suppose θ is not true in the Kripke model D, g . Then there is x ∈ D such that x |= θ in D, g . De?ne the model M= S, ω, ?, R, I, g such that the set S consists of the elements of D, the distinguished elements ω and ? are the same as in D, the relations R and I are de?ned as: Rxyz i? x ? y ≤ z and Ixyz i? x ∩ y ≤ z, and, ?nally, such that g is the same as for D, g . Let us consider the case that σ is {w}, so we deal with F Lw . It is straightforward (and sometimes trivial) to show that the 17 conditions of de?nition 2.5 hold. (See [11]). We shall show that condition (c20) holds. Suppose Rabc and Rb1 b2 b and Rb3 b4 b1 . Then a ? b ≤ c and b1 ? b2 ≤ b and b3 ? b4 ≤ b1 . Let q1 = a ? b3 and q2 = b4 ? b2 . Then q1 ? q2 = (a? b3 )? (b4 ? b2 ) = a? (b3 ? b4 )? b2 ≤ a? b1 ? b2 ≤ a? b ≤ c. Moreover, since the Kripke model D, g is a model of F Lw , b3 ≤ a ? b3 (= q1 ) and b2 ≤ b4 ? b2(= q2 ). Thus we may conclude R?b3 q1 , R?b2 q2 and Rq1 q2 c. In such a manner, we may verify that M is a RelKripke-model in which (c20) is true. Further, x |= 0 i? R?xω and R?ωx, because in a Kripkew -model, g(0) is exactly the element ω. We may use induction on the length of the formula, θ, to prove that for ?x ∈ S, if x |= θ in M, then x |= θ in D, g . The contrapositive of this last statement gives us the result we seek. Theorem 3.4 (Completeness theorem for F Lσ ) Suppose the sequent Γ → α is valid in all RelKripkeσ -models. Then Γ → α is provable in F Lσ . Proof. Using a proof by contradiction, the above result follows immediately from the Correspondence theorem above. Now we must discuss the logic RF Lσ , the relational logic corresponding to F Lσ . The RF Lσ -models are found by taking those RF L-models which satisfy the conditions corresponding to whatever σ is. The RF Lσ -logic is an extension to RF L-logic, found by adding speci?c rules which correspond to the added conditions on the RelKripkeσ models. The speci?c rules corresponding to these conditions are as follows: Condition (c18) - exchange: Rbac Rbac, Rabc; Condition (c19) - contraction: Raaa Condition (c20) - weakening: ?Rb1 b2 b, ?Rb3b4 b1 ?Rb1 b2 b, ?Rb3b4 b1 , ?R?b3q1 , ?R?b2q2 , ?Rq1 q2 c

688 Relational Proof System for Linear and Other Substructural Logics Condition (c21) - expansion: ?Rb1 b2 b, ?Rb3b4 b1 , ?Rb5b6 b3 ?Rb1 b2 b, ?Rb3b4 b1 , ?Rb5b6 b3 , ?Ib6 b4 q1 , ?Rb5q1 q2 , ?Rq2b2 b The proof of the following is immediate from the de?nitions. Proposition 3.5 The speci?c rules corresponding to (c18), (c19), (c20) and (c21) are admissible. Tableau correctness and tableau completeness for RF Lσ -logic and RF Lσ -models follow as in the propositions 2.24 and 2.30 of Section 2. Appropriate analogues for lemma 2.34 and theorem 2.35 of Section 2 follow routinely for F Lσ and RelKripkeσ -models. Example 2.36 (Continued) If we apply the speci?c rule (c18), to the ?rst branch in the example at the end of the previous section, we end up with the sequence: ?Rwvz, (?α)wtu, (?β)vtu, ?Rxyz, Rwvz, Rvwz, (β ? α)ztu which is a fundamental sequence. Since F L does not have the exchange rule, it is sometimes convenient to introduce a second implication, ?′ , which is governed by the following rules: α, Γ → β Γ → α ?′ β (→?′ ) Γ→α ?, β, Σ → θ ?, Γα ?′ β, Σ → θ (?′ →)

We say that in the RelKripke model M, state x satis?es formula α ?′ β and write x |= α ?′ β i? ?x, y if y |= α and Ryxz then z |= β. Soundness for RelKripke-models follows with no additional conditions on R or I.

4

Logic of involutive quantales

Definition 4.1 A (noncommutative) quantale Q is a lattice having arbitrary joins together with an associative product ? satisfying the rule: a ? bi = (a ? bi) and ( ai ) ? b = (ai ? b), for all a, b, ai, bi ∈ Q. The quantale will be said to be unital provided that there is an element e ∈ Q such that: e ? a = a = a ? e, for all a ∈ Q. Quantales, a generalization of locales, have been de?ned and used by Mulvey in connection of his work in C*-algebras. Involutive quantales were introduced in [12]: the motivating example of an involutive quantale is the spectrum M axA of a noncommuta tive C*-algebra, where M axA is the involutive quantale consisting of closed linear subspaces of A. The lattice of relations on a set X is a quantale and was used by Hoare and He (see [10]) in the case that X was the set of states of a machine to construct the weakest speci?cation of one program with respect to another. Mulvey and Pelletier quantized the construction starting with a Hilbert space, H, of states rather than a set X of states; to do so they required the following notion of involutive quantale.

4. LOGIC OF INVOLUTIVE QUANTALES

689

Definition 4.2 An involutive quantale is a quantale Q together with an involution, ? ; that is, with a unary operation ? satisfying: (i) a?? = a; (ii) (a ? b)? = b? ? a? ; (iii) ( ai )? = (a? ). i Remark 4.3 We de?ne the partial order in the usual fashion: a ≤ b i? a ∨ b = b. If a ≤ b then (iii), above, tells us that a? ≤ b? . As discussed in [13], so-monoids and unital quantales come to the same thing (except that the order is reversed) - if we ignore the fact that quantales come equipped with arbitrary joins and just use binary joins. We consider here just binary joins. (Of course, we could, alternatively consider the in?nitary case; relational logic with in?nitary joins is discussed in [18].) To describe the logic of involutive quantales, denoted F LI , we thus require the rules of F L augmented with the following 7 rules of inference: Γ, γ → α?? Γ, γ → α (?? 1) Γ, γ → α Γ, γ → α??

?

(?? 2)

Γ, γ → ( αi )? Γ, γ → ( α? ) i

(

1)

Γ, γ → ( α? ) i Γ, γ → ( αi )?

(

?

2)

Γ, γ → (α ? β)? (?? 1) Γ, γ → (β ? ? α? ) Γ→α Γ? → α ? (? )

Γ, γ → (α? ? β ? ) (?? 2) Γ, γ → (β ? α)?

If Γ is γ1 , γ2 , ..., γn, then Γ? denotes (γ1 ? γ2 ? ... ? γn )? . Definition 4.4 An involutive monoid, D = D, ∩, ?,? , ?, ω , is an so-monoid with a unary operator ? satisfying the following conditions: (i) x?? = x; (ii) (x ? y)? = y? ? x? ; and, (iii) (x ∩ y)? = x? ∩ y? . Definition 4.5 A KripkeI -model is a pair D, g consisting of an involutive monoid D and a mapping, g, as described in de?nition 2.3 satisfying, in addition to all the conditions of de?nition 2.3, the condition: x |= α? i? x? |= α. Proposition 4.6 (Soundness and Completeness) Let Γ → α be a sequent of F LI . Then Γ → α is provable in F LI i? Γ → α is valid in all F LI -models. Proof. Let D, g be a KripkeI -model. We ?rst need to show that the set of x such that x |= α? is a ?lter. So, we need to show that if x |= α? and y |= α? and x ∩ y ≤ z, then z |= α? , or, equivalently, z ? |= α. But we know x? |= α?, and y? |= α?

690 Relational Proof System for Linear and Other Substructural Logics and, also, x? ∩ y? = (x ∩ y)? ≤ z ? . Since KripkeI -models are Kripke-models, we may conclude that z ? |= α. Consequently, z |= α? . We also need to show that rules of inference of F LI preserve validity in KripkeI -models. Of course we only need to ? concern ourselves with the 7 rules listed above. We demonstrate the validity of ( 2). Assume for all x ≥ ?, x |= γ ? α? ∨ α?. Suppose now that ? ≤ x and Rxyz and y |= γ. 1 2 We need to show z |= (α1 ∨ α2 )? . Thus, we need to show that z ? |= (α1 ∨ α2 ). By assumption, z |= α? ∨ α? . So ?z1 , z2 , such that z1 ∩ z2 ≤ z and (z1 |= α? or z1 |= α?), 1 2 1 2 ? ? ? and (z2 |= α? or z2 |= α? ). (Equivalently, (z1 |= α1 or z1 |= α2 ), and (z2 |= α1 or 1 2 ? z2 |= α2 ).) Since D is an involutive monoid, z1 ∩ z2 ≤ z implies (z1 ∩ z2 )? ≤ z ? , and ? ? so z1 ∩ z2 ≤ z ? ; clearly, the desired result now follows. The other rules follow just as easily. Completeness is by the usual Lindenbaum-Tarski argument. Definition 4.7 By a RelKripkeI -model we shall mean a RelKripke-model (as in de?nition 2.5) with the further conditions: (c-I1) (c-I2) (c-I3) (c-I4) (c-I5) (c-I6) R?a?? a; R?aa?? ; Iabc? implies Ia? b? c; Iabc implies Ia? b? c? ; Rabc? implies Rb?a? c; Rabc implies Rb?a? c? ;

Theorem 4.8 (Soundness theorem for F LI ) If a sequent Γ → α is provable in F LI , then it is valid in all RelKripkeI -models. Proof. First we need to show that if x |= α? and y |= α? and Ixyz then z |= α? . This follows immediately from (c-I4). Now to the seven rules of inference (as a ? RelKripkeI - model is a RelKripke-model). To show that the rule ( 2) preserves validity in RelKripkeI -models, follow the proof of the preservation of the validity of this rule in KripkeI -models, replacing a ∩ b ≤ c by Iabc. Then use (c-I4) as listed above. To prove the other rules, use the conditions as indicated below: (?? 1) - use (c-I1) and remark 2.8. (?? 2) - use (c-I2) and remark 2.8. ? ( 1) - use (c-I3); (?? 1) - use (c-I5); (?? 2) - use (c-I6); (? ) - use (c10) and remark 2.8. The following are straightforward extensions of the theorems in Section 2 for F L. Theorem 4.9 (Correspondence theorem) For every KripkeI -model, D, g , of F LI there is a RelKripkeI -model, M, of F LI such that, if θ is not true in D, g , then θ is not true in M. Theorem 4.10 (Completeness theorem) Suppose the sequent Γ → α is valid in all RelKripkeI models. Then Γ → α is provable in F LI .

5. LINEAR LOGIC WITH EXPONENTIALS

691

We now brie?y discuss RF LI -logic and RF LI -models. To take care if the involution, we must de?ne a unary operation ? on the family of ternary relations as follows: let A be a ternary relation on a set U , then: A? = {(a, b, c) | (a? , b, c) ∈ A}. Clearly, if A is an ideal relation, then A? is an ideal relation. An RF LI -model is a 7-tuple M = (U, R, I,? , ω, ?, m), where ? is a unary operation, and U, R, I, ω, ?, and m are as in de?nition 2.16. The RF LI -logic will be RF L-logic augmented with decomposition rules for the operation ? , as well as speci?c rules corresponding to (cI1) to (c-I6). The speci?c rules are straightforward to write down, so we leave this to the reader. The decomposition rules for the connective ? are exactly as one would expect; to wit:

?

(A )xtu Ax? tu

?

?? ?(A? )xtu ?Ax? tu

Decomposition and speci?c rules are admissible, so we may prove the propositions, lemma and theorem corresponding to propositions 2.24 and 2.30, lemma 2.32 and theorem 2.35.

5

Linear logic with exponentials

Gentzen rules for (noncommutative) linear logic with modal operators ! and ?, denoted by F LM , are found by adding the following 8 rules to the Gentzen rules for F L : Γ, α, ? → θ Γ, !α, ? → θ Γ, ? → θ Γ, !α, ? → θ Γ, !α, β, ? → θ Γ, β, !α, ? → θ !Γ, α, !? →?θ !Γ, ?α, !? →?θ (! →) !Γ → α !Γ →!α !Γ, !α, !α? → θ !Γ, !α, ? → θ Γ, → Γ →?α Γ, → α Γ →?α (→?) (→!)

(!w)

(!c)

(!e)

(?w)

(? →)

If Γ is the sequence γ1 , γ2 , ..., γn then !Γ denotes !γ1 , !γ2 , ..., !γn. To determine a Kripke model for formulas with model operators ! and ?, Ono [13] gave the following de?nition: Definition 5.1 Let D = D, ∩, ?, ?, ω be an so-monoid with ?xed elemet ? ∈ D and let F and G be binary operations on D satisfying the following conditions: (1) if ? ≤ x then F ?x;

692 Relational Proof System for Linear and Other Substructural Logics (2) if F yx and x ≤ x′ then F yx′ ; (3) if F yx then ? ≤ y and y ? y ≤ x; (4) if F yx, then there is some u such that F yu and F ux; (5) if F yx then there exists w such that F yw and for every u, w ? u ≤ u ? x and u ? w ≤ x ? u; (6) if F ya and F y′ x′ then F y ∩ y′ x ∩ x′ and F y ? y′ x ? x′ ; (7) if Gyx and x ≤ x′ then Gyx′ ; (8) Gyx for every y if and only if ? ≤ x; (9) if Gyx and Gyx′ then Gyx ∩ x′ ; (10) for every x and y there exists a z such that if F xu for some u then: Gyx ? z and for every w, Gyx ? w i? Gzw. Then D, g is a KripkeM -model if g is a mapping as described in de?nition 2.3, with the added conditions that: x |=!α i? z |= α for some z such that F zx; x |=?α i? for every y, if z |= α implies Gyz for every z, then Gyx. Soundness and completeness for F LM with respect to KripkeM -models were proved in [13]. Definition 5.2 A RelKripkeM -model is a RelKripke-model with 2 binary accessibility relations F and G, satisfying the following conditions: (c-M0) Iabc and R?a′ b imply Ia′ bc; (c-M1) R??a implies F ?a; (c-M2) F ab and R?bb′ implies F ab′ ; (c-M3) F ba implies R??b and Rbba; (c-M4) F ba implies ?q(F bq and F qa); (c-M5) F ba implies ?q(F bq and ?u, h((Ruah implies Rquh) and (Rauh implies Ruqh))); (c-M6(i)) F ba and F b′ a′ implies ?a′′ ?b′′ (Ibb′ b′′ and Iaa′ a′′ and F b′′a′′ ); (c-M6(ii)) F ba and F b′ a′ implies ?b′′ ?a′′ (Rbb′ b′′ and ?h(Rbb′ h implies R?b′′ h) and Raa′ a′′ and ?h(Raa′ h implies R?a′′ h) and F b′′ a′′ ); (c-M7) Gba and R?aa′ imply Gba′ ; (c-M8(i)) (?bGba) implies R??a; (c-M8(ii)) R??a implies ?bGba; (c-M9) Gba and Gba′ and Iaa′ a′′ imply Gba′′ ; (c-M10(i)) ?q1 (?q2 F aq2 implies ((?q3 (Raq1 q3 and ?h(Raq1 h implies R?q3h) and Gbq3)) and (?c?q4 (Racq4 and ?h(Rach implies R?q4h) and Gbq4 ) if Gq1c))); (c-M10(ii))?q1 (?q2 F aq2 implies ((?q3 (Raq1 q3 and ?h(Raq1 h implies R?q3h) and Gbq3)) and (?c?q4 (Racq4 and ?h(Rach implies R?q4h) and Gbq4 ) only if Gq1 c)) ); (c-M11) Rabc and R?cd implies Rabd; (c-M12) ?c(Rabc and ?h(Rabh implies R?ch)). and x |=!α and x |=?α are de?ned as in the de?nition of KripkeM -model. Remark 5.3 Using (c13) of de?nition 2.5, we may immediately deduce that R??b and Rbba implies R?ba. Consequently, if F ba then R?ba. As mentioned previously, (c12) and (c13)

5. LINEAR LOGIC WITH EXPONENTIALS

693

articulate the monotonicity of ?, while (c15) articulates associativity. In addition, the reader should note that (c-M12) combined with (c-M11) (which gives transitivity) really allows us to deal with c as equal to a ? b. Theorem 5.4 (Soundness for F LM ) If a formula is provable in F LM -logic, then it is valid in all RelKripkeM -models. Proof. The ?rst thing we need to check is that if x |= θ and y |= θ and Ixyz then z |= θ for θ =!α or ?α. Now if x |=!α, and y |=!α, there exist x′ , y′ such that x′ |= α and F x′ x and y′ |= α and F y′ y. If Ixyz we then need to show that there exists z ′ such that z ′ |= α and F z ′ z. In fact, we shall show that z |= α; then, since F zz, we shall have what we need. By remark 2.28 we know that R?x′ x and R?y′ y and by (c-M0), Ixyz and R?x′ x imply Ix′ yz which, by (c4), implies Iy′ xz. Using remark 2.28 and (c4) again, we obtain Ix′ y′ z. Thus, by properties of RelKripke-models, z |= α. We can use (c-M9) to show that if x |=?α and y |=?α and Ixyz then z |=?α. The next thing we need to show is that each of the 8 rules of inference is valid in RelKripkeM -models. We shall demonstrate the validity of the most di?cult rule of inference, (? →). Assume !γ ? α?!δ ??θ is valid. Suppose R??v and Rvxu and x |=!γ??α?!δ. It su?ces to demonstrate that x |=?θ (because this then tells us that u |=?θ). By supposition, ?r, w, y, z such that: Ryzx and Rrwx and r |=!γ??α, y |=!γ, z |=?α, and w |=!δ. By de?nition of w |=!δ, ?w0 (F w0 w and w0 |= δ). By (c-M5), ?q(F w0 w ′ and ?z, h((Rzwh implies Rw ′ zh) and (Rwzh implies Rzw ′ h))). (1) By (c-M12), ?c1 (Rw ′ zc1 and ?h(Rw ′ zh implies R?c1 h)) and ?c2 (Rzwc2 and ?h(Rzwh implies R?c2 h)). Using (c-11),(c-M11), (1) and (c-M12), we may conclude R?c1 c2 . Then by (c-M12), again, we know: ?c3 (Ryzc3 and ?h(Ryzh implies R?c3 h)). Consequently, R?c3 r and this, with Rrwx and (c-13), allows to conclude Rc3 wx. From the de?nition of y |=!γ, we know ?y0 (F y0 y and y0 |= γ). Then from (c-M4), we know ?y1 , w1 (F y0 y1 , F y1 y, F w0 w1 and F w1 w ′ ); hence y1 |=!γ and R?y1 y and R?w1 w ′ . By(c-M5) ?w2 (F w0 w2 and, ?h((Rtw1 h implies Rw2 th) and (Rw1 th implies Rtw2 h)). Assume u |= θ implies Gvu for any u. (2) Suppose t |= α. Since F w0 w2 , we know w2 |=!δ. Since R???, the original assumption tells us that for all u, v if R?uv and u |=!γ ? α?!δ, then v |=?θ. By (c-M12), ?c4 (Rw1 tc4 and ?h(Rw1 th implies R?c4 h)) and ?c5 (Rtw2 c5 and ?h(Rtw2 h implies R?c5 h)). As above, we deduce R?c5 c4 . Again by (c-M12), ?d(Ry1 c5 d and ?h(Ry1 c5 h implies R?dh)). We may conclude d |=!γ ? (α?!δ). Again by (c-M12), ?f(Ry1 c4 f and ?h(Ry1 c4 h implies R?df). We can deduce R?df; whence f |=?θ. Use (2) and the de?nition of f |=?θ to conclude Gvf. By (c-M6), we know ?y′′ w ′′ (Ry1 w1 y′′ and Ryw ′ w ′′ and ?h(Ry1 w1 h implies R?y′′ h) and ?h(Ryw ′ h implies R?w ′′ h) and F y′′ w ′′ ). (3) By (c-M10) ?w x , sx(Ry′′ w x sx and ?h(Ry′′ w xh implies R?sx h) and Gvsx ) and for every w + , ?s+ (Ry′′ w + s+ and ?h(Ry′′ w + h implies R?s+ h) and Gvs+ ) i? Gw xw + ). (4)

694 Relational Proof System for Linear and Other Substructural Logics Let w + = t in the above; so then ?s+ (Ry′′ ts+ and ?h(Ry′′ th implies R?s+ h) and Gvs+ ) i? Gw x t. We wish to show Gvs+ for some s+ . We already know Gvf. We need to show (Ry′′ tf and ?h(Ry′′ th implies R?fh)). Use the fact that Rw1 tc4 and Ry1 c4 f and (c15), to conclude Ry1 w1 c6 ; then, from (3), we know R?y′′ c6 . Using (c13), we may conclude Ry′′ tf. In all we have t |= α implies Gw xt for any t. Since z |=?α we conclude Gw xz. From (4) we know ?sz (Ry′′ zsz and ?h(Ry′′ zh implies R?sz h) and Gvsz ). By de?nition, then sz |=?θ. Once we show R?sz x we may conclude x |=?θ. We show this by demonstrating (using (c12), (c13) and (cM11)): ?h(R?xh implies Rrwh); ?h(Rrwh implies Ryc2 h); ?h(Ryc2 h implies Ryc1 h); ?h(Ryc1 h implies Rw ′′ zh); ?h(Rw ′′ zh implies Ry′′ zh); and, ?nally, ?h(Ry′′ zh implies R?sz h). Correpondence and Completeness theorems for F LM with respect to RelKripkeM models follow as in earlier sections. We now brie?y consider RF LM -logic and RF LM -models. First of all we need to deal with formulas as ternary relations, so F and G will be considered as ternary relations with no restriction on the third variable. For any relation A, we de?ne the ternary relations !A and ?A as follows:

?A = {(a, b, c) | ?d( if ?e((e, b, c) ∈ A implies (d, e, c) ∈ G), then (d, a, c) ∈ G)}

!A = {(a, b, c) | ?d((d, b, c) ∈ A and (d, a, c) ∈ F }.

One can demonstrate that if A is an ideal relation then both !A and ?A are ideal relations. RF LM -models have the expected de?nition (add two more ternary relations and the conditions (c-M0)-(c-M12) to de?nition of RF L-model). The decomposition rules for RF LM -logic are the decomposition rules for RF L as well as the following four rules.

! (Tagged) !Axtu !Axtu, Aztu !Axtu, F zxu

?! ?!Axtu ?Aztu, ?F zxu

6. SOME OPEN PROBLEMS AND FUTURE DIRECTIONS ? (z is Tagged) ?Axtu Aztu, Gyxu ?? (y is Tagged) ??Axtu ?z(?Aztu, Gyzu)

695

?Gyzu, Gyxu

?Gyxu

In the last two speci?c rules, only one of the two variables introduced on the lower line is taggged. The speci?c rules for RF LM -logic are determined as before; the rules corresponding to (c-M5), (c-M6(ii)), (c-M8(ii)), (c-M10(i)), (c-M10(ii)) and (c-M12) will be tagged, which will necessitate their reapplication for each object expression on the branch (see de?nition 2.25(1) for completeness of the decomposition tree). Some of the conditions require multiple branches and ?rst order decomposition rules (see [4]). The speci?c rule for (c-M4) is easily seen to be: ?F yxz ?F yxz, ?F yuz, ?F uxz; while the speci?c rule for (c-M8(ii)) will be: ?R??x ?R??x, ?Gyxz (where y is a tagged variable). Decomposition and speci?c rules are admissible: so a fundamental decomposition tree for a formula θ of F ML -logic tells us that θ is a theorem of F ML . Some of the rules for ! or ? may be dropped if we consider F LM augmented with some structural rules. Once we add cut rules for F and G, we may prove a correspondence theorem and then the constructive completeness of the tableau procedure for RF LM -logic and RF LM -models (a proposition analogous to proposition 2.30). Then we may ?nish with the analogue for theorem 2.35 for F LM and RelKripkeM -models.

6

Some open problems and future directions

In [5], a sequent-style deductive system is considered with a branching rule PB (Principle of Bivalence), which is crucial in proving the (constructive) completeness of a labelled tableau proof system for the multiplicative fragment of F L and F Lσ . We note here that our deductive apparatus works to provide proofs and ?nds countermodels for all of propositional F Lσ , as well as for other logics. Much remains to be done to determine procedures which will terminate a tableau (so that we may conclude that a branch is nonfundamental), to determine if the procedure is decidable with respect to any fragments of the logics considered and to develop e?cient strategies to implement the algorithm. Buszkowski and Orlowska [4] are working on decidability questions for relational formulations of information logics. The large number of tagged rules for RF LM -logic as well as ?rst order decomposition rules may prevent this strategy from being e?ectively implemented for theorem proving in F LM . Herment and Orlowska [9] have included relational logic in a system for graphical edition of proofs.

696 Relational Proof System for Linear and Other Substructural Logics Our RelKripkeX semantics di?er from the relational semantics RelSem for LC (a version of Lambek calculus) of Andreka and Mikulas [3]. In [3], the relational models are Kripke models W, C, v , where the worlds are pairs, i.e., W is a transitive binary relation and C is a ternary relation de?ned as follows: Cxyz i? y = a, b , z = b, c , x = a, c for some a, b, c (and v is a valuation). Such a relational Kripke frame has been termed by Doˇen [6] as a “two dimensional ternary frame”. When [3] s augmented the sequent rules of LC by adding the rules (∨ →), (→ ∨1 ) and (→ ∨2 ) for ∨, strong completeness failed, and they did not have a completeness proof. Our RelKripkeσ -models exhibit completeness with respect to F Lσ , which includes the above three rules for ∨. The question of strong completeness remains open. We plan to compare the relational semantics discussed here with the RelSem of [3]. Our RelKripke semantics also di?ers from the Kripke semantics of Allwein and Dunn. The relational semantics corresponding to Kripke semantics developed in [1] would require three ternary relations and two partial orders and each connective would require four decomposition rules (because the Kripke valuations have three values). Thus the relational semantics would be more complicated, though they do have more expressive power as far as developing Kripke semantics for all the (nonmodal) connectives of nonassociative Linear Logic. In [2], we develop Kripke semantics for Gelfand logic. (Add to the de?nition of involutive monoid the following axiom: (?b(a ? b ≤ a)) implies (a ? a? ? a = a). Other interesting open questions are: Does each RelKripkeX -model give rise to a KripkeX -model with the same set of true formulas? What is the relationship of the class of RelKripkeX -models to the class of RF LX -algebras? (The class of RF LX algebras generated by a RelKripkeX -model M is the isomorphic copies of subalgebras of direct products of algebras which have as elements, the ideal relations over the set M , and which have as operations, logical operations. Orlowska (personal communication) has suggested that it would be interesting to try to formulate some general observations as to what kinds of algebraic systems could be coded using relational systems (of the kinds featured here). A worthwhile invertigation would be the characterization of classes de?nable relationally and the characterization of the relational conditions (on accessibility relations) which can be represented in the form of a relational rule. Andreas Blass, (personal communication) posed the following question: can we take the direct route to the completeness theorem; that is, if a formula is valid in RF LX -models can we show that it has a fundamental decomposition tree? Finally, one anonymous referee for this paper suggested that I should attempt ?nd a complete calculus in the language of F L rather than use the enriched language presented here. Such semantical considerations are investigated in the framework of modal and algebraic logic, (see [20]), but the connections between arrow logic and substructural logics remain to be investigated.

Acknowledgements

This research was partially supported by a St. Francis Xavier University Council for Research Grant #91885. The author wishes to thank the referees for their comments and suggestions.

6. SOME OPEN PROBLEMS AND FUTURE DIRECTIONS

697

References

[1] Gerard Allwein and J.Michael Dunn, Kripke models for linear logic, Journal of Symbolic Logic 58:514–545, 1993. [2] Gerard Allwein and Wendy MacCaull, A Kripke semantics for the logic of Gelfand quantales, in preparation. [3] Hajnal Andreka and Szabolcs Mikulas, Lambek calculus and its relational semantics: completeness and incompleteness, Journal of Logic, Language and Information 3:1–38, 1994. [4] Wojciech Buszkowski and Ewa Orlowska, Relational formalization of dependencies in information systems, Preprint, 1995. [5] Marcello D’Agostino and Dov Gabbay, A generalization of analytic deduction via labelled deductive systems I: Basic substructural logics, Journal of Automated Reasoning 13:243–281, 1994. [6] Kosta Doˇen, A brief survey of frames for the Lambek calculus, Zeitschr. f. Mathematische Logik s und Grundlagen d. Math 38:179–187, 1992. [7] J.Michael Dunn, Partial gaggle theory applied to logics with restricted structural rules, in Substructural Logics, eds: P. Schroeder-Heister and K. Doˇen, Oxford University Press, 1993, pp. s 63–102. [8] Dov Gabbay, A general theory of structured consequence relations, in Substructural Logics , eds: P. Schroeder-Heister and K. Doˇen, Oxford University Press, 1993, pp. 109–152. s [9] Michel Herment and Ewa Orlowska, Handling information logics in a graphical proof editor, Computational Intelligence 11:297–322, 1995. [10] C.A.R. Hoare and He Jifeng, A weakest pre-speci?cation, Inform. Process. Lett. 24:127–132, 1987. [11] Wendy MacCaull, Relational semantics and a relational proof system for full Lambek calculus, to appear, Journal of Symbolic Logic. [12] Chris Mulvey and Joan Wick Pelletier, The quantization of the calculus of relations, Canadian Mathematical Society Conference Proceeding 13, American Mathematical Society, 1992. [13] Hiroakira Ono, Semantics for substructural logics, in Substructural Logics, eds: P. SchroederHeister and K. Doˇen, Oxford University Press, 1993, pp. 259–291. s [14] Hiroakira Ono and Yuichi Komori, Logics without the contraction rule, Journal of Symbolic Logic 50:169–201, 1985. [15] Ewa Orlowska, Relational interpretation of modal logics, in Algebraic Logic, ed: H. Andreka et al., North Holland, 1991, pp. 443–471. [16] Ewa Orlowska, Relational proof system for relevant logics, Journal of Symbolic Logic 57:1425– 1440, 1992. [17] Ewa Orlowska, Relational semantics for nonclassical logics: formulas are relations, in Philosophical Logic in Poland, ed: Jan Wolenski, Kluwer, 1994, pp. 167–186. [18] Ewa Orlowska, Relational proof systems for modal logics, in Proof Theory for Modal Logics, ed: H. Wansing, to appear. [19] Richard Routley and Robert Meyer, The semantics of entailment, in Truth, Syntax and Modality, ed: H.LeBlanc, North Holland, 1973. [20] Yde Venema, A crash course in arrow logic, in Arrow logic and Multi-modal Logic, series Studies in Logic, Language and Information, eds: L.Polos, M.Marx and M.Masuch, CSLI Stanford, 1996. [21] Heinrich Wansing, Informational interpretation of substructural logics, Journal of Logic, Language and Information 2:285–308, 1993.

Received 2 August 1996. Revised 20 December 1996

赞助商链接

更多相关文档:

更多相关标签:

相关文档

- 9 Constructive Logics. Part II Linear Logic and Proof Nets
- SUBSTRUCTURAL LOGICS
- Proof Theory in Linear Logic A Specification of Concurrent Objects (Draft)
- On Structuring Proof Search for First Order Linear Logic
- Proof theory for full intuitionistic linear logic, bilinear logic
- The semantics and proof theory of linear logic
- Type System and Logics- Pure Type Systems- The Lambda Cube- The Logic Cube Extensions of
- 9 Constructive Logics. Part II Linear Logic and Proof Nets
- Proof search in first-order linear logic and other cut-free sequent calculi
- A Proof System and a Decision Procedure for Equality Logic
- Proof search and proof nets construction in linear logic
- System description proof planning in higher-order logic with CLAM
- Project-Team Calligramme Linear Logic, Proof Nets and Categorial Grammars
- ARE OTHER LOGICS POSSIBLE MACCOLL’S LOGIC
- ABSTRACT A COMPILER SYSTEM OF A LINEAR LOGIC PROGRAMMING LANGUAGE

文档资料共享网 nexoncn.com
copyright ©right 2010-2020。

文档资料共享网内容来自网络，如有侵犯请联系客服。email:zhit325@126.com