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 term 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
S = ⟨ F m , ⊢ S ⟩ {\displaystyle {\mathcal {S}}=\langle {\rm {Fm}},\vdash _{\mathcal {S}}\rangle }
denote the classical propositional calculus. According to the classical Lindenbaum–Tarski process, given a theory
T {\displaystyle T} of S {\displaystyle {\mathcal {S}}} , if ≡ T {\displaystyle \equiv _{T}}
denotes the binary relation on the set of formulas of S {\displaystyle {\mathcal {S}}} , defined by
ϕ ≡ T ψ {\displaystyle \phi \equiv _{T}\psi } if and only if T ⊢ S ϕ ↔ ψ , {\displaystyle T\vdash _{\mathcal {S}}\phi \leftrightarrow \psi ,}
where ↔ {\displaystyle \leftrightarrow } denotes the usual classical propositional equivalence connective, then
≡ T {\displaystyle \equiv _{T}} turns out to be a congruence on the formula algebra. Furthermore, the quotient
F m / ≡ T {\displaystyle {\rm {Fm}}/{\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
T ⊢ S ϕ ↔ ψ {\displaystyle T\vdash _{\mathcal {S}}\phi \leftrightarrow \psi }
that defines
ϕ ≡ T ψ {\displaystyle \phi \equiv _{T}\psi } is equivalent to the condition
for every formula χ {\displaystyle \chi } : T ⊢ S ϕ ↔ χ {\displaystyle T\vdash _{\mathcal {S}}\phi \leftrightarrow \chi } if and only if T ⊢ S ψ ↔ χ {\displaystyle T\vdash _{\mathcal {S}}\psi \leftrightarrow \chi } . Passing now to an arbitrary sentential logic
S = ⟨ F m , ⊢ S ⟩ , {\displaystyle {\mathcal {S}}=\langle {\rm {Fm}},\vdash _{\mathcal {S}}\rangle ,}
given a theory T {\displaystyle T} , the Leibniz congruence associated with T {\displaystyle T} is denoted by Ω ( T ) {\displaystyle \Omega (T)} and is defined, for all
ϕ , ψ ∈ F m {\displaystyle \phi ,\psi \in {\rm {Fm}}} , by
ϕ Ω ( T ) ψ {\displaystyle \phi \Omega (T)\psi }
if and only if, for every formula
α ( x , y → ) {\displaystyle \alpha (x,{\vec {y}})} containing a variable x {\displaystyle x}
… excerpt ends here. Continue reading the full article.
