Deduction Theorem and Peirce Law in General Algebraic Logic

In this book we study the issues of Deduction Theorem and Peirce Law within the context of finitary universal Horn theories and equivalence between them. As basic general results, we first obtain a model-theoretic chracterization of such theories having Deduction Theorem with Peirce Law and then prove that equivalence between them preserves both Deduction Theorem and Peirce law. Next, we argue that our Deduction Theorem schema for enlargable multiple-conclusion sequent calculi with structural rules found earlier respects Peirce Law. As a consequence, we provide a natural and quite useful semantics of such calculi. Finally, we explore the issues involved within the context of the Weak Contraposition extensions of so-called contraposable propositional calculi of the mentioned kind. After all, we successfully apply our generic elaboration to both certain sentential logics and several varieties of algebras, providing constructive and quite transparent proofs of Deduction Theorem withPeirce Law for the formers as well as implicativity (or, at least, restricted equational definability of principal congruences) for the latters.