Algebraic proof theory for LE-logics
arXiv:1808.04642 · doi:10.1145/3632526
Abstract
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.
final version
References in corpus (8)
- Multi-type Display Calculus for Dynamic Epistemic Logic
- Multi-type display calculus for Propositional Dynamic Logic
- Toward an Epistemic-Logical Theory of Categorization
- Rough concepts
- Toward a Dempster-Shafer theory of concepts
- Constructive Canonicity of Inductive Inequalities
- The Logic of Resources and Capabilities
- Modelling socio-political competition