Constructive logic with strong negation is a substructural logic. I (Q931408)

This is the first half of two papers in which the authors show that the constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension of the substructural logic FLew, namely the full Lambek calculus with exchange and weakening. In this paper it is shown by an extensive use of the automated theorem prover PROVER9 that the variety of Nelson algebras and a certain variety of FLew-algebras are term-equivalent, which answers to a long-standing question of Nelson's asking whether the Nelson algebras form a variety of certain residuated lattices. The result establishes the above-mentioned definitional equivalence of the two deductive systems in the sequel to conclude that the logic N is a substructural logic over FLew.