The Lindenbaum-Tarski algebra of a logical theory T is the algebra obtained by taking the set of all formulas in the language of T and quotienting by the relation of logical equivalence within T. Two formulas are identified when T proves them equivalent. The result is an algebraic structure whose operations mirror the logical connectives.
The nature of the resulting algebra depends on the logic:
- For a classical propositional theory, the Lindenbaum-Tarski algebra is a Boolean algebra. Every formula is equivalent to its double negation, and excluded middle holds.
- For an intuitionistic propositional theory, the Lindenbaum-Tarski algebra is a Heyting algebra. Implication is not reducible to negation and disjunction, and excluded middle need not hold.
This construction provides the algebraic semantics for a given logic. It makes precise the sense in which algebraic structures (Boolean algebras, Heyting algebras) are the “natural home” for logical reasoning: every theory generates one, and conversely every such algebra arises as the Lindenbaum-Tarski algebra of some theory.
Adolf Lindenbaum introduced the construction; Alfred Tarski developed its algebraic properties. The construction is a standard tool in mathematical logic for connecting syntactic theories with their semantic counterparts.
In the context of this vault, the Lindenbaum-Tarski construction clarifies why the semiotic universe takes a Heyting algebra as its base: the algebra of judgements about signs is the Lindenbaum-Tarski algebra of a constructive theory of sign relations.