We elaborate a general theory of many-sorted algebraic structures as well as universal Horn theories both with and without equality on a uniform formal basis. We then study the issues of interpretability, equivalence, algebraic semantics, extensions, disjunctivity and deduction theorem within that general framework. We argue that not merely equivalence but equally interpretability properly retains extensions of Universal Horn theories. As a generic application, we develop a general theory of sequent calculi of various known kinds showing, among other things, existence of lattice-based algebraic semantics for any sequent calculi 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. Skryť popis