Many-Sorted General Algebraic Logic Subprevarieties Versus Extensions

We elaborate a general theory of many-sorted algebraic structures as well as infinitary universal Horn theories both with and without equality on a uniform formal basis.We then study the issues of interpretability, equivalence, algebraic semantics, admissible rules, extensions, their relative axiomatizations, disjunctivity and deduction theorem within that general framework. We argue that not merely equivalence but equally interpretability properly retains extensions of Universal Horn theories and their relative axiomatizations as well as the admissibility of rules. As a generic application, we develop a general theory of sequent calculi of various known kinds showing, among other things, existence of many-sorted lattice-based algebraic semantics for any sequent calculus with basic structural rules (Enlargement, Permutation and Contraction).In addition, we apply our general elaboration to study many-valued paraconsistent logics (in particular, their maximal paraconsistency). Finally, we exemplify our general study by investigating certain propositional calculi of both Hilbert and Gentzen types.