Leibniz operator

In abstract algebraic logic, a branch of mathematical logic, the Leibniz operator is a tool used to classify deductive systems, which have a precise technical definition, and capture a large number of logics. The Leibniz operator was introduced by Wim Blok and Don Pigozzi, two of the founders of the field, as a means to abstract the well-known Lindenbaum–Tarski process, that leads to the association of Boolean algebras to classical propositional calculus, and make it applicable to as wide a variety of sentential logics as possible. It is an operator that assigns to a given theory of a given sentential logic, perceived as a free algebra with a consequence operation on its universe, the largest congruence on the algebra that is compatible with the theory.
Formulation.
In this article, we introduce the Leibniz operator in the special case of classical propositional calculus, then we abstract it to the general notion applied to an arbitrary sentential logic and, finally, we summarize some of the most important consequences of its use in the theory of abstract algebraic logic. 
Let 
denote the classical propositional calculus. According to the classical 
Lindenbaum–Tarski process, given a theory
formula_2 of formula_3,
if formula_4
denotes the binary relation on the set of formulas 
of formula_3, defined by
where formula_8 denotes the usual
classical propositional equivalence connective, then
formula_4 turns out to be a congruence
on the formula algebra. Furthermore, the quotient 
formula_10 is a Boolean algebra
and every Boolean algebra may be formed in this way.
Thus, the variety of Boolean algebras, which is,
in algebraic logic terminology, the 
equivalent algebraic semantics (algebraic counterpart)
of classical propositional calculus, is the class of
all algebras formed by taking appropriate quotients
of free algebras by those special kinds of
congruences.
The condition 
that defines 
formula_6 is equivalent to the 
condition 
Passing now to an arbitrary sentential logic 
given a theory formula_2,
the Leibniz congruence associated with formula_2 is
denoted by formula_18 and is defined, for all
formula_19, by
if and only if, for every formula 
formula_21 containing a variable formula_22
and possibly other variables in the list formula_23,
and all formulas formula_24 forming a list of the same 
length as that of formula_23, we have that
if and only if formula_27.
It turns out that this binary relation is a congruence relation on the formula algebra and, in fact, may alternatively be characterized as the largest congruence on the formula algebra that is compatible
with the theory formula_2, in the sense that if formula_20 and formula_13, then we must have also formula_14. It is this congruence that plays the same role as the congruence used in the traditional Lindenbaum–Tarski process described above in the context of an arbitrary sentential logic. 
It is not, however, the case that for arbitrary sentential logics the quotients of the free algebras by these Leibniz congruences over different theories yield all algebras in the class that forms the natural algebraic counterpart of the sentential logic. This phenomenon occurs only in the case of "nice" logics and one of the main goals of abstract algebraic logic is to make this vague notion of a logic being "nice", in this sense, mathematically precise. 
The Leibniz operator 
is the operator that maps a theory formula_2 of a given logic to the 
Leibniz congruence 
associated with the theory. Thus, formally, 
is a mapping from the collection 
formula_3 to the collection 
of all congruences on the formula algebra formula_39 
of the sentential logic.
Hierarchy.
The Leibniz operator and the study of various of its properties that may or may not be satisfied for particular sentential logics have given rise to what is now known as the abstract algebraic hierarchy or Leibniz hierarchy of sentential logics. Logics are classified in various levels of this hierarchy depending on how strong a tie exists between the logic and its algebraic counterpart.
The properties of the Leibniz operator that help classify the logics are monotonicity, injectivity, continuity and commutativity with inverse substitutions. For instance, protoalgebraic logics, forming the widest class in the hierarchy, i.e., the one that lies in the bottom of the hierarchy and contains all other classes, are characterized by the monotonicity of the Leibniz operator on their theories.
Other notable classes are formed by the equivalential logics, the weakly algebraizable logics and the algebraizable logics, among others.
There is a generalization of the Leibniz operator, in the context of categorical abstract algebraic logic, that makes it possible to apply a wide variety of techniques that were previously applicable only in the sentential logic framework to logics formalized as formula_40-institutions.
The formula_40-institution framework is significantly wider in scope than the framework of sentential logics because it allows incorporating multiple signatures and quantifiers in the language and it provides a mechanism for handling logics that are not syntactically based.