Leibniz operator

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

${\displaystyle \mathcal{S}=⟨\mathrm{F}\mathrm{m},{⊢}_{\mathcal{S}}⟩}$

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

${\displaystyle \varphi {\equiv }_T\psi }$ if and only if ${\displaystyle T{⊢}_{\mathcal{S}}\varphi \leftrightarrow \psi ,}$

where ${\displaystyle \leftrightarrow }$ denotes the usual classical propositional equivalence connective, then ${\displaystyle {\equiv }_T}$ turns out to be a congruence on the formula algebra. Furthermore, the quotient ${\displaystyle \mathrm{F}\mathrm{m}/{\equiv }_T}$ 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 term algebras by those special kinds of congruences.

Notice that the condition

${\displaystyle T{⊢}_{\mathcal{S}}\varphi \leftrightarrow \psi }$

that defines ${\displaystyle \varphi {\equiv }_T\psi }$ is equivalent to the condition

for every formula ${\displaystyle \chi }$: ${\displaystyle T{⊢}_{\mathcal{S}}\varphi \leftrightarrow \chi }$ if and only if ${\displaystyle T{⊢}_{\mathcal{S}}\psi \leftrightarrow \chi }$.

Passing now to an arbitrary sentential logic

${\displaystyle \mathcal{S}=⟨\mathrm{F}\mathrm{m},{⊢}_{\mathcal{S}}⟩,}$

given a theory ${\displaystyle T}$, the Leibniz congruence associated with ${\displaystyle T}$ is denoted by ${\displaystyle \mathrm{\Omega }(T)}$ and is defined, for all ${\displaystyle \varphi ,\psi \in \mathrm{F}\mathrm{m}}$, by

${\displaystyle \varphi \mathrm{\Omega }(T)\psi }$

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

${\displaystyle T{⊢}_{\mathcal{S}}\alpha (\varphi ,\overrightarrow{\chi })}$ if and only if ${\displaystyle T{⊢}_{\mathcal{S}}\alpha (\psi ,\overrightarrow{\chi })}$.

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 ${\displaystyle T}$, in the sense that if ${\displaystyle \varphi \mathrm{\Omega }(T)\psi }$ and ${\displaystyle T{⊢}_{\mathcal{S}}\varphi }$, then we must have also ${\displaystyle T{⊢}_{\mathcal{S}}\psi }$. 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 term 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

${\displaystyle \mathrm{\Omega }}$

is the operator that maps a theory ${\displaystyle T}$ of a given logic to the Leibniz congruence

${\displaystyle \mathrm{\Omega }(T),}$

associated with the theory. Thus, formally,

${\displaystyle \mathrm{\Omega }:\mathrm{T}\mathrm{h}(\mathcal{S})\to \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{F}\mathrm{m})}$

is a mapping from the collection

${\displaystyle \mathrm{T}\mathrm{h}(\mathcal{S})}$ of the theories of a sentential logic

${\displaystyle \mathcal{S}}$ to the collection

${\displaystyle \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{F}\mathrm{m})}$

of all congruences on the formula algebra ${\displaystyle \mathrm{F}\mathrm{m}}$ of the sentential logic.