Algebraic semantics for Nelson’s logic S

Abstract

Besides the better-known Nelson’s Logic and Paraconsistent Nelson’s Logic, in “Negation and separation of concepts in constructive systems” (1959), David Nelson introduced a logic called S with the aim of analyzing the constructive content of provable negation statements in mathematics. Motivated by results from Kleene, in “On the Interpretation of Intuitionistic Number Theory” (1945), Nelson investigated a more symmetric recursive definition of truth, according to which a formula could be either primitively verified or refuted. The logic S was defined by means of a calculus lacking the contraction rule and having infinitely many schematic rules, and no semantics was provided. This system received little attention from researchers; it even remained unnoticed that on its original presentation it was inconsistent. Fortunately, the inconsistency was caused by typos and by a rule whose hypothesis and conclusion were swapped. We investigate a corrected version of the logic S, and focus on its propositional fragment, showing that it is algebraizable in the sense of Blok and Pigozzi (in fact, implicative) with respect to a certain class of involutive residuated lattices. We thus introduce the first (algebraic) semantics for S as well as a finite Hilbert-style calculus equivalent to Nelson’s presentation; we also compare S with the other two above-mentioned logics of the Nelson family. Our approach is along the same lines of (and partly relies on) previous algebraic work on Nelson’s logics due to M. Busaniche, R. Cignoli, S. Odintsov, M. Spinks and R. Veroff.