Nelson's Logic S

TL;DR

This paper introduces the propositional fragment of Nelson's logic S, providing the first algebraic semantics and a Hilbert calculus, clarifying its relation to Nelson's N3 and N4 logics.

Contribution

It is the first to algebraize the propositional fragment of Nelson's logic S and establish its algebraic semantics, connecting it to existing Nelson logics.

Findings

Propositional S is algebraizable with respect to three-potent involutive residuated lattices.

A finite Hilbert calculus equivalent to Nelson's original presentation is provided.

The relation between S and Nelson's N3 and N4 logics is clarified.

Abstract

Besides the better-known Nelson logic (N3) and paraconsistent logic (N4), in 1959 David Nelson introduced, with motivations of realizability and constructibility, a logic called S. The logic S was originally presented by means of a calculus (crucially lacking the contraction rule) with infinitely many rule schemata and no semantics (other than the intended interpretation into Arithmetic.) We look here at the propositional fragment of S, showing that it is algebraizable (in fact, implicative), in the sense of Blok and Pigozzi, with respect to a variety of three-potent involutive residuated lattices. We thus introduce the first known algebraic semantics for S as well as a finite Hilbert-style calculus equivalent to Nelson's presentation; this also allows us to clarify the relation between S and the other two Nelson logics N3 and N4.