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.

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.

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.

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 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>

Sign in / Sign up

Export Citation Format

Share Document