Semi De Morgan logic properly displayed
Giuseppe Greco, Fei Liang, M. Andrew Moshier, Alessandra, Palmigiano
TL;DR
This paper develops multi-type display calculi for semi De Morgan logic, ensuring soundness, completeness, and desirable proof-theoretic properties through algebraic analysis and a systematic methodology.
Contribution
It introduces a family of axiomatic extensions with proper display calculi based on algebraic and multi-type methodology, advancing proof-theoretic understanding of semi De Morgan logic.
Findings
Calculi are sound and complete
Calculi enjoy cut elimination and subformula property
Framework applies to various subvarieties of semi De Morgan algebras
Abstract
In the present paper, we endow a family of axiomatic extensions of semi De Morgan logic with proper multi-type display calculi which are sound, complete, conservative, and enjoy cut elimination and subformula property. Our proposal builds on an algebraic analysis of semi De Morgan algebras and its subvarieties and applies the guidelines of the multi-type methodology in the design of display calculi.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.