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

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

Download Full-text

On the unification of classical, intuitionistic and affine logics

Mathematical Structures in Computer Science ◽

10.1017/s0960129518000403 ◽

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.

Download Full-text

Non-commutative logic II: sequent calculus and phase semantics

Mathematical Structures in Computer Science ◽

10.1017/s0960129599003084 ◽

2000 ◽

Vol 10 (2) ◽

pp. 277-312 ◽

Cited By ~ 12

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.

Download Full-text

Pretopologies and completeness proofs

Journal of Symbolic Logic ◽

10.2307/2275761 ◽

1995 ◽

Vol 60 (3) ◽

pp. 861-878 ◽

Cited By ~ 23

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.

Download Full-text

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

Journal of Symbolic Logic ◽

10.2178/jsl/1190150036 ◽

2002 ◽

Vol 67 (1) ◽

pp. 162-196 ◽

Cited By ~ 1

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.

Download Full-text

Admissibility of structural rules for contraction-free systems of intuitionistic logic

Journal of Symbolic Logic ◽

10.2307/2695061 ◽

2000 ◽

Vol 65 (4) ◽

pp. 1499-1518 ◽

Cited By ~ 10

Author(s):

Roy Dyckhoff ◽

Sara Negri

Keyword(s):

Intuitionistic Logic ◽

Propositional Logic ◽

Sequent Calculus ◽

Direct Proof ◽

Intuitionistic Propositional Logic ◽

Structural Rules

AbstractWe give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs, i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.

Download Full-text

An approach to automated reparation of failed proof attempts in propositional linear logic sequent calculus

Proceedings of the Fifth Balkan Conference in Informatics on - BCI '12 ◽

10.1145/2371316.2371329 ◽

2012 ◽

Author(s):

Tatjana Lutovac

Keyword(s):

Sequent Calculus ◽

Linear Logic

Download Full-text

Deduction in Non-Fregean Propositional Logic SCI

Axioms ◽

10.3390/axioms8040115 ◽

2019 ◽

Vol 8 (4) ◽

pp. 115 ◽

Cited By ~ 1

Author(s):

Joanna Golińska-Pilarek ◽

Magdalena Welle

Keyword(s):

Propositional Logic ◽

Sequent Calculus ◽

Classical Propositional Logic ◽

Tableau System ◽

Soundness And Completeness

We study deduction systems for the weakest, extensional and two-valued non-Fregean propositional logic SCI . The language of SCI is obtained by expanding the language of classical propositional logic with a new binary connective ≡ that expresses the identity of two statements; that is, it connects two statements and forms a new one, which is true whenever the semantic correlates of the arguments are the same. On the formal side, SCI is an extension of classical propositional logic with axioms characterizing the identity connective, postulating that identity must be an equivalence and obey an extensionality principle. First, we present and discuss two types of systems for SCI known from the literature, namely sequent calculus and a dual tableau-like system. Then, we present a new dual tableau system for SCI and prove its soundness and completeness. Finally, we discuss and compare the systems presented in the paper.

Download Full-text

On Polymorphic Sessions and Functions

ACM Transactions on Programming Languages and Systems ◽

10.1145/3457884 ◽

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.

Download Full-text