Exchange rules

2001 ◽  
Vol 66 (2) ◽  
pp. 509-516 ◽  
Author(s):  
Mario Piazza
Keyword(s):  
Linear Logic ◽  
Expressive Power ◽  
Theoretical Argument ◽  
Structural Rules

AbstractIn this paper, we show by a proof-theoretical argument that in a logic without structural rules, that is in noncommutative linear logic with exponentials, every formula A for which exchange rules (and weakening and contraction as well) are admissible is provably equivalent to? A. This property shows that the expressive power of “noncommutative exponentials” is much more important than that of “commutative exponentials”.

scholarly journals Relations and Non-commutative Linear Logic

1991 ◽  
Vol 20 (372) ◽  
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>

scholarly journals Possession as Linear Knowledge

10.29007/ntkm ◽  
2018 ◽  
Author(s):  
Frank Pfenning
Keyword(s):  
Distributed System ◽  
Epistemic Logic ◽  
Linear Logic ◽  
Expressive Power ◽  
Cut Elimination ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Ongoing Effort ◽  
Multi Agent ◽  
Localized Knowledge

Epistemic logic analyzes reasoning governing localized knowledge, and is thus fundamental to multi- agent systems. Linear logic treats hypotheses as consumable resources, allowing us to model evolution of state. Combining principles from these two separate traditions into a single coherent logic allows us to represent localized consumable resources and their flow in a distributed system. The slogan “possession is linear knowledge” summarizes the underlying idea. We walk through the design of a linear epistemic logic and discuss its basic metatheoretic properties such as cut elimination. We illustrate its expressive power with several examples drawn from an ongoing effort to design and implement a linear epistemic logic programming language for multi-agent distributed systems.

Logique, effectivité et faisabilité

Dialogue ◽  
1997 ◽  
Vol 36 (1) ◽  
pp. 45-68 ◽  
Author(s):  
Jacques Dubucs
Keyword(s):  
Linear Logic ◽  
Structural Rules ◽  
Philosophical Foundations ◽  
Logical Rule ◽  
Practical Feasibility

AbstractThis paper can be read as an attempt at providing philosophical foundations to linear logic. The only plausible form of philosophical antirealism deals with practical feasibility rather than with effectivity in principle. The very notion of recognizability is ambiguous, audit has to be considered from a stricter perspective than currently done. The intuitionistic assertability conditions are to be reinforced. This change requires a move towards a frame in which the circumstances of the application of a logical rule can be specified. Gentzen's sequential calculi provide such a frame, when some structural rules have been removed or limited.

On the unification of classical, intuitionistic and affine logics

2018 ◽  
Vol 29 (8) ◽  
pp. 1177-1216
Author(s):  
CHUCK LIANG
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Kripke Semantics ◽  
Cut Elimination ◽  
Structural Rules ◽  
Phase Semantics ◽  
Intuitionistic Logics

This article presents a unified logic that combines classical logic, intuitionistic logic and affine linear logic (restricting contraction but not weakening). We show that this unification can be achieved semantically, syntactically and in the computational interpretation of proofs. It extends our previous work in combining classical and intuitionistic logics. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. We define a phase semantics for this logic that naturally extends the Kripke semantics of intuitionistic logic. We present a sequent calculus with novel structural rules, which entail a more elaborate procedure for cut elimination. Computationally, this system allows affine-linear interpretations of proofs to be combined with classical interpretations, such as the λμ calculus. We show how cut elimination must respect the boundaries between classical and non-classical modes of proof that correspond to delimited control effects.

On bunched typing

2003 ◽  
Vol 13 (4) ◽  
pp. 747-796 ◽  
Author(s):  
PETER O'HEARN
Keyword(s):  
Additive Function ◽  
Linear Logic ◽  
Type System ◽  
The Other ◽  
Basic System ◽  
Interference Control ◽  
Joint Work ◽  
Function Type ◽  
Structural Rules ◽  
Single Category

We study a typing scheme derived from a semantic situation where a single category possesses several closed structures, corresponding to different varieties of function type. In this scheme typing contexts are trees built from two (or more) binary combining operations, or in short, bunches. Bunched typing and its logical counterpart, bunched implications, have arisen in joint work of the author and David Pym. The present paper gives a basic account of the type system, and then focusses on concrete models that illustrate how it may be understood in terms of resource access and sharing. The most basic system has two context-combining operations, and the structural rules of Weakening and Contraction are allowed for one but not the other. This system includes a multiplicative, or substructural, function type −∗ alongside the usual (additive) function type $\rightarrow$; it is dubbed the $\alpha\lambda$-calculus after its binders, $\alpha$ for the $\alpha$dditive binder and $\lambda$ for the multiplicative, or $\lambda$inear, binder. We show that the features of this system are, in a sense, complementary to calculi based on linear logic; it is incompatible with an interpretation where a multiplicative function uses its argument once, but perfectly compatible with a reading based on sharing of resources. This sharing interpretation is derived from syntactic control of interference, a type-theoretic method of controlling sharing of storage, and we show how bunch-based management of Contraction can be used to provide a more flexible type system for interference control.

