Lindenbaum–Tarski algebra
Encyclopedia
In mathematical logic
, the Lindenbaum–Tarski algebra (or Lindenbaum algebra) of a logical theory T consists of the equivalence classes of sentence
s of the theory (i.e., the quotient
, under the 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
.
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
.
and disjunction, which are well-defined
on the equivalence classes. When negation
is also present in T, then A is a Boolean algebra, provided the logic is classical
. If the theory is propositional
and its set of logical connective
s is functionally complete, the Lindenbaum-Tarski algebra is the free Boolean algebra
generated by the set of propositional variable
s.
s and interior algebra
s are the Lindenbaum-Tarski algebras for intuitionistic logic
and the modal logic
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 logics where Tarski's method is inapplicable are relevance logic
s, 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
.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, the Lindenbaum–Tarski algebra (or Lindenbaum algebra) of a logical theory T consists of the equivalence classes of sentence
Sentence (mathematical logic)
In mathematical logic, a sentence of a predicate logic is a boolean-valued well formed formula with no free variables. A sentence can be viewed as expressing a proposition, something that may be true or false...
s of the theory (i.e., the quotient
Quotient
In mathematics, a quotient is the result of division. For example, when dividing 6 by 3, the quotient is 2, while 6 is called the dividend, and 3 the divisor. The quotient further is expressed as the number of times the divisor divides into the dividend e.g. The quotient of 6 and 2 is also 3.A...
, under the equivalence relation
Equivalence relation
In mathematics, an equivalence relation is a relation that, loosely speaking, partitions a set so that every element of the set is a member of one and only one cell of the partition. Two elements of the set are considered equivalent if and only if they are elements of the same cell...
~ 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
Quotient algebra
In mathematics, a quotient algebra, , also called a factor algebra is obtained by partitioning the elements of an algebra in equivalence classes given by a congruence, that is an equivalence relation that is additionally compatible with all the operations of the algebra, in the formal sense...
obtained by factoring the algebra of formulas by this congruence relation
Congruence relation
In abstract algebra, a congruence relation is an equivalence relation on an algebraic structure that is compatible with the structure...
.
The algebra is named for logicians Adolf Lindenbaum
Adolf Lindenbaum
Adolf Lindenbaum , was a Polish logician and mathematician.He was a student of Wacław Sierpiński, became a distinguished author of works on set theory and had served as an Assistant Professor at Warsaw University...
and Alfred Tarski
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
. It was first introduced by Tarski in 1935 as a device to establish correspondence between classical propositional calculus
Propositional calculus
In mathematical logic, a propositional calculus or logic is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true...
and Boolean algebras. The Lindenbaum–Tarski algebra is considered the origin of the modern algebraic logic
Algebraic logic
In mathematical logic, algebraic logic is the study of logic presented in an algebraic style.What is now usually called classical algebraic logic focuses on the identification and algebraic description of models appropriate for the study of various logics and connected problems...
.
Operations
The operations in a Lindenbaum–Tarski algebra A are inherited from those in the underlying theory T. These typically include conjunctionLogical conjunction
In logic and mathematics, a two-place logical operator and, also known as logical conjunction, results in true if both of its operands are true, otherwise the value of false....
and disjunction, which are well-defined
Well-defined
In mathematics, well-definition is a mathematical or logical definition of a certain concept or object which uses a set of base axioms in an entirely unambiguous way and satisfies the properties it is required to satisfy. Usually definitions are stated unambiguously, and it is clear they satisfy...
on the equivalence classes. When negation
Negation
In logic and mathematics, negation, also called logical complement, is an operation on propositions, truth values, or semantic values more generally. Intuitively, the negation of a proposition is true when that proposition is false, and vice versa. In classical logic negation is normally identified...
is also present in T, then A is a Boolean algebra, provided the logic is classical
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
. If the theory is propositional
Propositional calculus
In mathematical logic, a propositional calculus or logic is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true...
and its set of logical connective
Logical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s is functionally complete, the Lindenbaum-Tarski algebra is the free Boolean algebra
Free Boolean algebra
In abstract algebra, a branch of mathematics, a free Boolean algebra is a Boolean algebra 〈B,F〉, such that the set B has a subset whose elements are called generators...
generated by the set of propositional variable
Propositional variable
In mathematical logic, a propositional variable is a variable which can either be true or false...
s.
Related algebras
Heyting algebraHeyting algebra
In mathematics, a Heyting algebra, named after Arend Heyting, is a bounded lattice equipped with a binary operation a→b of implication such that ∧a ≤ b, and moreover a→b is the greatest such in the sense that if c∧a ≤ b then c ≤ a→b...
s and interior algebra
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 ordinary propositional logic...
s are the Lindenbaum-Tarski algebras for intuitionistic logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
and the modal logic
Modal logic
Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
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 logics where Tarski's method is inapplicable are relevance logic
Relevance logic
Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications be relevantly related. They may be viewed as a family of substructural or modal logics...
s, 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
Abstract Algebraic Logic
In mathematical logic, abstract algebraic logic is the study of the algebraization of deductive systemsarising as an abstraction of the well-known Lindenbaum-Tarski algebra, and how the resulting algebras are related to logical systems.-Overview:...
.