# 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?

-
If the language is countable, then the set of formulas is well-ordered and you don't need choice to prove Lindembaum's lemma. This holds also for first order logic. Nevertheless, the condition in the inductive step of the construction of a complete theory extending some given first order theory is not, in general, recursive because it asks if a sentence is consistent or not with the given theory. –  Rodrigo Freire Nov 19 '11 at 16:26
The compactness theorem does not require choice if the set of symbols in the theory is countable (or well-orderable). So, it can be proved in ZF. But, this does not give a constructive proof unless you can also prove it without the law of the excluded middle. –  George Lowther Nov 19 '11 at 16:29
FWIW, to prove that a product of compact Hausdorff spaces 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

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.

-
Thanks for this great answer! So after all, the topological proof is overkill. On the other hand, I wonder if your argument translates to a proof that $2^P$ is compact. –  Martin Brandenburg Nov 19 '11 at 17:08
This proof of propositional compactness can be rewritten as a proof that $2^P$ is compact for countable $P$. Under the usual identification of $2^P$ with the Cantor set, the proof amounts to an argument by repeated bisection. –  Andreas Blass Nov 19 '11 at 18:15

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$.

-