Leibniz operator

In abstract algebraic 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.

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 ${\displaystyle T}$ of ${\displaystyle {\mathcal {S}}}$, if ${\displaystyle \equiv _{T}}$ denotes the binary relation on the set of formulas of ${\displaystyle {\mathcal {S}}}$, defined by

...
Wikipedia