Algebraic proof theory for LE-logics

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Greco, Giuseppe, Jipsen, Peter, Liang, Fei, Palmigiano, Alessandra, Tzimoulis, Apostolos
Format: Preprint
Published: 2018
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866913197939752960
author Greco, Giuseppe
Jipsen, Peter
Liang, Fei
Palmigiano, Alessandra
Tzimoulis, Apostolos
author_facet Greco, Giuseppe
Jipsen, Peter
Liang, Fei
Palmigiano, Alessandra
Tzimoulis, Apostolos
contents In this paper 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 generalise the residuated frames in [34] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LE-logics in full uniformity. We prove semantic cut elimination for the display calculi D.LE associated with the basic normal LE-logics and their axiomatic extensions with 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.
format Preprint
id arxiv_https___arxiv_org_abs_1808_04642
institution arXiv
publishDate 2018
record_format arxiv
spellingShingle Algebraic proof theory for LE-logics
Greco, Giuseppe
Jipsen, Peter
Liang, Fei
Palmigiano, Alessandra
Tzimoulis, Apostolos
Logic
In this paper 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 generalise the residuated frames in [34] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LE-logics in full uniformity. We prove semantic cut elimination for the display calculi D.LE associated with the basic normal LE-logics and their axiomatic extensions with 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.
title Algebraic proof theory for LE-logics
topic Logic
url https://arxiv.org/abs/1808.04642