A new deconstructive logic: linear logic

Vincent Danos, Jean-Baptiste Joinet, Harold Schellinx

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

The main concern of this paper is the design of a noetherian and confluent normalization for LK 2 (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’.
Original languageEnglish
Pages (from-to)755-807
Number of pages53
JournalJournal of Symbolic Logic
Publication statusPublished - Sept 1997


Dive into the research topics of 'A new deconstructive logic: linear logic'. Together they form a unique fingerprint.

Cite this