Algebraic Proof Theory for LE-logics

Giuseppe Greco; Peter Jipsen; Fei Liang; Alessandra Palmigiano; Apostolos Tzimoulis

doi:10.1145/3632526

Algebraic Proof Theory for LE-logics

Giuseppe Greco, Peter Jipsen, Fei Liang, Alessandra Palmigiano, Apostolos Tzimoulis

Ethics, Governance and Society

Research output: Contribution to Journal › Article › Academic › peer-review

23 Downloads (Pure)

Abstract

In this article, we extend the research programme in algebraic proof theory from axiomatic extensions of the full Lambek calculus to logics algebraically captured by certain varieties of normal lattice expansions (normal LE-logics). Specifically, we generalize the residuated frames in Reference [34] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LElogics in full uniformity. We prove semantic cut elimination for the display calculi D.LE associated with the basic normal LE-logics and their axiomatic extensionswith analytic inductive axioms. We also prove the finite model property (FMP) for each such calculus D.LE, as well as for its extensions with analytic structural rules satisfying certain additional properties.

Original language	English
Article number	6
Pages (from-to)	1-37
Number of pages	37
Journal	ACM Transactions on Computational Logic
Volume	25
Issue number	1
DOIs	https://doi.org/10.1145/3632526
Publication status	Published - Jan 2024

Bibliographical note

Funding Information:
This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 101007627. The research of the third author is supported by the Chinese Ministry of Education of Humanities and Social Science Project (23YJC72040003) and the Young Scholars Program of Shandong University (11090089964225). The research of the first and fourth author is partially funded by the NWO grant KIVI.2019.001. The research of the third and fifth authors is supported by the Key Project of Chinese Ministry of Education (22JJD720021).

Funding Information:
This project has received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 101007627. The research of the third author is supported by the Chinese Ministry of Education of Humanities and Social Science Project (23YJC72040003) and the Young Scholars Program of Shandong University (11090089964225). The research of the first and fourth author is partially funded by the NWO grant KIVI.2019.001. The research of the third and fifth authors is supported by the Key Project of Chinese Ministry of Education (22JJD720021).

Publisher Copyright:
© 2024 Copyright held by the owner/author(s).

Funding

This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 101007627. The research of the third author is supported by the Chinese Ministry of Education of Humanities and Social Science Project (23YJC72040003) and the Young Scholars Program of Shandong University (11090089964225). The research of the first and fourth author is partially funded by the NWO grant KIVI.2019.001. The research of the third and fifth authors is supported by the Key Project of Chinese Ministry of Education (22JJD720021). This project has received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 101007627. The research of the third author is supported by the Chinese Ministry of Education of Humanities and Social Science Project (23YJC72040003) and the Young Scholars Program of Shandong University (11090089964225). The research of the first and fourth author is partially funded by the NWO grant KIVI.2019.001. The research of the third and fifth authors is supported by the Key Project of Chinese Ministry of Education (22JJD720021).

Funders	Funder number
Horizon 2020 Framework Programme
Horizon 2020
Nederlandse Organisatie voor Wetenschappelijk Onderzoek	015.008.054, KIVI.2019.001
Ministry of Education of the People's Republic of China	22JJD720021
H2020 Marie Skłodowska-Curie Actions	101007627
Shandong University	11090089964225
Chinese Ministry of Education of Humanities and Social Science Project	23YJC72040003

Keywords

Algebraic proof theory polarity-based semantics
cut-elimination
display sequent calculi
finite model property
non-distributive logics
normal lattice expansions
substructural logics

Access to Document

10.1145/3632526

3632526_Algebraic Proof Theory for LE-logicsFinal published version, 500 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

