We introduce a proper multi-type display calculus for semi De Morgan logic which is sound, complete, conservative, and enjoys cut-elimination and subformula property. Our proposal builds on an algebraic analysis of semi De Morgan algebras and applies the guidelines of the multi-type methodology in the design of display calculi.
展开▼
