Paradigms for Many-sorted Non-classical Substitutions

We present three paradigms for non-classical substitution in a many-sorted context. Such an exposition has previously been demonstrated in the unsorted case but its extension is far from trivial. The first paradigm, classical many-sorted substitution taking variables to terms, is traditionally presented in a rather informal and "verbal" manner but we find that a strict categorical formulation is necessary to pave the way for non-classical extensions. The second paradigm provides substitution of variables for many-valued sets of terms and relies heavily on functors and monads over the category of indexed sets. Finally, in the third paradigm, we establish full non-classical substitution of many-valued sets of variables by many-valued sets of terms. The third paradigm has the category of many-valued indexed sets as its underlying category. These paradigms ensures transparency of the underlying categories and also makes a clear distinction between set-theoretic operation in the meta language and operations on sets and many-valued sets as found within respective underlying categories.