Uncountable-language proof of propositional completeness (source code)

= Uncountable-language proof of propositional completeness

When the primitive propositions are not countable, replace sequential enumeration of the formulae by <Zorn lemma>. The union of a chain of consistent extensions is consistent because every formal proof is finite, so every consistent theory extends to a <maximal consistent set in propositional logic>. Declaring an atom true exactly when it belongs to that maximal set and proving the truth lemma by structural induction produces a model.