Topological proof of the Compactness Theorem in propositional logic without the Axiom of Choice There is a well-known proof of the Compactness Theorem in propositional logic which uses the compactness of the space $\{0,1\}^P$, where $P$ is the set of propositional variables in consideration. In general, this compactness relies on the Tychonoff theorem which in turn requires the Axiom of Choice. Let me sketch it (in danger of boring the experts, but for reference it will be useful):
For a set $A$ of formulas in $P$, let $T(A)$ be the set of interpretations $P \to \{0,1\}$ which make the formulas in $A$ true. Then $T(\cup_i A_i)=\cap_i T(A_i)$ and each $T(A)$ is closed in $\{0,1\}^P$. Thus if $A$ is finitely consistent, then $T(A)$ is the directed intersection of nonempty closed sets, thus also nonempty (compactness).
My question concerns the case that $P = \{p_1,p_2,\dotsc\}$ is countable. Then it seems to me that it is provable in ZF that $\{0,1\}^P$ is compact: Use the homeomorphism to the closed cantor set $C \subseteq [0,1]$ and the compactness of $[0,1]$. From this we can conclude that the Compactness Theorem in propositional logic for countably many propositional variables is provable in ZF - if everything is correct so far.
Isn't this somehow counterintuitive? Or does this proof yield a constructive algorithm how to find an interpretation which makes all formulas in $A$ true provided one can find them for finitely many?
 A: 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$.
A: The proof is correct, but it does not provide an algorithm unless you have some additional information about $A$.  If you untangle the proofs, you find the following pseudo-algorithm: Go through the propositional variables $p_i$ in order, adding each $p_i$ or its negation to $A$ "greedily", i.e., add $p_i$ if doing so leaves $A$ (which now contains the original $A$, all your previous additions, and $p_i$) finitely satisfiable, and otherwise add $\neg p_i$.  An easy induction shows that this preserves finite satisfiability.  At the end, your decisions tell you what truth value to give each $p_i$, and it's easy to check that $A$ is satisfied by this truth assignment.  The reason this is only a pseudo-algorithm rather than an algorithm is that there is, in general, no way to decide what happens at any step.  You'd need to able to decide whether a certain set of formulas (the original $A$ plus decisions) is consistent, and that might not be algorithmically decidable, even if the original $A$ was a computable set of formulas.
