In
mathematical logic, the Lindenbaum–Tarski algebra (or Lindenbaum algebra) of a
logical theory ''T'' consists of the
equivalence class
In mathematics, when the elements of some set S have a notion of equivalence (formalized as an equivalence relation), then one may naturally split the set S into equivalence classes. These equivalence classes are constructed so that elements a ...
es of
sentences of the theory (i.e., the
quotient, under the
equivalence relation
In mathematics, an equivalence relation is a binary relation that is reflexive, symmetric and transitive. The equipollence relation between line segments in geometry is a common example of an equivalence relation.
Each equivalence relation ...
~ defined such that ''p'' ~ ''q'' exactly when ''p'' and ''q'' are provably equivalent in ''T''). That is, two sentences are equivalent if the theory ''T'' proves that each implies the other. The Lindenbaum–Tarski algebra is thus the
quotient algebra obtained by factoring the algebra of formulas by this
congruence relation
In abstract algebra, a congruence relation (or simply congruence) is an equivalence relation on an algebraic structure (such as a group, ring, or vector space) that is compatible with the structure in the sense that algebraic operations done wi ...
.
The algebra is named for
logicians
Adolf Lindenbaum and
Alfred Tarski.
It was first introduced by Tarski in 1935
as a device to establish correspondence between classical
propositional calculus and
Boolean algebras.
The Lindenbaum–Tarski algebra is considered the origin of the modern
algebraic logic
In mathematical logic, algebraic logic is the reasoning obtained by manipulating equations with free variables.
What is now usually called classical algebraic logic focuses on the identification and algebraic description of models appropriate for ...
.
[; here: pages 1-2]
Operations
The operations in a Lindenbaum–Tarski algebra ''A'' are inherited from those in the underlying theory ''T''. These typically include
conjunction and
disjunction, which are
well-defined on the equivalence classes. When
negation
In logic, negation, also called the logical complement, is an operation that takes a proposition P to another proposition "not P", written \neg P, \mathord P or \overline. It is interpreted intuitively as being true when P is false, and false ...
is also present in ''T'', then ''A'' is a
Boolean algebra, provided the logic is
classical. If the theory ''T'' consists of the
propositional tautologies, the Lindenbaum–Tarski algebra is the
free Boolean algebra In mathematics, a free Boolean algebra is a Boolean algebra with a distinguished set of elements, called ''generators'', such that:
#Each element of the Boolean algebra can be expressed as a finite combination of generators, using the Boolean opera ...
generated by the
propositional variables.
Related algebras
Heyting algebras and
interior algebra In abstract algebra, an interior algebra is a certain type of algebraic structure that encodes the idea of the topological interior of a set. Interior algebras are to topology and the modal logic S4 what Boolean algebras are to set theory and o ...
s are the Lindenbaum–Tarski algebras for
intuitionistic logic and the
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
S4, respectively.
A logic for which Tarski's method is applicable, is called ''algebraizable''. There are however a number of logics where this is not the case, for instance the modal logics S1, S2, or S3, which lack the
rule of necessitation (⊢φ implying ⊢□φ), so ~ (defined above) is not a congruence (because ⊢φ→ψ does not imply ⊢□φ→□ψ). Another type of logic where Tarski's method is inapplicable is
relevance logics, because given two theorems an implication from one to the other may not itself be a theorem in a relevance logic.
[ The study of the algebraization process (and notion) as topic of interest by itself, not necessarily by Tarski's method, has led to the development of ]abstract algebraic logic
In mathematical logic, abstract algebraic logic is the study of the algebraization of deductive systems
arising as an abstraction of the well-known Lindenbaum–Tarski algebra, and how the resulting algebras are related to logical systems.Font, 20 ...
.
See also
* Algebraic semantics (mathematical logic)
*Leibniz operator 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 W ...
* List of Boolean algebra topics
References
*
{{DEFAULTSORT:Lindenbaum-Tarski algebra
Algebraic logic
Algebraic structures