Compactness for countable models?

Question

How and where is it proved that WKL$_0$ proves the compactness theorem for countable models? (This is a follow-up to a comment of F. Dorais.)

Answer 1

The proof is basically the usual Henkinization proof of completeness (and hence compactness as a corollary), using your favorite proof system. Starting with a consistent theory, first add constants and complete the theory, then build the term model.

The only noneffective step here is completing the theory, which is where $WKL_0$ comes in: given a consistent theory $S$ in a language $L$, we build a tree of complete consistent extensions of $S$ as follows. Let $\{\varphi_i: i\in\omega\}$ be a listing of all the $L$-sentences. For $\sigma\in 2^{<\omega}$, let $S_\sigma=S\cup\{\varphi_i: \sigma(i)=1\}\cup\{\neg\varphi(i): \sigma(i)=0\}$, and say a theory $S'$ is $n$-consistent if $S'\cap\{\varphi_i: i<n\}$ cannot prove a contradiction in fewer than $n$ steps. Note that telling whether a theory is $n$-consistent is computable. Now let $$T_S=\{\sigma: S_\sigma\text{ is $\vert\sigma\vert$-consistent}\}.$$ Since telling whether a theory is $n$-complete is effective, the tree $T_S$ exists by $RCA_0$. It's not hard to show that $T_S$ is infinite since $S$ is finitely satisfiable, so by $WKL_0$ it has a path $f$. This $f$ yields a complete consistent theory extending $S$.

You can now check that the term model built according to $f$ is in fact a model of $T$; this is the usual analysis, and goes through unchanged in $RCA_0$.

---

But wait! Did we have to derive Compactness as a corollary of Completeness? This may seem odd, since we can classically get compactness on its own - either via ultraproducts (clearly a no-no here), or by Henkinization with "finitely satisfiable" in place of "consistent." However, as it turns out, in the reverse mathematical context it is necessary to go through completeness, at least if you want to work in $WKL_0$.

Why? Look at the definition of the tree $T_S$. The analogous predicate "$n$-satisfiable" is a priori merely $\Sigma^1_1$, so the version of $T_S$ build with "$n$-satisfiability" does not obviously exist in $WKL_0$.

---

For more details, see Simpson's book Subsystems of Second-Order Arithmetic.

EDIT: See Carl Mummert's answer for a citation. The reversal was proved by Harvey Friedman in 1976, improving a prior result by Friedman from 1974.

Answer 2

The statement for the completeness theorem is due to Harvey Friedman, 1976, "Systems of second order arithmetic with restricted induction II", p. 558 of: Meeting of the Association for Symbolic Logic, John Baldwin, D. A. Martin, Robert I. Soare and W. W. Tait, The Journal of Symbolic Logic, Vol. 41, No. 2 (Jun., 1976), pp. 551-560, http://www.jstor.org/stable/2272259

Friedman had previously worked in systems without restricted induction. He stated the corresponding result for the completeness theorem for WKL in his paper "Some Systems of Second Order Arithmetic and Their Use", Proceedings of the International Congress of Mathematicians, Vancouver, 1974, pp. 235-242, http://www.mathunion.org/ICM/ICM1974.1/Main/icm1974.1.0235.0242.ocr.pdf

As Noah Schweber mentioned, the proof of the completeness theorem in WKL is essentially just a formalization of Henkin's proof of the completeness theorem from ZFC. However, Friedman's theorems show that the completeness theorem for countable first-order theories is equivalent to WKL over RCA (also to $\mathsf{WKL}_0$ over $\mathsf{RCA}_0$), which requires an additional proof for the reversal.