Constructive logic with strong negation is a substructural logic. II (Q1005940)

This is the latter half of two papers in which the authors show that the constructive logic with strong negation is definitionally equivalent to a certain axiomatic extension of the substructural logic FLew, namely, the full Lambek calculus with exchange and weakening. In the first half [\textit{M. Spinks} and \textit{R. Veroff}, Stud. Log. 88, No. 3, 325--348 (2008; Zbl 1145.03013)], it was shown that the variety of Nelson algebras and a certain variety of FLew-algebras are term equivalent, which is lifted in this paper to the above-mentioned equivalence to get the result stated in the title. As a matter of fact, the equivalence is obtained by an application of a theorem to give a sufficient condition for the definitional equivalence of regularly algebraisable logics in a general setting. For the theorem, therefore, the authors survey briefly some fundamental notions in abstract algebraic logics, such as deductive system, definitional equivalence for deductive systems, regularly algebraisable logics, and so on, where a refinement of the definition of substructural logics is also proposed.