A modal view of linear logic

1994 ◽  
Vol 59 (3) ◽  
pp. 888-899 ◽  
Author(s):  
Simone Martini ◽  
Andrea Masini
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Decision Problem ◽  
Sequent Calculus ◽  
Linear Logic

AbstractWe present a sequent calculus for the modal logic S4, and building on some relevant features of this system (the absence of contraction rules and the confinement of weakenings into axioms and modal rules) we show how S4 can easily be translated into full prepositional linear logic, extending the Grishin-Ono translation of classical logic into linear logic. The translation introduces linear modalities (exponentials) only in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations.

scholarly journals Deep Proof Search in MELL

10.29007/p1fd ◽  
2018 ◽  
Author(s):  
Ozan Kahramanogullari
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Proof Search ◽  
Proof Construction ◽  
Deep Inference ◽  
Speed Up

The deep inference presentation of multiplicative exponential linear logic (MELL) benefits from a rich combinatoric analysis with many more proofs in comparison to its sequent calculus presentation. In the deep inference setting, all the sequent calculus proofs are preserved. Moreover, many other proofs become available, and some of these proofs are much shorter. However, proof search in deep inference is subject to a greater nondeterminism, and this nondeterminism constitutes a bottleneck for applications. To this end, we address the problem of reducing nondeterminism in MELL by refining and extending our technique that has been previously applied to multiplicative linear logic and classical logic. We show that, besides the nondeterminism in commutative contexts, the nondeterminism in exponential contexts can be reduced in a proof theoretically clean manner. The method conserves the exponential speed-up in proof construction due to deep inference, exemplified by Statman tautologies. We validate the improvement in accessing the shorter proofs by experiments with our implementations.

On categorical models of classical logic and the Geometry of Interaction

2007 ◽  
Vol 17 (5) ◽  
pp. 957-1027 ◽  
Author(s):  
CARSTEN FÜHRMANN ◽  
DAVID PYM
Keyword(s):  
Classical Logic ◽  
Disjoint Union ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Structural Theory ◽  
Cut Elimination ◽  
Categorical Models ◽  
Boolean Lattices ◽  
Deep Exploration ◽  
Straightforward Proof

It is well known that weakening and contraction cause naive categorical models of the classical sequent calculus to collapse to Boolean lattices. In previous work, summarised briefly herein, we have provided a class of models calledclassical categoriesthat is sound and complete and avoids this collapse by interpreting cut reduction by a poset enrichment. Examples of classical categories include boolean lattices and the category of sets and relations, where both conjunction and disjunction are modelled by the set-theoretic product. In this article, which is self-contained, we present an improved axiomatisation of classical categories, together with a deep exploration of their structural theory. Observing that the collapse already happens in the absence of negation, we start with negation-free models calledDummett categories. Examples of these include, besides the classical categories mentioned above, the category of sets and relations, where both conjunction and disjunction are modelled by the disjoint union. We prove that Dummett categories are MIX, and that the partial order can be derived from hom-semilattices, which have a straightforward proof-theoretic definition. Moreover, we show that the Geometry-of-Interaction construction can be extended from multiplicative linear logic to classical logic by applying it to obtain a classical category from a Dummett category.Along the way, we gain detailed insights into the changes that proofs undergo during cut elimination in the presence of weakening and contraction.

A new deconstructive logic: linear logic

1997 ◽  
Vol 62 (3) ◽  
pp. 755-807 ◽  
Author(s):  
Vincent Danos ◽  
Jean-Baptiste Joinet ◽  
Harold Schellinx
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Predicate Logic ◽  
Linear Logic ◽  
Second Order ◽  
Main Concern ◽  
Simple Pattern ◽  
Strong Normalization ◽  
Viable Systems ◽  
Proof Nets

AbstractThe main concern of this paper is the design of a noetherian and confluent normalization for LK2 (that is, classical second order predicate logic presented as a sequent calculus).The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD ([10, 12, 32, 36]), delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of ‘programming-with-proofs’ ([26, 27]) to classical logic; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic (for non-additive proof nets, to be precise) using appropriate embeddings (so-called decorations); it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making.A comparison of our method to that of embedding LK into LJ (intuitionistic sequent calculus) brings to the fore the latter's defects for these ‘deconstructive purposes’.

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

scholarly journals The geometry of non-distributive logics

2005 ◽  
Vol 70 (4) ◽  
pp. 1108-1126 ◽  
Author(s):  
Greg Restall ◽  
Francesco Paoli
Keyword(s):  
Classical Logic ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Cut Elimination ◽  
Deduction System ◽  
Inductive Definition ◽  
Theoretical Criterion ◽  
Natural Deduction System

AbstractIn this paper we introduce a new natural deduction system for the logic of lattices, and a number of extensions of lattice logic with different negation connectives. We provide the class of natural deduction proofs with both a standard inductive definition and a global graph-theoretical criterion for correctness, and we show how normalisation in this system corresponds to cut elimination in the sequent calculus for lattice logic. This natural deduction system is inspired both by Shoesmith and Smiley's multiple conclusion systems for classical logic and Girard's proofnets for linear logic.

scholarly journals On Polymorphic Sessions and Functions

2021 ◽  
Vol 43 (2) ◽  
pp. 1-55
Author(s):  
Bernardo Toninho ◽  
Nobuko Yoshida
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Linear Formulation ◽  
Session Types ◽  
Logical Foundation ◽  
Π Calculus ◽  
Soundness And Completeness ◽  
System F ◽  
Algebraic Representations

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Multiplicative conjunction and an algebraic meaning of contraction and weakening

1998 ◽  
Vol 63 (3) ◽  
pp. 831-859 ◽  
Author(s):  
A. Avron
Keyword(s):  
Classical Logic ◽  
Linear Logic ◽  
Substructural Logics ◽  
Interesting Property ◽  
Relevance Logic ◽  
Proper Subset ◽  
Algebraic Structures ◽  
Elimination Rule ◽  
First Case ◽  
Soundness And Completeness

AbstractWe show that the elimination rule for the multiplicative (or intensional) conjunction Λ is admissible in many important multiplicative substructural logics. These include LLm (the multiplicative fragment of Linear Logic) and RMIm (the system obtained from LLm by adding the contraction axiom and its converse, the mingle axiom.) An exception is Rm (the intensional fragment of the relevance logic R, which is LLm together with the contraction axiom). Let SLLm and SRm be, respectively, the systems which are obtained from LLm and Rm by adding this rule as a new rule of inference. The set of theorems of SRm is a proper extension of that of Rm, but a proper subset of the set of theorems of RMIm. Hence it still has the variable-sharing property. SRm has also the interesting property that classical logic has a strong translation into it. We next introduce general algebraic structures, called strong multiplicative structures, and prove strong soundness and completeness of SLLm relative to them. We show that in the framework of these structures, the addition of the weakening axiom to SLLm corresponds to the condition that there will be exactly one designated element, while the addition of the contraction axiom corresponds to the condition that there will be exactly one nondesignated element (in the first case we get the system BCKm, in the second - the system SRm). Various other systems in which multiplicative conjunction functions as a true conjunction are studied, together with their algebraic counterparts.

Sign in / Sign up

Export Citation Format

Share Document