Extending the Lambek calculus with classical negation (Q2118967)

Let \textbf{NL} be the non-associative Lambek calculus and S (our symbol) be the ternary relational semantics for \textbf{NL} as defined in [\textit{K. Došen}, Z. Math. Logik Grundlagen Math. 38, No. 2, 179--187 (1992; Zbl 0793.03025)]. Moreover, let negation be classically interpreted when ``a world satisfies the negation of a formula if and only if it does not satisfy the formula itself'' (p. 295). The question the author poses is how \textbf{NL} has to be extended in order to obtain a sound and complete system w.r.t. S with the classical interpretation of negation just defined. The author recalls some known items in the literature and claims that none of them answers the question he has posed. Then he defines the calculus \textbf{NLN}\(^{+}\), which is proved sound and complete w.r.t. S with negation interpreted classically as defined above. As the author notes (p. 296), ``the calculus \textbf{NLN}\(^{+}\) is tightly related to \textbf{PNL} -- the Lambek calculus extended with classical propositional logic'' defined by \textit{M. Kaminski} and \textit{N. Francez} [Stud. Log. 102, No. 3, 479--497 (2014; Zbl 1322.03018)]. So some results of the quoted work are used throughout the paper. The author remarks (Remark 31) that \textbf{NLN}\(^{+}\) is strongly decidable.