Multiple conclusion linear logic: Cut elimination and more

Harley D Eades, Valeria de Paiva

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

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. It was shown that their formalization of FILL did not enjoy cut-elimination by Bierman, but Bellin proposed a change to the definition of FILL in the hope to regain cut-elimination. In this note we adopt Bellin’s proposed change and give a direct proof of cut-elimination. Then we show that a categorical model of FILL in the basic dialectica category is also a LNL model of Benton and a full tensor model of Melli`es’ and Tabareau’s tensorial logic. Lastly, we give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor.

Original languageEnglish (US)
Title of host publicationLogical Foundations of Computer Science - International Symposium, LFCS 2016, Proceedings
EditorsAnil Nerode, Sergei Artemov
PublisherSpringer Verlag
Pages90-105
Number of pages16
ISBN (Print)9783319276823
DOIs
StatePublished - Jan 1 2016
EventInternational Symposium on Logical Foundations of Computer Science, LFCS 2016 - Deerfield Beach, United States
Duration: Jan 4 2016Jan 7 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9537
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherInternational Symposium on Logical Foundations of Computer Science, LFCS 2016
CountryUnited States
CityDeerfield Beach
Period1/4/161/7/16

Fingerprint

Cut-elimination
Linear Logic
Intuitionistic Logic
Tensors
Regain
Tensor
Formalization
Categorical
Model
Logic

Keywords

  • Categorical model
  • Classical linear logic
  • Cut-elimination
  • Dialectica category
  • Full intuitionistic linear logic
  • Linear/non-linear models
  • Par
  • Proof theory
  • Tensorial logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Eades, H. D., & de Paiva, V. (2016). Multiple conclusion linear logic: Cut elimination and more. In A. Nerode, & S. Artemov (Eds.), Logical Foundations of Computer Science - International Symposium, LFCS 2016, Proceedings (pp. 90-105). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9537). Springer Verlag. https://doi.org/10.1007/978-3-319-27683-0_7

Multiple conclusion linear logic : Cut elimination and more. / Eades, Harley D; de Paiva, Valeria.

Logical Foundations of Computer Science - International Symposium, LFCS 2016, Proceedings. ed. / Anil Nerode; Sergei Artemov. Springer Verlag, 2016. p. 90-105 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9537).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Eades, HD & de Paiva, V 2016, Multiple conclusion linear logic: Cut elimination and more. in A Nerode & S Artemov (eds), Logical Foundations of Computer Science - International Symposium, LFCS 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9537, Springer Verlag, pp. 90-105, International Symposium on Logical Foundations of Computer Science, LFCS 2016, Deerfield Beach, United States, 1/4/16. https://doi.org/10.1007/978-3-319-27683-0_7
Eades HD, de Paiva V. Multiple conclusion linear logic: Cut elimination and more. In Nerode A, Artemov S, editors, Logical Foundations of Computer Science - International Symposium, LFCS 2016, Proceedings. Springer Verlag. 2016. p. 90-105. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-27683-0_7
Eades, Harley D ; de Paiva, Valeria. / Multiple conclusion linear logic : Cut elimination and more. Logical Foundations of Computer Science - International Symposium, LFCS 2016, Proceedings. editor / Anil Nerode ; Sergei Artemov. Springer Verlag, 2016. pp. 90-105 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{5a7d3baf24884eb19953798bee8137ed,
title = "Multiple conclusion linear logic: Cut elimination and more",
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. It was shown that their formalization of FILL did not enjoy cut-elimination by Bierman, but Bellin proposed a change to the definition of FILL in the hope to regain cut-elimination. In this note we adopt Bellin’s proposed change and give a direct proof of cut-elimination. Then we show that a categorical model of FILL in the basic dialectica category is also a LNL model of Benton and a full tensor model of Melli`es’ and Tabareau’s tensorial logic. Lastly, we give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor.",
keywords = "Categorical model, Classical linear logic, Cut-elimination, Dialectica category, Full intuitionistic linear logic, Linear/non-linear models, Par, Proof theory, Tensorial logic",
author = "Eades, {Harley D} and {de Paiva}, Valeria",
year = "2016",
month = "1",
day = "1",
doi = "10.1007/978-3-319-27683-0_7",
language = "English (US)",
isbn = "9783319276823",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "90--105",
editor = "Anil Nerode and Sergei Artemov",
booktitle = "Logical Foundations of Computer Science - International Symposium, LFCS 2016, Proceedings",

}

TY - GEN

T1 - Multiple conclusion linear logic

T2 - Cut elimination and more

AU - Eades, Harley D

AU - de Paiva, Valeria

PY - 2016/1/1

Y1 - 2016/1/1

N2 - 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. It was shown that their formalization of FILL did not enjoy cut-elimination by Bierman, but Bellin proposed a change to the definition of FILL in the hope to regain cut-elimination. In this note we adopt Bellin’s proposed change and give a direct proof of cut-elimination. Then we show that a categorical model of FILL in the basic dialectica category is also a LNL model of Benton and a full tensor model of Melli`es’ and Tabareau’s tensorial logic. Lastly, we give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor.

AB - 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. It was shown that their formalization of FILL did not enjoy cut-elimination by Bierman, but Bellin proposed a change to the definition of FILL in the hope to regain cut-elimination. In this note we adopt Bellin’s proposed change and give a direct proof of cut-elimination. Then we show that a categorical model of FILL in the basic dialectica category is also a LNL model of Benton and a full tensor model of Melli`es’ and Tabareau’s tensorial logic. Lastly, we give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor.

KW - Categorical model

KW - Classical linear logic

KW - Cut-elimination

KW - Dialectica category

KW - Full intuitionistic linear logic

KW - Linear/non-linear models

KW - Par

KW - Proof theory

KW - Tensorial logic

UR - http://www.scopus.com/inward/record.url?scp=84952815116&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84952815116&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-27683-0_7

DO - 10.1007/978-3-319-27683-0_7

M3 - Conference contribution

AN - SCOPUS:84952815116

SN - 9783319276823

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 90

EP - 105

BT - Logical Foundations of Computer Science - International Symposium, LFCS 2016, Proceedings

A2 - Nerode, Anil

A2 - Artemov, Sergei

PB - Springer Verlag

ER -