arXiv · 1612.05930
Lattice Logic Properly Displayed
Abstract
We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and sub-formula property. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest Belnap-style proof of cut-elimination. Our proposal builds on an algebraic and order-theoretic analysis of the semantic environment of lattice logic, and applies the guidelines of the multi-type methodology in the design of display calculi.
Explore related subjects
Keep this discovery
Giuseppe Greco, Alessandra Palmigiano. 2016-12-18. Lattice Logic Properly Displayed. https://arxiv.org/abs/1612.05930
Cite the original work for its findings. Save a collection to share your selection of sources.