@article{78ae9e78e6ac4468b5e92c32ab5e869e,

title = "Algebraic Proof Theory for LE-logics",

abstract = "In this article, we extend the research programme in algebraic proof theory from axiomatic extensions of the full Lambek calculus to logics algebraically captured by certain varieties of normal lattice expansions (normal LE-logics). Specifically, we generalize the residuated frames in Reference [34] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LElogics in full uniformity. We prove semantic cut elimination for the display calculi D.LE associated with the basic normal LE-logics and their axiomatic extensionswith analytic inductive axioms. We also prove the finite model property (FMP) for each such calculus D.LE, as well as for its extensions with analytic structural rules satisfying certain additional properties.",

keywords = "Algebraic proof theory polarity-based semantics, cut-elimination, display sequent calculi, finite model property, non-distributive logics, normal lattice expansions, substructural logics",

author = "Giuseppe Greco and Peter Jipsen and Fei Liang and Alessandra Palmigiano and Apostolos Tzimoulis",

note = "Funding Information: This project has received funding from the European Union{\textquoteright}s Horizon 2020 research and innovation programme under the Marie Sk{\l}odowska-Curie grant agreement No 101007627. The research of the third author is supported by the Chinese Ministry of Education of Humanities and Social Science Project (23YJC72040003) and the Young Scholars Program of Shandong University (11090089964225). The research of the first and fourth author is partially funded by the NWO grant KIVI.2019.001. The research of the third and fifth authors is supported by the Key Project of Chinese Ministry of Education (22JJD720021). Funding Information: This project has received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Sk{\l}odowska-Curie grant agreement No 101007627. The research of the third author is supported by the Chinese Ministry of Education of Humanities and Social Science Project (23YJC72040003) and the Young Scholars Program of Shandong University (11090089964225). The research of the first and fourth author is partially funded by the NWO grant KIVI.2019.001. The research of the third and fifth authors is supported by the Key Project of Chinese Ministry of Education (22JJD720021). Publisher Copyright: {\textcopyright} 2024 Copyright held by the owner/author(s).",

year = "2024",

month = jan,

doi = "10.1145/3632526",

language = "English",

volume = "25",

pages = "1--37",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

publisher = "Association for Computing Machinery (ACM)",

number = "1",

}

TY - JOUR

T1 - Algebraic Proof Theory for LE-logics

AU - Greco, Giuseppe

AU - Jipsen, Peter

AU - Liang, Fei

AU - Palmigiano, Alessandra

AU - Tzimoulis, Apostolos

N1 - Funding Information: This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 101007627. The research of the third author is supported by the Chinese Ministry of Education of Humanities and Social Science Project (23YJC72040003) and the Young Scholars Program of Shandong University (11090089964225). The research of the first and fourth author is partially funded by the NWO grant KIVI.2019.001. The research of the third and fifth authors is supported by the Key Project of Chinese Ministry of Education (22JJD720021). Funding Information: This project has received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 101007627. The research of the third author is supported by the Chinese Ministry of Education of Humanities and Social Science Project (23YJC72040003) and the Young Scholars Program of Shandong University (11090089964225). The research of the first and fourth author is partially funded by the NWO grant KIVI.2019.001. The research of the third and fifth authors is supported by the Key Project of Chinese Ministry of Education (22JJD720021). Publisher Copyright: © 2024 Copyright held by the owner/author(s).

PY - 2024/1

Y1 - 2024/1

N2 - In this article, we extend the research programme in algebraic proof theory from axiomatic extensions of the full Lambek calculus to logics algebraically captured by certain varieties of normal lattice expansions (normal LE-logics). Specifically, we generalize the residuated frames in Reference [34] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LElogics in full uniformity. We prove semantic cut elimination for the display calculi D.LE associated with the basic normal LE-logics and their axiomatic extensionswith analytic inductive axioms. We also prove the finite model property (FMP) for each such calculus D.LE, as well as for its extensions with analytic structural rules satisfying certain additional properties.

AB - In this article, we extend the research programme in algebraic proof theory from axiomatic extensions of the full Lambek calculus to logics algebraically captured by certain varieties of normal lattice expansions (normal LE-logics). Specifically, we generalize the residuated frames in Reference [34] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LElogics in full uniformity. We prove semantic cut elimination for the display calculi D.LE associated with the basic normal LE-logics and their axiomatic extensionswith analytic inductive axioms. We also prove the finite model property (FMP) for each such calculus D.LE, as well as for its extensions with analytic structural rules satisfying certain additional properties.

KW - Algebraic proof theory polarity-based semantics

KW - cut-elimination

KW - display sequent calculi

KW - finite model property

KW - non-distributive logics

KW - normal lattice expansions

KW - substructural logics

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

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

U2 - 10.1145/3632526

DO - 10.1145/3632526

M3 - Article

AN - SCOPUS:85183330736

SN - 1529-3785

VL - 25

SP - 1

EP - 37

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 1

M1 - 6

ER -

Algebraic Proof Theory for LE-logics

Abstract

Bibliographical note

Funding

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this