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.

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 Connecting Sequent Calculi with Lorenzen-Style Dialogue Games

2021 ◽  
pp. 115-141
Author(s):  
Christian G. Fermüller
Keyword(s):  
Intuitionistic Logic ◽  
Linear Logic ◽  
Substructural Logics ◽  
Point Of View ◽  
Sequent Calculi ◽  
Dialogue Games ◽  
Structured Information ◽  
Logical Connectives ◽  
Pluralistic Approach ◽  
Intuitionistic Linear Logic

Abstract Lorenzen has introduced his dialogical approach to the foundations of logic in the late 1950s to justify intuitionistic logic with respect to first principles about constructive reasoning. In the decades that have passed since, Lorenzen-style dialogue games turned out to be an inspiration for a more pluralistic approach to logical reasoning that covers a wide array of nonclassical logics. In particular, the close connection between (single-sided) sequent calculi and dialogue games is an invitation to look at substructural logics from a dialogical point of view. Focusing on intuitionistic linear logic, we illustrate that intuitions about resource-conscious reasoning are well served by translating sequent calculi into Lorenzen-style dialogue games. We suggest that these dialogue games may be understood as games of information extraction, where a sequent corresponds to the claim that a certain information package can be systematically extracted from a given bundle of such packages of logically structured information. As we will indicate, this opens the field for exploring new logical connectives arising by consideration of further forms of storing and structuring information.

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.

scholarly journals The Girard Translation Extended with Recursion

1995 ◽  
Vol 2 (13) ◽  
Author(s):  
Torben Braüner
Keyword(s):  
Intuitionistic Logic ◽  
Linear Logic ◽  
Full Version ◽  
Intuitionistic Linear Logic

<p>This paper extends Curry-Howard interpretations of Intuitionistic Logic (IL) and Intuitionistic Linear Logic (ILL) with rules for recursion. The resulting term languages, the rec-calculus and the linear rec-calculus respectively, are given sound<br />categorical interpretations. The embedding of proofs of IL into proofs of ILL given by the Girard Translation is extended with the rules for recursion, such that an embedding of terms of the rec-calculus into terms of the linear rec-calculus is induced via the extended Curry-Howard isomorphisms. This embedding is shown to be sound with respect to the categorical interpretations.</p><p><br />Full version of paper to appear in Proceedings of CSL '94, LNCS 933, 1995.

The undecidability of second order linear logic without exponentials

1996 ◽  
Vol 61 (2) ◽  
pp. 541-548 ◽  
Author(s):  
Yves Lafont
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Linear Logic ◽  
Classical Case ◽  
Second Order ◽  
Order Linear ◽  
Phase Semantics ◽  
Counter Machines ◽  
Intuitionistic Linear Logic

AbstractRecently, Lincoln, Scedrov and Shankar showed that the multiplicative fragment of second order intuitionistic linear logic is undecidable, using an encoding of second order intuitionistic logic. Their argument applies to the multiplicative-additive fragment, but it does not work in the classical case, because second order classical logic is decidable. Here we show that the multiplicative-additive fragment of second order classical linear logic is also undecidable, using an encoding of two-counter machines originally due to Kanovich. The faithfulness of this encoding is proved by means of the phase semantics.

scholarly journals On the correspondence between nested calculi and semantic systems for intuitionistic logics

2020 ◽  
Author(s):  
Tim Lyon
Keyword(s):  
Intuitionistic Logic ◽  
Structural Rules ◽  
First Order ◽  
Constant Domains ◽  
The Relationship ◽  
Intuitionistic Logics

Abstract This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic’s semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic’s semantics.

Sign in / Sign up

Export Citation Format

Share Document