Strong negation in intuitionistic style sequent systems for residuated lattices

We study the sequent system mentioned in the author's work 18 as CyInFL with ‘intuitionistic’ sequents. We explore the connection between this system and symmetric constructive logic of Zaslavsky 40 and develop an algebraic semantics for both of them. In contrast to the previous work, we prove the strong completeness theorem for CyInFL with ‘intuitionistic’ sequents and all of its basic variants, including variants with contraction. We also show how the defined classes of structures are related to cyclic involutive FL‐algebras and Nelson FL_ew‐algebras. In particular, we prove the definitional equivalence of symmetric constructive FL_ewc‐algebras (algebraic models of symmetric constructive logic) and Nelson FL_ew‐algebras (algebras introduced by Spinks and Veroff 33 , 34 as the termwise equivalent definition of Nelson algebras). Because of the strong completeness theorem that covers all basic variants of CyInFL with ‘intuitionistic’ sequents, we rename this sequent system to symmetric constructive full Lambek calculus (). We verify the decidability of this system and its basic variants, as we did in the case of their distributive cousins 18 . As a consequence we obtain that the corresponding theories of (distributive and nondistributive) symmetric constructive FL‐algebras are decidable.