scholarly journals Pretopologies and completeness proofs

1995 ◽  
Vol 60 (3) ◽  
pp. 861-878 ◽  
Author(s):  
Giovanni Sambin
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Predicate Logic ◽  
Linear Logic ◽  
Double Negation ◽  
Open Problems ◽  
Completeness Proof ◽  
Structural Rules ◽  
First Order ◽  
Definition Of

Pretopologies were introduced in [S], and there shown to give a complete semantics for a propositional sequent calculus BL, here called basic linear logic, as well as for its extensions by structural rules, ex falso quodlibet or double negation. Immediately after Logic Colloquium '88, a conversation with Per Martin-Löf helped me to see how the pretopology semantics should be extended to predicate logic; the result now is a simple and fully constructive completeness proof for first order BL and virtually all its extensions, including the usual, or structured, intuitionistic and classical logic. Such a proof clearly illustrates the fact that stronger set-theoretic principles and classical metalogic are necessary only when completeness is sought with respect to a special class of models, such as the usual two-valued models.To make the paper self-contained, I briefly review in §1 the definition of pretopologies; §2 deals with syntax and §3 with semantics. The completeness proof in §4, though similar in structure, is sensibly simpler than that in [S], and this is why it is given in detail. In §5 it is shown how little is needed to obtain completeness for extensions of BL in the same language. Finally, in §6 connections with proofs with respect to more traditional semantics are briefly investigated, and some open problems are put forward.

SN and CR for free-style LKtq: linear decorations and simulation of normalization

2002 ◽  
Vol 67 (1) ◽  
pp. 162-196 ◽  
Author(s):  
Jean-Baptiste Joinet ◽  
Harold Schellinx ◽  
Lorenzo Tortora De Falco
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Present Report ◽  
Point Of View ◽  
Strong Normalization ◽  
Structural Rules ◽  
Specific Combination ◽  
Proof Nets ◽  
Classical Proof

AbstractThe present report is a, somewhat lengthy, addendum to [4], where the elimination of cuts from derivations in sequent calculus for classical logic was studied ‘from the point of view of linear logic’. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives.The main novelty here is the observation that this type-distinction is not essential: we can allow classical sequent derivations to use any combination of additive and multiplicative introduction rules for each of the connectives, and still have strong normalization and confluence of tq-reductions.We give a detailed description of the simulation of tq-reductions by means of reductions of the interpretation of any given classical proof as a proof net of PN2 (the system of second order proof nets for linear logic), in which moreover all connectives can be taken to be of one type, e.g., multiplicative.We finally observe that dynamically the different logical cuts, as determined by the four possible combinations of introduction rules, are independent: it is not possible to simulate them internally, i.e.. by only one specific combination, and structural rules.

Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic

1991 ◽  
Vol 56 (4) ◽  
pp. 1403-1451 ◽  
Author(s):  
V. Michele Abrusci
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Commutative Monoid ◽  
Structural Rules ◽  
Exchange Rule ◽  
Phase Semantics ◽  
Correct Program ◽  
Image Position

The linear logic introduced in [3] by J.-Y. Girard keeps one of the so-called structural rules of the sequent calculus: the exchange rule. In a one-sided sequent calculus this rule can be formulated asThe exchange rule allows one to disregard the order of the assumptions and the order of the conclusions of a proof, and this means, when the proof corresponds to a logically correct program, to disregard the order in which the inputs and the outputs occur in a program.In the linear logic introduced in [3], the exchange rule allows one to prove the commutativity of the multiplicative connectives, conjunction (⊗) and disjunction (⅋). Due to the presence of the exchange rule in linear logic, in the phase semantics for linear logic one starts with a commutative monoid. So, the usual linear logic may be called commutative linear logic.The aim of the investigations underlying this paper was to see, first, what happens when we remove the exchange rule from the sequent calculus for the linear propositional logic at all, and then, how to recover the strength of the exchange rule by means of exponential connectives (in the same way as by means of the exponential connectives ! and ? we recover the strength of the weakening and contraction rules).

The Logic of Bunched Implications

1999 ◽  
Vol 5 (2) ◽  
pp. 215-244 ◽  
Author(s):  
Peter W. O'Hearn ◽  
David J. Pym
Keyword(s):  
Intuitionistic Logic ◽  
Linear Logic ◽  
Structural Rules ◽  
Intuitionistic Linear Logic

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.

Sign in / Sign up

Export Citation Format

Share Document