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.