Is the Lindenbaum-Theorem of sentential logic (= propositional logic) provable in ZF (i. e. without the axiom of choice)?
Lindenbaum's theorem of sentential logic states that every set $\Sigma$ of sentences of the propositional calculus can be enlarged to a maximal consistent set $\Gamma$ of sentences of the propositional calculus.
To prove this theorem concerning the whole predicates logic you need the axiom of choice. My question is, whether you need the axiom of choice to prove Lindenbaum's theorem if you only consider sentential logic.
In general, no. Because your propositional logic could have a "strange" number of propositional variables.
If you assume, however, that there are only countably many propositional variables, then you can prove without the aid of the axiom of choice that there are only countably many propositions to write. Then you can enumerate them, and start enlarging your theory one step at a time by going through the enumeration; and at the end you get a maximal consistent theory.
Lesser known fact is that this theorem when applied to propositional calculus, and when applied predicate calculus, both have the same "choice strength". Which in the countable case is none, and in the general case is the Boolean Prime Ideal Theorem.