Are there any purely semantic proofs of the compactness theorem that don't use the full axiom of choice?

Question

Using Godel's completeness theorem, it can be shown that the compactness theorem is equivalent to the ultrafilter lemma. The compactness theorem can also be proven using ultraproducts and Los's Theorem, but it requires reference to the full axiom of choice. My question is: are there any known proofs of the compactness theorem that make no reference to syntactic provability, that use no choice principles stronger than BPIT?

Answer 1

Jech proves compactness from the ultrafilter theorem in his The Axiom of Choice. He uses the ultrafilter theorem to show how one can take an appropriate set $M$ of finite, binary-valued partial functions on a set $X$, and produce a totally defined binary-valued function $f:X\to 2$ such that every $f\restriction p$ is in $M$ for all finite $p\subseteq X$.

The idea is then to take $X$ as all the sentences of a language and let $\Sigma$ be a consistent theory. Then $M$ is the set of all truth value assignments $t$ to finite sets of sentences such that A) $dom(t)\cap\Sigma$ has a model and B) $t(\varphi)=1$ iff $\varphi$ is true in that model. Assuming every finite subset of $\Sigma$ has a model, this $M$ matches the criteria Jech describes and can be expanded to a total binary function on the sentences of the language, defining a maximal consistent theory with $\Sigma$ as a subtheory. A Henkin construction then gives you the sought after model of $\Sigma$.