Leibniz operator


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 theoryT 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, thenequiv_{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{Sphiif 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 allphi,psiin{ m Fm}, by

:phiOmega(T)psi

if and only if, for every formula alpha(x,vec{y}) containing a variable xand 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.


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Leibniz (disambiguation) — Gottfried Leibniz (1646 – 1716) was a German philosopher and mathematician.In mathematics, several results and concepts are attributed to Leibniz:* Leibniz algebra, an algebraic structure * Leibniz formula for pi, a method for calculating pi; *… …   Wikipedia

  • Leibniz rule (generalized product rule) — In calculus, the Leibniz rule, named after Gottfried Leibniz, generalizes the product rule. It states that if f and g are n times differentiable functions, then the n th derivative of the product fg is given by:(f cdot g)^{(n)}=sum {k=0}^n {n… …   Wikipedia

  • Dolbeault-Operator — Die äußere Ableitung oder Cartan Ableitung ist eine Funktion aus den Bereichen Differentialgeometrie und Analysis. Die äußere Ableitung verallgemeinert das aus der Analysis bekannte Leibniz sche Differential auf den Raum der Differentialformen.… …   Deutsch Wikipedia

  • Minimal negation operator — In logic and mathematics, the minimal negation operator u! is a multigrade operator ( u {k}) {k in mathbb{N where each u {k}! is a k ary boolean function defined in such a way that u {k}(x 1, ldots , x k) = 1 if and only if exactly one of the… …   Wikipedia

  • Modal operator — In modal logic, a modal operator is an operator which forms propositions from propositions. In general, a modal operator has the formal property of being non truth functional, and is intuitively characterised by expressing a modal attitude (such… …   Wikipedia

  • List of mathematics articles (L) — NOTOC L L (complexity) L BFGS L² cohomology L function L game L notation L system L theory L Analyse des Infiniment Petits pour l Intelligence des Lignes Courbes L Hôpital s rule L(R) La Géométrie Labeled graph Labelled enumeration theorem Lack… …   Wikipedia

  • Лейбниц, Готфрид Вильгельм — Готфрид Вильгельм Лейбниц Gottfried Wilhelm Leibniz …   Википедия

  • Список объектов, названных в честь Лейбница — Существует несколько математических и другого рода объектов, названных в честь Лейбница: Содержание 1 Теоремы 2 Формулы 3 Прочее 4 См …   Википедия

  • Non-classical logic — Non classical logics (and sometimes alternative logics) is the name given to formal systems which differ in a significant way from standard logical systems such as propositional and predicate logic. There are several ways in which this is done,… …   Wikipedia

  • Notation for differentiation — In differential calculus, there is no single uniform notation for differentiation. Instead, several different notations for the derivative of a function or variable have been proposed by different mathematicians. The usefulness of each notation… …   Wikipedia