Leibniz operator

One of the cornerstone concepts in the theory of
abstract algebraic logic is that of the Leibniz operator.

Motivation

The Leibniz operator was introduced by Willem 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 applicableto 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 algebrawith a consequence operation on its universe, thelargest congruence on the algebra that is compatible with the theory.

Formulation

In this article, we introduce the Leibniz operator in the special case of classicalpropositional calculus, then we abstract it to the general notion applied to an arbitrary sentential logic and, finally, we summarizesome of the most important consequences ofits use in the theory of abstract algebraic logic.

Let

:$mathcal\{S\}=langle\{\; m\; Fm\},vdash\_\{mathcal\{S\; angle$ denote the classical propositional calculus. According to the classical Lindenbaum-Tarski process, given a theory$T$ of $mathcal\{S\}$,if $equiv\_\{T\}$denotes the binary relation on the set of formulas of $mathcal\{S\}$, defined by

:$phiequiv\_\{T\}psi$ if and only if $phileftrightarrowpsiin\; T,$ where $leftrightarrow$ denotes the usualclassical propositional equivalence connective, then$equiv\_\{T\}$ turns out to be a congruenceon the formula algebra. Furthermore, the quotient $\{\; m\; Fm\}/\{equiv\_\{T$ is a Boolean algebraand every Boolean algebra may be formed in this way.

Thus, the variety of Boolean algebras, which is,in Abstract Algebraic Logic terminology, the equivalent algebraic semantics (algebraic counterpart)of classical propositional calculus, is the class ofall algebras formed by taking appropriate quotientsof free algebras by those special kinds ofcongruences.

The condition :$phileftrightarrowpsiin\; T$

that defines $phiequiv\_\{T\}psi$ is equivalent to the condition

:$Tvdash\_\{mathcal\{Sphi$if and only if $Tvdash\_\{mathcal\{Spsi$.

Passing now to an arbitrary sentential logic :$mathcal\{S\}=langle\{\; m\; Fm\},vdash\_\{mathcal\{S\; angle,$

given a theory $T$,the Leibniz congruence associated with $T$ isdenoted by $Omega(T)$ and is defined, for all$phi,psiin\{\; m\; Fm\}$, by

:$phiOmega(T)psi$

if and only if, for every formula $alpha(x,vec\{y\})$ containing a variable $x$and possibly other variables in the list $vec\{y\}$,and all formulas $vec\{chi\}$ forming a list of the same length as that of $vec\{y\}$, we have that

:$Tvdash\_\{mathcal\{Salpha(phi,vec\{chi\})$if and only if $Tvdash\_\{mathcal\{Salpha(psi,vec\{chi\})$.

It turns out that this binary relation is a congruence relationon the formula algebra and, in fact, may alternatively be characterizedas the largest congrunece on the formula algebra that is compatiblewith the theory $T$, in the sense thatif $phiOmega(T)psi$ and $phiin\; T$, then we must have also $psiin\; T$. It is this congruence thatplays the same role as the congruence used in thetraditional 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 bythese Leibniz congruences over different theories yield all algebrasin the class that forms the natural algebraic counterpart of thesentential logic. This phenomenon occurs only in the caseof "nice" logics and one of the main goals of Abstract Algebraic Logicis to make this vague notion of a logic being "nice", in thissense, mathematically precise. The Leibniz operator

:$Omega$

is the operator that maps a theory $T$ of a given logic to the Leibniz congruence

:$Omega(T),$

that is associated with the theory. Thus, formally,

:$Omega:\{\; m\; Th\}mathcal\{S\}\; ightarrow\{\; m\; Con\}\{\; m\; Fm\}$

is a mapping from the collection

:$\{\; m\; Th\}mathcal\{S\}$ of the theories of a sentential logic $mathcal\{S\}$ to the collection

:$\{\; m\; Con\}\{\; m\; Fm\}$

of all congruences on the formula algebra $\{\; m\; Fm\}$of the sentential logic.

Hierarchy

The Leibniz operator and the study of various of its properties that may or may not be satisfied for particularsentential logics have given rise to what is now known asthe abstract algebraic hierarchy or Leibniz hierarchy ofsentential logics. Logics are classified in various steps 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 classifythe logics are monotonicity, injectivity, continuityand 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 hierarchyand contains all other classes, are characterized bythe monotonicity of the Leibniz operator on their theories.Other famous classes are formed by the equivalential logics,the weakly algebraizable logics, the algebraizable logicsetc.

By now, there is a generalization of the Leibniz operator in the context of CategoricalAbstract Algebraic Logic, that makes it possibleto apply a wide variety of techniques that werepreviously applicable in the sentential logicframework to logics formalized as $pi$-institutions.The $pi$-institution framework is significantly widerin scope than the framework of sentential logicsbecause it allows incorporating multiple signaturesand quantifies in the language and it provides a mechanism forhandling logics that are not syntactically-based.