A SEQUENT CALCULUS FOR CONSTRUCTIVE LOGIC WITH STRONG NEGATION AS A SUBSTRUCTURAL LOGIC
George Metcalfe · BORIS (University Library Bern) · 2009
Gentzen systems are introduced for Spinks and Veroff’s substructural logic cor-responding to constructive logic with strong negation, and some logics in its vicinity. It has been shown by Spinks and Veroff in [9], [10] that the variety of Nelson algebras, the algebras of constructive logic with strong negation N, is term-equivalent to a certain variety of bounded commutative residuated lattices called Nelson residuated lattices. An algebraic proof of this result, simplifying some aspects of the presentation, has been given by Busaniche and Cignoli in [4]. In this short note a sequent calculus is defined for Nel-son residuated lattices by extending a sequent calculus (essentially CFLew or AMALL, see e.g. [6]) for involutive bounded integral commutative resid-uated lattices with a single structural rule. Using the translation of [9], [10] this is also a calculus for the logic N, providing an alternative to systems in the literature that make use either of decomposition rules acting on more