nLab Lindenbaum-Tarski algebra



The Lindenbaum–Tarski algebra of a theory in propositional logic is an algebraic (and order-theoretic) structure built out of its formulas (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 normal modal logic

Associated to any normal modal logic, Λ\Lambda in ω(n)\mathcal{L}_\omega(n) (and more generally) is an algebra 𝔄 ω Λ\mathfrak{A}^\Lambda_\omega,which is a BAO of type nn, i.e. nn (modal) operators, m im_i. This is called the Lindenbaum–Tarski algebra of Λ\Lambda, and is a quotient of the term algebra? of ω(n)\mathcal{L}_\omega(n), i.e. of the free universal algebra of type nn formed by the ω(n)\mathcal{L}_\omega(n)-formulae using the connectives \vee, \wedge, ¬\neg, \bot, \top, and the i\Diamond_i. The Lindenbaum–Tarski algebra is formed from this free algebra by using the congruence Λ\simeq_\Lambda, where

ϕ Λψ Λϕψ.\phi \simeq_\Lambda\psi \iff {\vdash}_\Lambda \phi\leftrightarrow \psi.

(Recall the usual rules of notation: ϕψ\phi \to \psi is ¬ϕψ\neg\phi\vee\psi; ϕψ\phi\leftrightarrow \psi is (ϕψ)(ψϕ)(\phi\to \psi)\wedge (\psi\to\phi); and Λϕ{\vdash}_\Lambda \phi means ϕΛ\phi \in \Lambda.)

The elements of 𝔄 ω Λ\mathfrak{A}^\Lambda_\omega are the equivalence classes:

ϕ={ψ Λϕψ},{\left\|\phi\right\|} = \{\psi \mid \vdash_\Lambda \phi\leftrightarrow \psi\},

with the operations

  • ϕ+ψ=ϕψ{\left\|\phi\right\|} + {\left\|\psi\right\|} = {\left\|\phi \vee \psi\right\|};

  • ϕψ=ϕψ{\left\|\phi\right\|} \cdot {\left\|\psi\right\|}= {\left\|\phi \wedge \psi\right\|};

  • ϕ =¬ϕ{\|\phi\|^-} = {\|\neg\phi\|};

  • 0=0 = {\|\bot\|};

  • 1=1 = {\|\top\|};


  • m iϕ= iϕm_i {\|\phi\|} = {\|\Diamond_i\phi\|} .

As we assumed that Λ\Lambda was normal, the normality schemata:

(K)(K): (ψχ)ψχ\Diamond(\psi \vee \chi)\to \diamond \psi\vee \diamond \chi;

(N)(N), in the form, ¬ i()\neg \Diamond_i(\bot)

and monotonicity :

if ψχΛ\psi \to \chi \in \Lambda then iψ iχΛ\Diamond_i \psi \to \Diamond_i \chi \in \Lambda.



m im_i is a normal operator.


We first note that Λ(ψϕ) iψ iϕ\vdash_\Lambda \Diamond(\psi\vee \phi) \leftrightarrow \Diamond_i \psi \vee \Diamond_i \phi, then the result follows by simply writing down what is required and staring at it for a moment!

Canonical models

The Lindenbaum–Tarski algebra for a modal logic, Λ\Lambda, gives rise a canonical Kripke model. This has the set of Λ\Lambda-maximal consistent formulae as its set of states.

Last revised on July 12, 2017 at 10:59:29. See the history of this page for a list of all contributions to it.