Extending intuitionistic linear logic with knotted structural rules.

AbstractWe introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers and which arise from observing restrictions on structural rules on the level of terms as well as propositions. We discuss computational interpretations, based on sharing, at both the propositional and predicate levels.

Download Full-text

Relations and Non-commutative Linear Logic

DAIMI Report Series ◽

10.7146/dpb.v20i372.6604 ◽

1991 ◽

Vol 20 (372) ◽

Cited By ~ 4

Author(s):

Carolyn Brown ◽

Doug Gurr

Keyword(s):

Intuitionistic Logic ◽

Arbitrary Number ◽

Linear Logic ◽

Expressive Power ◽

Cut Elimination ◽

Natural Class ◽

Structural Rules ◽

Restricted Sense ◽

Intuitionistic Linear Logic ◽

Natural Way

<p>Linear logic differs from intuitionistic logic primarily in the absence of the structural rules of weakening and contraction. Weakening allows us to prove a proposition in the context of irrelevant or unused premises, while contraction allows us to use a premise an arbitrary number of times. Linear logic has been called a ''resource-conscious'' logic, since the premises of a sequent must appear exactly as many times as they are used.</p><p>In this paper, we address this ''experimental nature'' by presenting a non-commutative intuitionistic linear logic with several attractive properties. Our logic discards even the limited commutativityof Yetter's logic in which cyclic permutations of formulae are permitted. It arises in a natural way from the system of intuitionistic linear logic presented by Girard and Lafont, and we prove a cut elimination theorem. In linear logic, the rules of weakening and contraction are recovered in a restricted sense by the introduction of the exponential modality(!). This recaptures the expressive power of intuitionistic logic. In our logic the modality ! recovers the non-commutative analogues of these structural rules. However, the most appealing property of our logic is that it is both sound and complete with respect to interpretation in a natural class of models which we call relational quantales.</p>

Download Full-text