Non-commutative logic II: sequent calculus and phase semantics

2000 ◽  
Vol 10 (2) ◽  
pp. 277-312 ◽  
Author(s):  
PAUL RUET
Keyword(s):  
Special Class ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Partial Orders ◽  
Cut Elimination ◽  
Phase Semantics ◽  
Entropy Relation

Non-commutative logic, which is a unification of commutative linear logic and cyclic linear logic, is extended to all linear connectives: additives, exponentials and constants. We give two equivalent versions of the sequent calculus (directly with the structure of order varieties, and with their presentations as partial orders), phase semantics and a cut-elimination theorem. This involves, in particular, the study of the entropy relation between partial orders, and the introduction of a special class of order varieties: the series–parallel order varieties.

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

Basic logic: reflection, symmetry, visibility

2000 ◽  
Vol 65 (3) ◽  
pp. 979-1013 ◽  
Author(s):  
Giovanni Sambin ◽  
Giulia Battilotti ◽  
Claudia Faggian
Keyword(s):  
Sequent Calculus ◽  
Linear Logic ◽  
Logical Constant ◽  
Cut Elimination ◽  
Inference Rules ◽  
Reflection Symmetry ◽  
Basic Logic ◽  
Strict Control ◽  
Geometric Symmetry

AbstractWe introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic. quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility.A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection.To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube.

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

Multiple conclusion linear logic: cut elimination and more

2020 ◽  
Vol 30 (1) ◽  
pp. 157-174 ◽  
Author(s):  
Harley Eades III ◽  
Valeria de Paiva
Keyword(s):  
Sequent Calculus ◽  
Linear Logic ◽  
Direct Proof ◽  
Cut Elimination ◽  
Tensor Model ◽  
Double Negation ◽  
Proof Nets ◽  
Small Change ◽  
Definition Of ◽  
Intuitionistic Linear Logic

Abstract Full intuitionistic linear logic (FILL) was first introduced by Hyland and de Paiva, and went against current beliefs that it was not possible to incorporate all of the linear connectives, e.g. tensor, par and implication, into an intuitionistic linear logic. Bierman showed that their formalization of FILL did not enjoy cut elimination as such, but Bellin proposed a small change to the definition of FILL regaining cut elimination and using proof nets. In this note we adopt Bellin’s proposed change and give a direct proof of cut elimination for the sequent calculus. Then we show that a categorical model of FILL in the basic dialectica category is also a linear/non-linear model of Benton and a full tensor model of Melliès’ and Tabareau’s tensorial logic. We give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor. Lastly, we introduce a new library to be used in the proof assistant Agda for proving properties of dialectica categories.

Resource sharing linear logic

2020 ◽  
Vol 30 (1) ◽  
pp. 295-319
Author(s):  
Hidenori Kurokawa ◽  
Hirohiko Kushida
Keyword(s):  
Computational Model ◽  
Resource Sharing ◽  
Linear Logic ◽  
Cut Elimination ◽  
Parallel Version ◽  
Phase Semantics

Abstract In this paper, we introduce a new logic that we call ‘resource sharing linear logic (RSLL)’. In linear logic (LL), formulas without modality express some resource-conscious situation (a formula can be used only once); formulas with modality express a situation with unlimited resources. We introduce the logic RSLL in which we have a strengthened modality (S5-modality) that can be understood as expressing not only unlimited resources but also resources shared by different agents. Observing that merely strengthening the modality allows weakening axiom to be derivable in a Hilbert-style formulation of this logic, we reformulate RSLL as a logic similar to affine logic by a hypersequent calculus that has weakening as a primitive rule. We prove the completeness of the hypersequent calculus with respect to phase semantics and the cut-elimination theorem for the system by a syntactical method. We also prove the decidability of RSLL via a computational interpretation of RSLL, which is a parallel version of Kopylov’s computational model for LL. We then introduce an explicit counterpart of RSLL in the style of Artemov’s justication logic (JRSLL). We prove a realization theorem for RSLL via its explicit counterpart.

A focused linear logical framework and its application to metatheory of object logics

2021 ◽  
pp. 1-29
Author(s):  
Amy Felty ◽  
Carlos Olarte ◽  
Bruno Xavier
Keyword(s):  
Programming Languages ◽  
Sequent Calculus ◽  
Necessary Conditions ◽  
Linear Logic ◽  
Cut Elimination ◽  
Logical Framework ◽  
Minimal Logic ◽  
First Order ◽  
Fundamental Properties ◽  
Logical Frameworks

Abstract Linear logic (LL) has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks, and models for concurrency. LL’s cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. This paper formalizes the proof of cut-elimination for focused LL. For that, we propose a set of five cut-rules that allows us to prove cut-elimination directly on the focused system. We also encode the inference rules of other logics as LL theories and formalize the necessary conditions for those logics to have cut-elimination. We then obtain, for free, cut-elimination for first-order classical, intuitionistic, and variants of LL. We also use the LL metatheory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic. Hence, we propose a framework that can be used to formalize fundamental properties of logical systems specified as LL theories.

Linear logic propositions as session types

2014 ◽  
Vol 26 (3) ◽  
pp. 367-423 ◽  
Author(s):  
LUÍS CAIRES ◽  
FRANK PFENNING ◽  
BERNARDO TONINHO
Keyword(s):  
Sequent Calculus ◽  
Linear Logic ◽  
Type System ◽  
Type Systems ◽  
Cut Elimination ◽  
Session Types ◽  
Deadlock Freedom ◽  
Session Type ◽  
Π Calculus ◽  
Intuitionistic Linear Logic

Throughout the years, several typing disciplines for the π-calculus have been proposed. Arguably, the most widespread of these typing disciplines consists of session types. Session types describe the input/output behaviour of processes and traditionally provide strong guarantees about this behaviour (i.e. deadlock-freedom and fidelity). While these systems exploit a fundamental notion of linearity, the precise connection between linear logic and session types has not been well understood.This paper proposes a type system for the π-calculus that corresponds to a standard sequent calculus presentation of intuitionistic linear logic, interpreting linear propositions as session types and thus providing a purely logical account of all key features and properties of session types. We show the deep correspondence between linear logic and session types by exhibiting a tight operational correspondence between cut-elimination steps and process reductions. We also discuss an alternative presentation of linear session types based on classical linear logic, and compare our development with other more traditional session type systems.

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.

Sign in / Sign up

Export Citation Format

Share Document