Lindenbaum algebra

Identify classical propositional formulae when their equivalence is provable from a fixed theory. Their equivalence classes form the Lindenbaum algebra: meet and join are induced by conjunction and disjunction, complementation by negation, and the order by provable implication. Provable equivalence is preserved by each connective, so these operations are well-defined; the familiar classical propositional identities make this a Boolean algebra. A homomorphism of lattices to $\{0,1\}$ preserving zero and one also preserves complements and therefore specifies a truth valuation of the atomic propositions. All axioms of the fixed theory represent one. Separating the class of an unprovable formula from one consequently gives a countervaluation, proving the completeness theorem for propositional logic.

Take formulas whose free variables lie among a fixed $n$-tuple and identify them when their universal equivalence follows from $T$. Conjunction, disjunction and negation induce a Boolean algebra; its order is implication modulo $T$. Complete types correspond to ultrafilters and isolated complete types to atoms. For a complete theory in a countable language, finiteness of these algebras for every finite $n$ characterizes countable categoricity.