Algebraic semantics for Nelson’s logic S

Abstract

Besides the better-known Nelson logic (𝒩3) and paraconsistent Nelson logic (𝒩4), in Negation and separation of concepts in constructive systems (1959) David Nelson introduced a logic that he called 𝒮, with motivations of arithmetic and constructibility. The logic was defined by means of a calculus (crucially lacking the contraction rule) having infinitely many rule schemata, and no semantics was provided for it. We look in the present dissertation at the propositional fragment of 𝒮, showing that it is algebraizable (in fact, implicative) in the sense of Blok and Pigozzi with respect to a class of involutive residuated lattices. We thus provide the first known algebraic semantics for 𝒮(we call them of 𝒮-algebras) as well as a finite Hilbert-style calculus equivalent to Nelson’s presentation. We provide an algorithm to make 𝒮-algebras from 𝒮-algebras or implicative lattices and we prove some results about the class of algebras which we have introduced. We also compare 𝒮 with other logics of the Nelson family, that is, 𝒩3 and 𝒩4.