1
$\begingroup$

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

$\endgroup$

2 Answers 2

5
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ I think that the context is ZF, rather than RCA; but the point is the same. We don't need anything more than ZF to prove the compactness theorem for countable theories. When we move from a countable theory to an arbitrary theory it is no longer the case we can use $2^{<\omega}$ as a "guide" for generating larger and larger extensions, and this is where the axiom of choice comes into play. $\endgroup$
    – Asaf Karagila
    Jan 14, 2016 at 10:02
  • $\begingroup$ @CarlMummert Quite right, I was being silly: I took the last sentence of en.wikipedia.org/wiki/PA_degree#Properties as attributing the result to Simpson's survey paper (derp :P) "Degrees of unsolvability: a survey of results". Fixed! $\endgroup$ Jan 16, 2016 at 20:59
  • $\begingroup$ That makes sense. @Noah $\endgroup$ Jan 16, 2016 at 21:14
3
$\begingroup$

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.

$\endgroup$
1

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.