= Lindenbaum algebra
{c}
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>.
Back to article page
