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?
Best Answer
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.