Metatheories of deductive systems
A deductive system (Hilbert-style) is an algebraic closure system over the set of formulas of given propositional language. Similarly, a Gentzen system is an algebraic closure system over the set of all sequents, i.e., finite sequences of formulas, of this language. The main feature of this work is a technique that allows us to adapt the methods, previously developed in the area of algebraic logic for work with Hilbert-style deductive systems, to the case of Gentzen systems. Using the properties of the Tarski congruence, a generalization of the Leibnitz congruence, we develop an algebraic hierarchy for Gentzen systems that closely parallels the well-known algebraic hierarchy of deductive systems. This approach allows us to unify in a single framework several previously known results about algebraizable and equivalential Gentzen systems. We also obtain a characterization of weakly algebraizable Gentzen systems. The significance of Gentzen systems and related axiomatizations by Gentzen rules is due in large part to the fact that various metatheoretical properties of deductive systems can be formulated in their terms. It was observed that a number of important non-protoalgebraic deductive system that have a natural algebraic semantics also have a so-called fully adequate Gentzen system associated with them, the conjunction-disjunction fragment of the classical propositional logic being a paradigmatic example. In this work, a general criterion for the existence of a fully adequate Gentzen system for non-protoalgebraic deductive systems is obtained, and it is shown that many of the known partial results can be explained based on this general criterion. This includes such cases as the existence of fully adequate Gentzen systems for self-extensional logics with conjunction or implication, and the criterions for the existence of a fully adequate Gentzen system for protoalgebraic and weakly algebraizable logics. In another vein, it is shown that the existence of a multiterm deduction-detachment theorem in a deductive system is equivalent to the fact that, so called, axiomatic closure relations for the deductive system form a Gentzen system.