In P. Johnstone "Notes on Logic and Set theory" there is a proof of completeness (and then compactness) of propositional logic for a countable set of base atomic proposition, avoiding the choise axiom (in the exercise Johnstone prove it in general by Zorn Lemma).
If you want I send you the outline of the proof. \

THE OUTLINE:

Let $S\subset Bool(P)$ a set of propositions (where $Bool(P)$ is the set of propositional expressions building from a set of primitives proposition alphabet $P=${*p, q, r, s..*} this is the free Boolean algebra on the set $P$). A valuation is a funtion $v: P\to ${$1$}, any valuation as a unique natural extension to $S$ that indicate still by the some letter $v: S\to ${$1$}. We write $S\models s$ if any valuation $v$ such that is 1 (true) on all elements of $S$ is $1$ also on $s$. We write $S\vdash s$ is there is a *deduction* of $s$ from $S$. We call $S$ inconsistent if $S\vdash \bot$ and consistent if $S\vdash \bot$ is false.
Then $S\models \bot$ means that any valuation $s$ is $0$ (false) on each members of $S$ (where $\bot$ is the atomic expression "false").

LEMMA1.

If $S\models \bot$ then $S\vdash \bot$ (i.e. $S$ is inconsistent).

PROOF (in the case of $P$ countable): We have to suppose $S$ consistent, and show a valuation $v$ on $P$ such that $v(s)=1$.
Observe that for $t\in Bool(P)$ we have that either $S\cup${$t$} or $S\cup${$\neg t$} is consistent (if $S\cup${$t$}$\vdash \bot$ from deduction lemma follow that $S\vdash (t\to \bot)$ i.e. $S\vdash \neg t$ (we can define $ \neg t:= t\to \bot$), and then $S\models \neg t$ then is $S$ is consistent (hypothesis) so is $S\cup${$\neg t$}).

Then we enumerate the elements of $Bool(P)$ and one to one add it to $S$ is preserve the consistence, ot add its negation in opposite. We have a set $S'\supset S$ which is consistent (is $S'\vdash \bot$ then exist a dedution of $\bot$ from $S'$ that involve a finite number of elements of $S'$), and such that for any $t\in Bool(P)$ or $t$ ot $\neq t$ belong to $S'$. Let $v(t)=1\ if\ t\in S'$ and $v(t)=0\ if\ t\not\in S'$ . We claim that $v$ is a valutation i.e. preserve the boolean operations: clearly $v(\bot)=0$, and its enought show that $v(s\to t)= (v(s)\to v(t))$, we shall consider three cases:

1) $v(t)=1$ i.i $t\in S'$ Then we cannot have $\neg (s\to t)\in S'$ since $t\vdash (s\to t)$ and $S'$ is consistent. So $s\to t)\in S'$ i.e. $v(s\to t)=1= v(s)\to v(t))$.

2) $v(s)=0$, then $\neg s\in S'$, and since $\neg s \vdash (s\to t)$ (exercise) as in $(1)$ we must have $v(s\to t)=1= v(s)\to v(t))$.

3) $v(s)=1,\ v(t)=0$ . In this case we have $s\in S'$ and $t\not\in S'$ so since {$s,\ s\to t$}$\vdash t$ we have $(s\to t)\not\in S'$ hence $v(s\to t)=0= v(s)\to v(t))$.

Theorem of Completeness: $S\models t\ iff\ S\vdash t$.

PROOF. The "$if$" part is obvious. Suppose $S\models t$, from {$t, \neg t$}$\vdash \bot$ we have $S\cup${$\neg t$}$\models \bot$, by lemma we have $S\cup${$\neg t$}$\vdash \bot$, by deduction lemma we have
$S\vdash (\neg t)\to \bot$ then $S\vdash t$ .

Theorem of Compactness: is $S\models t$ then $S\vdash t$ then exist a finite $S'\subset S$ such that $S'\vdash t$ and then $S'\models t$.

Hausdorffspaces is compact (Hausdorff) is strictly weaker than Tychonoff; it's equivalent to the compactness theorem, and it's also equivalent to the ultrafilter lemma. – Qiaochu Yuan Nov 19 '11 at 21:32