A many-sorted natural deduction

The goal of this paper is to motivate and define yet another sorted logic, called SND. All the previous sorted logics that can be found in the Artificial Intelligence literature have been designed to be used in (completely) automated deduction. SND has been designed to be used in interactive theorem proving. Because of this shift of focus, SND has been designed to satisfy three innovative design requirements: it is defined on top of a natural deduction calculus, and in a way to be a definitional extension of such calculus; and it is implemented on top of its implementation. In turn, because of this fact, SND has various innovative technical properties; among them: it allows us to deal with free variables, it has no notion of well-sortedness and of well-sortedness being a prerequisite of well-formedness, its implementation is such that, in the default mode, the system behaves exactly as with the original unsorted calculus.