Constructive Logic with Strong Negation as a Substructural Logic

Gentzen systems are introduced for Spinks and Veroff's substructural logic corresponding 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 Nelson residuated lattices by extending a sequent calculus (essentially CFLew or AMALL, see e.g. [6]) for involutive bounded integral commutative residuated 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...

• Type: Journal
• Year: 2010
• Where: LOGCOM
• Authors: Manuela Busaniche, Roberto Cignoli
• Keywords: Commutative Residuated Lattice, LOGCOM 2010, Logic, Programming Languages, Strong Negation