The Lindenbaum–Tarski algebra of a theory in propositional logic is an algebraic (and order-theoretic) structure built out of its formula?s (modulo provable equivalence) and connectives. It thus carries an algebraic structure that corresponds to the logic in question and is generally the free such structure generated by the axioms of the theory.
The Lindenbaum–Tarski algebra of a theory in classical propositional logic is a Boolean algebra.
Associated to any normal modal logic, in (and more generally) is an algebra ,which is a BAO of type , i.e. (modal) operators, . This is called the Lindenbaum–Tarski algebra of , and is a quotient of the term algebra? of , i.e. of the free universal algebra of type formed by the -formulae using the connectives , , , , , and the . The Lindenbaum–Tarski algebra is formed from this free algebra by using the congruence , where
(Recall the usual rules of notation: is ; is ; and means .)
The elements of are the equivalence classes:
with the operations
As we assumed that was normal, the normality schemata:
, in the form,
and monotonicity :
if then .
is a normal operator.
We first note that , then the result follows by simply writing down what is required and staring at it for a moment!
The Lindenbaum–Tarski algebra for a modal logic, , gives rise a canonical Kripke model. This has the set of -maximal consistent formulae as its set of states.